Set Implicit Arguments. Unset Strict Implicit. Require Export gzloc. Require Export cardinal. Module Infinite. Export UpdateA. Export Cardinal. (** First we go back to the next things we wanted to prove in cardinal. **) Lemma is_infinite_rw1 : forall x, is_infinite x = (exists f, Transformation.injective x x f & ~(Transformation.surjective x x f)). Proof. ir. ap iff_eq; ir. uh H; ee. ap excluded_middle. uhg; ir. ap H. uhg. ir. ap excluded_middle. uhg; ir. ap H0. sh f. ee. am. uhg; ir. ap H2. uhg; ee. uh H1; ee; am. am. am. nin H. ee. uhg. uhg; ir. uh H1; ee. cp (H1 x0 H). ap H0. uh H2; ee; am. Qed. Lemma is_infinite_rw : forall x, is_infinite x = (exists f, exists u, (inc u x & Transformation.injective x x f & (forall v, inc v x -> ~ (f v = u)))). Proof. ir. ap iff_eq; ir. rwi is_infinite_rw1 H. nin H; ee. sh x0. ap excluded_middle. uhg; ir. ap H0. uhg; ee. uh H; ee; am. uhg. ir. ap excluded_middle. uhg; ir. ap H1. sh x1; ee. am. am. ir. uhg; ir. ap H3. sh v; ee. am. am. rw is_infinite_rw1. nin H. nin H. sh x0. ee. am. uhg; ir. uh H1; ee. uh H2; ee. uh H3. cp (H3 x1 H). nin H4. ee. apply H1 with x2. am. am. Qed. Lemma infinite_sub_infinite : forall x, (exists y, (is_infinite y & sub y x)) -> is_infinite x. Proof. ir. nin H. ee. rwi is_infinite_rw H. nin H. nin H. ee. set (g:= fun (y:E) => Y (inc y x0) (x1 y) y). assert (forall y, inc y x0 -> g y = x1 y). ir. uf g. rw Y_if_rw. tv. am. assert (forall y, ~inc y x0 -> g y = y). ir. uf g. rw Y_if_not_rw. tv. am. assert (forall y, inc y x -> inc (g y) x). ir. apply by_cases with (inc y x0); ir. rw H3. ap H0. uh H1; ee. uh H1. app H1. am. rw H4. am. am. assert (Transformation.injective x x g). uhg; ee. uhg. am. uhg. ir. apply by_cases with (inc x3 x0); ir. apply by_cases with (inc y x0); ir. rwi H3 H8. rwi H3 H8. uh H1; ee. uh H11. ap H11. am. am. am. am. am. rwi H3 H8. rwi H4 H8. assert False. ap H10. wr H8. uh H1; ee. uh H1. ap H1. am. elim H11. am. am. apply by_cases with (inc y x0); ir. assert False. ap H9. rwi H4 H8. rwi H3 H8. rw H8. uh H1; ee. uh H1; ap H1. am. am. am. elim H11. rwi H4 H8. rwi H4 H8. am. am. am. assert (forall v, inc v x -> g v <> x2). ir. apply by_cases with (inc v x0); ir. rw H3. app H2. am. rw H4. uhg; ir. ap H8. rww H9. am. rw is_infinite_rw. sh g. sh x2. ee. app H0. am. am. Qed. Lemma is_finite_natural : forall x, inc x nat -> is_finite x. Proof. ir. set (i:= B H). cp (B_eq H). fold i in H0. wr H0. clear H0. nin i. rw nat_zero_emptyset. ap finite_emptyset. rw nat_succ_tack_on. ap finite_tack_on. am. Qed. Lemma is_infinite_nat : is_infinite nat. Proof. rw is_infinite_rw. sh (fun x => tack_on x x). sh emptyset. ee. wr nat_zero_emptyset. ap R_inc. uhg; ee. uhg. ir. cp (B_eq H). wr H0. wr nat_succ_tack_on. ap R_inc. uhg; ir. cp (B_eq H). cp (B_eq H0). set (i:= B H). fold i in H2. set (j:= B H0). fold j in H3. wri H2 H1. wri H3 H1. wr H2; wr H3. wri nat_succ_tack_on H1. wri nat_succ_tack_on H1. assert (S i = S j). ap R_inj. am. assert (i = j). om. rww H5. ir. cp (B_eq H). set (i:= B H). fold i in H0. wr H0. wr nat_succ_tack_on. uhg; ir. wri nat_zero_emptyset H1. assert (S i = 0). app R_inj. discriminate. Qed. Lemma is_finite_cardinality : forall x, is_finite (cardinality x) = is_finite x. Proof. ir. ap iff_eq; ir. ap finite_invariant. sh (cardinality x). ee. ap are_isomorphic_symm. ap card_isomorphic. am. ap finite_invariant. sh x. ee. ap card_isomorphic. am. Qed. Lemma is_infinite_cardinality : forall x, is_infinite (cardinality x) = is_infinite x. Proof. ir. uf is_infinite. rw is_finite_cardinality. tv. Qed. (** We have to do the following to manipulate nat as an element of E because actually it is of type Set; whenever it appears in one of our formulae it gets pushed up into E but if it stands alone we should write natE e.g. in the assertion [natE = union nat]. **) Definition natE : E. exact nat. Defined. Lemma is_ordinal_nat : is_ordinal nat. Proof. change (is_ordinal natE). assert (natE = union nat). ap extensionality; uhg; ir. cp (B_eq H). set (i:= B H). fold i in H0. apply union_inc with (tack_on x x). rw tack_on_inc. ap or_intror; tv. wr H0. wr nat_succ_tack_on. ap R_inc. cp (union_exists H). nin H0. ee. assert (sub x0 nat). cp (B_eq H1). wr H2. ap Naturals.sub_R_nat. ap H2. am. rw H. ap ordinal_union. ir. cp (B_eq H0). wr H1. ap Naturals.nat_ordinal. Qed. Lemma inc_cardinality_nat_or_sub_nat_cardinality : forall x, (inc (cardinality x) nat) \/ (sub nat (cardinality x)). Proof. ir. assert (is_ordinal (cardinality x)). ap cardinality_ordinal. cp (is_ordinal_nat). cp (ordinal_lt_lt_eq_or H H0). nin H1. rwi ordinal_lt_rw H1. ee. ap or_introl; am. nin H1. ap or_intror. assert (ordinal_leq nat (cardinality x)). rw ordinal_leq_inc_tack_on. rw tack_on_inc. ap or_introl. rwi ordinal_lt_rw H1. ee. am. am. uh H2; ee. am. ap or_intror. rw H1. uhg; ir. am. Qed. Lemma is_finite_inc_cardinality_nat : forall x, is_finite x = inc (cardinality x) nat. Proof. ir. wr is_finite_cardinality. ap iff_eq; ir. cp (inc_cardinality_nat_or_sub_nat_cardinality x). nin H0. am. assert (is_infinite (cardinality x)). ap infinite_sub_infinite. sh natE. ee. ap is_infinite_nat. am. uh H1. assert False. app H1. elim H2. app is_finite_natural. Qed. Lemma is_infinite_sub_nat_cardinality : forall x, is_infinite x = sub nat (cardinality x). Proof. ir. uf is_infinite. rw is_finite_inc_cardinality_nat. ap iff_eq; ir. cp (inc_cardinality_nat_or_sub_nat_cardinality x). nin H0. assert False. app H. elim H1. am. uhg; ir. assert (inc (cardinality x) (cardinality x)). ap H. am. assert (is_ordinal (cardinality x)). ap cardinality_ordinal. cp (ordinal_not_inc_itself H2). app H3. Qed. Definition plus_one x := tack_on x x. Lemma is_ordinal_plus_one : forall x, is_ordinal x -> is_ordinal (plus_one x). Proof. ir. uf plus_one. ap ordinal_tack_on. am. Qed. Lemma plus_one_R : forall (i:nat), plus_one (R i) = R (i+1). Proof. ir. uf plus_one. wr nat_succ_tack_on. assert (S i = i+1). om. rww H. Qed. Lemma inc_plus_one_nat : forall x, inc x nat -> inc (plus_one x) nat. Proof. ir. cp (B_eq H). wr H0. rw plus_one_R. ap R_inc. Qed. Lemma function_V_tack_on_old : forall f x y z, Function.axioms f -> ~inc x (domain f) -> inc z (domain f) -> V z (tack_on f (pair x y)) = V z f. Proof. ir. sy. ap function_sub_V. ap function_tack_on_axioms. am. am. uhg. ee. am. am. uhg; ir. rw tack_on_inc. app or_introl. Qed. Lemma function_V_tack_on_new : forall f x y z, Function.axioms f -> ~inc x (domain f) -> z = x -> V z (tack_on f (pair x y)) = y. Proof. ir. util (pr2_V (f:=tack_on f (pair x y)) (x:=pair x y)). app function_tack_on_axioms. rw tack_on_inc. app or_intror. rwi pr1_pair H2. rwi pr2_pair H2. sy; rww H1. Qed. Lemma are_isomorphic_tack_on : forall x y u v, ~inc y x -> ~inc v u -> are_isomorphic x u -> are_isomorphic (tack_on x y) (tack_on u v). Proof. ir. uh H1. nin H1. uhg. sh (tack_on x0 (pair y v)). uh H1; ee. uh H1. uh H2. uh H3. ee. uh H5. uh H4. uhg. dj. uhg; ee. ap function_tack_on_axioms. am. rww H6. rw domain_tack_on. rww H6. rw range_tack_on. uhg; ir. rwi tack_on_inc H8. nin H8. rw tack_on_inc. ap or_introl. app H7. rw H8. rw tack_on_inc; app or_intror. uhg. ee. am. uhg. ir. rwi tack_on_inc H9. nin H9. cp (H5 x1 H9). nin H10. ee. sh x2. ee. rw tack_on_inc. app or_introl. rw function_V_tack_on_old. am. am. rww H6. rww H6. sh y. ee. rw tack_on_inc. app or_intror. rw function_V_tack_on_new. sy; am. am. rww H6. tv. uhg; ee. am. uhg. ir. rwi tack_on_inc H10; rwi tack_on_inc H11. nin H10; nin H11. ap H4. am. am. rwi function_V_tack_on_old H12. rwi function_V_tack_on_old H12. am. am. rww H6. rww H6. am. rww H6. rww H6. rwi function_V_tack_on_old H12. rwi function_V_tack_on_new H12. assert False. ap H0. ap H7. wr H12. ap range_inc. am. sh x1. ee. rww H6. tv. elim H13. am. rww H6. am. am. rww H6. rww H6. rwi function_V_tack_on_new H12. rwi function_V_tack_on_old H12. assert False. ap H0. ap H7. rw H12. ap range_inc. am. sh y0. ee. rww H6. tv. elim H13. am. rww H6. rww H6. am. rww H6. am. rww H11. Qed. Lemma nat_are_isomorphic_eq : forall x y, inc x nat -> inc y nat -> are_isomorphic x y -> x = y. Proof. assert (forall (i j:nat), i < j -> ~(are_isomorphic (R i) (R j))). ir. uhg; ir. assert (are_isomorphic (R j) (R i)). app are_isomorphic_symm. set (g:= isotrans (R j) (R i)). assert (is_infinite (R j)). rw is_infinite_rw. sh g. sh (R (j-1)). ee. ap Naturals.lt_implies_inc. om. uf g. assert (Transformation.bijective (R j) (R i) (isotrans (R j) (R i))). ap isotrans_bij. am. uhg; ee. uhg. ir. uh H2; ee. uh H2. assert (inc (isotrans (R j) (R i) x) (R i)). ap H2. am. assert (sub (R i) (R j)). ap Naturals.le_implies_sub. om. app H7. uhg. ir. uh H2; ee. uh H7; ee. uh H8; ee. ap H8. am. am. am. ir. assert (inc (g v) (R i)). assert (Transformation.bijective (R j) (R i) (isotrans (R j) (R i))). ap isotrans_bij. am. uf g. uh H3; ee. uh H3; ee. ap H3. am. uhg; ir. rwi H4 H3. rwi Naturals.inc_lt H3. om. uh H2. ap H2. ap is_finite_natural. ap R_inc. ir. cp (B_eq H0); cp (B_eq H1). set (i:= B H0); set (j:= B H1). fold i in H3; fold j in H4. wr H3; wr H4. assert (~ i < j). uhg; ir. cp (H _ _ H5). ap H6. rw H3; rww H4. assert (~ j < i). uhg; ir. cp (H _ _ H6). ap H7. ap are_isomorphic_symm. rw H3; rww H4. assert (i = j). om. rww H7. Qed. Lemma nat_cardinality_refl : forall x, inc x nat -> cardinality x = x. Proof. ir. ap nat_are_isomorphic_eq. wr is_finite_inc_cardinality_nat. ap is_finite_natural. am. am. ap are_isomorphic_symm. ap card_isomorphic. Qed. Lemma cardinality_tack_on : forall x y, is_finite x -> ~inc y x -> cardinality (tack_on x y) = plus_one (cardinality x). Proof. ir. uf plus_one. ap nat_are_isomorphic_eq. wr is_finite_inc_cardinality_nat. ap finite_tack_on. am. assert (inc (cardinality x) nat). wr is_finite_inc_cardinality_nat. am. cp (B_eq H1). wr H2. wr nat_succ_tack_on. ap R_inc. ap are_isomorphic_trans. sh (tack_on x y). ee. ap are_isomorphic_symm. ap card_isomorphic. ap are_isomorphic_tack_on. am. ap ordinal_not_inc_itself. ap cardinality_ordinal. ap card_isomorphic. Qed. Definition number x := Bnat (cardinality x). Lemma R_number : forall x, is_finite x -> R (number x) = cardinality x. Proof. ir. rwi is_finite_inc_cardinality_nat H. uf number. rw R_Bnat. tv. am. Qed. Lemma cardinality_emptyset : cardinality emptyset = emptyset. Proof. ap extensionality; uhg; ir. assert (are_isomorphic emptyset (cardinality emptyset)). ap card_isomorphic. uh H0; ee. nin H0. uh H0; ee. uh H1; ee. uh H3. cp (H3 x H). nin H4. ee. nin H4. elim x2. nin H. elim x0. Qed. Lemma number_emptyset : forall x, x = emptyset -> number x = 0. Proof. ir. ap R_inj. rw nat_zero_emptyset. rw R_number. rw H. rww cardinality_emptyset. rw H. ap finite_emptyset. Qed. Lemma number_tack_on : forall x y, is_finite x -> ~inc y x -> number (tack_on x y) = (number x) + 1. Proof. ir. uf number. transitivity (S (Bnat (cardinality x))). rw cardinality_tack_on. ap R_inj. rw R_Bnat. rw nat_succ_tack_on. rw R_Bnat. tv. wr is_finite_inc_cardinality_nat. am. ap inc_plus_one_nat. wrr is_finite_inc_cardinality_nat. am. am. om. Qed. Definition take_out x y := complement x (singleton y). Lemma inc_take_out : forall x y z, inc z (take_out x y) = (inc z x & ~z=y). Proof. ir. uf take_out. rw inc_complement. ap iff_eq; ir. ee. am. uhg; ir. ap H0. rw H1. ap singleton_inc. ee. am. uhg; ir. ap H0. ap singleton_eq. am. Qed. Lemma tack_on_take_out : forall x y, inc y x -> tack_on (take_out x y) y = x. Proof. ir. ap extensionality; uhg; ir. rwi tack_on_inc H0. nin H0. rwi inc_take_out H0. ee. am. rww H0. rw tack_on_inc. apply by_cases with (x0 = y). ir. app or_intror. ir. ap or_introl. rww inc_take_out. ee; am. Qed. Lemma not_inc_take_out : forall x y, ~inc y (take_out x y). Proof. ir. uhg; ir. rwi inc_take_out H. ee. ap H0. tv. Qed. Lemma subset_finite : forall x, (exists y, (sub x y & is_finite y)) -> is_finite x. Proof. ir. nin H. ee. apply excluded_middle. uhg; ir. assert (is_infinite x0). apply infinite_sub_infinite. sh x. ee. am. am. uh H2; au. Qed. Lemma is_finite_take_out : forall x y, is_finite x -> is_finite (take_out x y). Proof. ir. ap subset_finite. sh x. ee. uhg; ir. rwi inc_take_out H0; ee. am. am. Qed. Lemma number_take_out : forall x y, is_finite x -> inc y x -> number (take_out x y) = (number x) -1. Proof. ir. cp (tack_on_take_out H0). transitivity (number (tack_on (take_out x y) y) - 1). rw number_tack_on. om. ap is_finite_take_out. am. ap not_inc_take_out. rww H1. Qed. Lemma number_zero_emptyset : forall x, is_finite x -> number x = 0 -> x = emptyset. Proof. ir. ap extensionality; uhg; ir. cp (tack_on_take_out H1). wri H2 H0. rwi number_tack_on H0. assert False. om. elim H3. app is_finite_take_out. ap not_inc_take_out. nin H1. nin x1. Qed. Lemma number_gt_zero_nonempty : forall x, is_finite x -> number x > 0 -> (exists y, inc y x). Proof. ir. ap excluded_middle; uhg; ir. assert (x = emptyset). ap extensionality; uhg; ir. assert False. ap H1. sh x0. am. elim H3. nin H2. nin x1. rwi H2 H0. rwi number_emptyset H0. om. tv. Qed. Lemma finite_induction: forall (p:EP) x, (p emptyset) -> (forall y z, p y -> p (tack_on y z)) -> is_finite x -> p x. Proof. ir. assert (forall n, (forall y, is_finite y -> number y = n -> p y)). intro n. nin n; ir. cp (number_zero_emptyset H2 H3). rww H4. assert (number y > 0). om. cp (number_gt_zero_nonempty H2 H4). nin H5. cp (tack_on_take_out H5). wr H6. ap H0. ap IHn. ap is_finite_take_out. am. rw number_take_out. rw H3. om. am. am. apply H2 with (number x). am. tv. Qed. Lemma image_create_tack_on : forall x y f, Image.create (tack_on x y) f = tack_on (Image.create x f) (f y). Proof. ir. ap extensionality; uhg; ir. rwi Image.inc_rw H. nin H. ee. rwi tack_on_inc H. rw tack_on_inc. nin H. ap or_introl. rw Image.inc_rw. sh x1. ee; try am. ap or_intror. wrr H. sy; am. rwi tack_on_inc H. rw Image.inc_rw. nin H. rwi Image.inc_rw H. nin H. ee. sh x1. ee. rw tack_on_inc. app or_introl. am. sh y. ee. rw tack_on_inc. app or_intror. sy; am. Qed. Lemma image_create_emptyset : forall f, Image.create emptyset f = emptyset. Proof. ir. ap extensionality; uhg; ir. rwi Image.inc_rw H. nin H. ee. nin H. nin x1. nin H. nin x0. Qed. Lemma image_finite : forall x f, is_finite x -> is_finite (Image.create x f). Proof. ir. apply finite_induction with (p:= fun y=> is_finite (Image.create y f)). rw image_create_emptyset. ap finite_emptyset. ir. rw image_create_tack_on. ap finite_tack_on. am. am. Qed. (** We do some additional things about infinite cardinals. These eventually should be put back into Cardinal when we do a backward-revamp. **) (** We would like to show that if [a] is an infinite cardinal then the disjoint union of [a] with itself, and the product of [a] with itself, have the same cardinality as [a]. The idea of the proof is to look at [op_triangle a] which is the set of pairs (x,y) of elements of [a] with [ordinal_leq y x]. Up to a [union2] this is basically the same as [product a a]. The [op_triangle a] is well-ordered by [op_lex] the lexicographic ordering on ordinal pairs (i.e. pairs of ordinals). If [a] is a cardinal then all downward subsets of [op_triangle a] have cardinality strictly smaller than that of [a], using the induction hypothesis; this allows us to conclude that [op_triangle a] has cardinality less than or equal to that of [a]. Along the way we use this fact to obtain the statement that [union2] doesn't increase cardinality; then we can use that to go from [op_triangle a] to [product a a] obtaining the induction step. **) Definition is_ordinal_pair x := is_pair x & is_ordinal (pr1 x) & is_ordinal (pr2 x). Definition op_lex_lt x y := is_ordinal_pair x & is_ordinal_pair y & (ordinal_lt (pr1 x) (pr1 y) \/ (pr1 x = pr1 y & ordinal_lt (pr2 x) (pr2 y))). Definition op_lex_leq x y := is_ordinal_pair x & is_ordinal_pair y & (ordinal_lt (pr1 x) (pr1 y) \/ (pr1 x = pr1 y & ordinal_leq (pr2 x) (pr2 y))). Lemma ordinal_leq_refl : forall x, is_ordinal x -> ordinal_leq x x. Proof. ir. uhg; ee. am. am. uhg; ir; am. Qed. Lemma ordinal_lt_leq : forall x y, ordinal_lt x y -> ordinal_leq x y. Proof. ir. uh H; ee; am. Qed. Lemma ordinal_leq_rw : forall x y, ordinal_leq x y = (ordinal_lt x y \/ (x = y & is_ordinal x)). Proof. ir. ap iff_eq; ir. cp (ordinal_if_leq_or H). nin H0. app or_introl. ap or_intror. ee. am. uh H; ee. am. nin H. uh H; ee. am. ee. wr H. ap ordinal_leq_refl. am. Qed. Lemma op_lex_lt_leq : forall x y, op_lex_lt x y -> op_lex_leq x y. Proof. ir. uh H; ee. uhg; ee. am. am. nin H1. app or_introl. ap or_intror. ee. am. ap ordinal_lt_leq. am. Qed. Lemma op_lex_leq_refl : forall x, is_ordinal_pair x -> op_lex_leq x x. Proof. ir. uhg; ee; try am. ap or_intror. ee. tv. ap ordinal_leq_refl. uh H; ee. am. Qed. Lemma op_lex_leq_rw : forall x y, op_lex_leq x y = (op_lex_lt x y \/ (x = y & is_ordinal_pair x)). Proof. ir. ap iff_eq; ir. uh H; ee. nin H1. ap or_introl. uhg; ee; try am. ap or_introl. am. ee. rwi ordinal_leq_rw H2. nin H2. ap or_introl. uhg; ee. am. am. ap or_intror. ee. am. am. ap or_intror. ee. uh H. uh H0. ap pair_extensionality. ee; am. ee; am. am. am. am. nin H. ap op_lex_lt_leq. am. ee. wr H. ap op_lex_leq_refl. am. Qed. Lemma not_ordinal_lt_refl : forall x, ~(ordinal_lt x x). Proof. ir. uhg; ir. uh H; ee. ap H0. tv. Qed. Lemma not_op_lex_lt_refl : forall x, ~ (op_lex_lt x x). Proof. ir. uhg; ir. uh H; ee. nin H1. ap (not_ordinal_lt_refl H1). ee. ap (not_ordinal_lt_refl H2). Qed. Lemma ordinal_lt_trans : forall x z, (exists y, (ordinal_lt x y & ordinal_lt y z)) -> ordinal_lt x z. Proof. ir. nin H. ee. uh H; uh H0; uhg. ee. ap ordinal_leq_trans. sh x0; ee; am. uhg; ir. wri H3 H0. cp (ordinal_leq_leq_eq H H0). ap H2. am. Qed. Lemma op_lex_lt_trans : forall x z, (exists y, (op_lex_lt x y & op_lex_lt y z)) -> op_lex_lt x z. Proof. ir. nin H. ee. uh H; uh H0; uhg; ee; try am. nin H4. nin H2. ap or_introl. ap ordinal_lt_trans. sh (pr1 x0). ee; am. ee. ap or_introl. wrr H2. nin H2. ap or_introl. ee. rww H4. ap or_intror; ee. wrr H2. ap ordinal_lt_trans. sh (pr2 x0); ee; am. Qed. Lemma op_lex_leq_trans : forall x z, (exists y, (op_lex_leq x y & op_lex_leq y z)) -> op_lex_leq x z. Proof. ir. nin H. ee. rwi op_lex_leq_rw H. rwi op_lex_leq_rw H0. nin H. nin H0. ap op_lex_lt_leq. ap op_lex_lt_trans. sh x0; ee; am. ee. wr H0. ap op_lex_lt_leq. am. nin H0. ee. rww H. app op_lex_lt_leq. ee. rw op_lex_leq_rw. ap or_intror. ee. rww H. am. Qed. Lemma not_ordinal_lt_lt : forall x y, ordinal_lt x y -> ordinal_lt y x -> False. Proof. ir. uh H; uh H0; ee. cp (ordinal_leq_leq_eq H H0). au. Qed. Lemma not_op_lex_lt_lt : forall x y, op_lex_lt x y -> op_lex_lt y x -> False. Proof. ir. uh H; uh H0; ee. nin H4; nin H2. apply not_ordinal_lt_lt with (pr1 x) (pr1 y). am. am. ee. rwi H2 H4. cp (not_ordinal_lt_refl H4). am. ee. rwi H4 H2. cp (not_ordinal_lt_refl H2). am. ee. apply not_ordinal_lt_lt with (pr2 x) (pr2 y). am. am. Qed. Lemma op_lex_leq_leq_eq : forall x y, op_lex_leq x y -> op_lex_leq y x -> x = y. Proof. ir. rwi op_lex_leq_rw H. rwi op_lex_leq_rw H0. nin H; nin H0. cp (not_op_lex_lt_lt H H0). elim H1. ee. sy; am. ee. am. ee. am. Qed. Lemma op_lex_dichotomy : forall x y, is_ordinal_pair x -> is_ordinal_pair y -> (op_lex_lt x y \/ op_lex_lt y x \/ x = y). Proof. ir. cp H; cp H0. uh H1; uh H2; ee. cp (ordinal_lt_lt_eq_or H5 H3). nin H7. ap or_introl. uhg; ee. am. am. app or_introl. nin H7. ap or_intror. ap or_introl. uhg; ee; try am. app or_introl. cp (ordinal_lt_lt_eq_or H6 H4). nin H8. ap or_introl. uhg; ee; try am. ap or_intror; ee. am. am. nin H8. ap or_intror. ap or_introl. uhg; ee; try am. ap or_intror; ee; try am. sy; am. ap or_intror. ap or_intror. app pair_extensionality. Qed. Definition least_ordinal z := sow (fun x => inc x z). Lemma is_ordinal_least_ordinal: forall z, is_ordinal (least_ordinal z). Proof. ir. uf least_ordinal. ap sow_ordinal. Qed. Lemma inc_least_ordinal_ex : forall z, (exists y, (inc y z & is_ordinal y)) -> inc (least_ordinal z) z. Proof. ir. uf least_ordinal. ap sow_property. nin H. ee. sh x; ee; am. Qed. Definition set_of_ordinals z := (forall y, inc y z -> is_ordinal y). Lemma inc_least_ordinal : forall z, set_of_ordinals z -> nonempty z -> inc (least_ordinal z) z. Proof. ir. ap inc_least_ordinal_ex. nin H0. sh y. ee. am. uh H; au. Qed. Lemma ordinal_leq_least_ordinal : forall y z, inc y z -> is_ordinal y -> ordinal_leq (least_ordinal z) y. Proof. ir. uf least_ordinal. ap sow_smallest. am. am. Qed. Definition set_of_ordinal_pairs z := (forall y, inc y z -> is_ordinal_pair y). Lemma set_of_ordinal_pairs_relation : forall z, set_of_ordinal_pairs z -> is_relation z. Proof. ir. uhg; ee. ir. uh H; ee. cp (H _ H0). uh H1; ee; am. Qed. Lemma set_of_ordinals_domain : forall z, set_of_ordinal_pairs z -> set_of_ordinals (domain z). Proof. ir. uhg; ee. ir. ufi domain H0. rwi Image.inc_rw H0. nin H0. ee. uh H. cp (H _ H0). uh H2. ee. wrr H1. Qed. Definition column z x:= range (Z z (fun y => pr1 y = x)). Lemma inc_column : forall z x y, is_relation z -> inc y (column z x) = inc (pair x y) z. Proof. ir. uf column. uf range. rw Image.inc_rw. ap iff_eq; ir. nin H0. ee. Ztac. uh H; ee. cp (H _ H2). rwi is_pair_rw H4. rwi H1 H4. rwi H3 H4. wrr H4. sh (pair x y). ee. Ztac. rww pr1_pair. rww pr2_pair. Qed. Lemma set_of_ordinals_column : forall z x, set_of_ordinal_pairs z -> set_of_ordinals (column z x). Proof. ir. uhg. ir. rwi inc_column H0. uh H; ee. cp (H _ H0). uh H1; ee. rwi pr2_pair H3. am. ap set_of_ordinal_pairs_relation. am. Qed. Lemma nonempty_domain : forall z, nonempty z -> nonempty (domain z). Proof. ir. nin H. sh (pr1 y). uf domain. rw Image.inc_rw. sh y. ee. am. tv. Qed. Lemma nonempty_column : forall z x, is_relation z -> inc x (domain z) -> nonempty (column z x). Proof. ir. ufi domain H0. rwi Image.inc_rw H0. nin H0. ee. sh (pr2 x0). uf column. uf range. rw Image.inc_rw. sh x0. ee. Ztac. tv. Qed. Definition op_lex_least z := pair (least_ordinal (domain z)) (least_ordinal (column z (least_ordinal (domain z)))). Lemma is_ordinal_pair_op_lex_least : forall z, is_ordinal_pair (op_lex_least z). Proof. ir. uhg; ee. uf op_lex_least. ap pair_is_pair. uf op_lex_least. rw pr1_pair. ap is_ordinal_least_ordinal. uf op_lex_least. rw pr2_pair. ap is_ordinal_least_ordinal. Qed. Lemma inc_op_lex_least : forall z, set_of_ordinal_pairs z -> nonempty z -> inc (op_lex_least z) z. Proof. ir. uf op_lex_least. set (k:= least_ordinal (domain z)). assert (is_relation z). app set_of_ordinal_pairs_relation. assert (inc k (domain z)). uf k. ap inc_least_ordinal. app set_of_ordinals_domain. app nonempty_domain. wr inc_column. ap inc_least_ordinal. app set_of_ordinals_column. app nonempty_column. am. Qed. Lemma pr1_op_lex_least : forall z, pr1 (op_lex_least z) = least_ordinal (domain z). Proof. ir. uf op_lex_least. rww pr1_pair. Qed. Lemma pr2_op_lex_least : forall z, pr2 (op_lex_least z) = least_ordinal (column z (least_ordinal (domain z))). Proof. ir. uf op_lex_least. rww pr2_pair. Qed. Lemma op_lex_leq_op_lex_least : forall z y, set_of_ordinal_pairs z -> inc y z -> op_lex_leq (op_lex_least z) y. Proof. ir. assert (nonempty z). sh y. am. assert (is_ordinal_pair (op_lex_least z)). ap is_ordinal_pair_op_lex_least. assert (is_ordinal_pair y). uh H; au. uhg; ee; try am. assert (inc (pr1 y) (domain z)). uf domain. rw Image.inc_rw. sh y. ee; try am; try tv. assert (ordinal_leq (least_ordinal (domain z)) (pr1 y)). ap ordinal_leq_least_ordinal. am. assert (set_of_ordinals (domain z)). app set_of_ordinals_domain. uh H5; au. apply by_cases with (pr1 y = least_ordinal (domain z)); ir. ap or_intror. ee. sy. rww pr1_op_lex_least. assert (inc (pr2 y) (column z (least_ordinal (domain z)))). wr H6. rw inc_column. uh H3; ee. rwi is_pair_rw H3. wr H3. am. app set_of_ordinal_pairs_relation. rw pr2_op_lex_least. ap ordinal_leq_least_ordinal. am. uh H3; ee; am. ap or_introl. uhg; ee. rww pr1_op_lex_least. rw pr1_op_lex_least. uhg; ir. ap H6. sy; am. Qed. (** With the above lemma we have basically finished showing that any set of ordinal pairs is well-ordered by the relation op_lex_leq. However we need to put this into the notation of well-ordered sets. **) Definition op_lex z := Order_notation.create z op_lex_leq. Lemma U_op_lex : forall z, U (op_lex z) = z. Proof. ir. uf op_lex. rw underlying_create; tv. Qed. Lemma leq_op_lex : forall z u v:E, leq (op_lex z) u v = (inc u z & inc v z & op_lex_leq u v). Proof. ir. uf op_lex; rw leq_create_all. tv. Qed. Lemma op_lex_axioms : forall z:E, set_of_ordinal_pairs z -> Order.Definitions.axioms (op_lex z). Proof. ir. uf op_lex. ap Order.Definitions.create_axioms. uf property; dj. ap op_lex_leq_refl. uh H; ee; au. ap op_lex_leq_leq_eq. am. am. ap op_lex_leq_trans. sh y. ee. am. am. Qed. Lemma is_linear_op_lex : forall z:E, set_of_ordinal_pairs z -> is_linear (op_lex z). Proof. ir. uhg; ee. app op_lex_axioms. ir. rwi U_op_lex H0. rwi U_op_lex H1. uh H; ee. cp (H _ H0). cp (H _ H1). cp (op_lex_dichotomy H2 H3). nin H4. ap or_introl. rw leq_op_lex. ee; try am. app op_lex_lt_leq. nin H4. ap or_intror. rw leq_op_lex. ee; try am. app op_lex_lt_leq. ap or_introl. wr H4. rw leq_op_lex. ee; try am. app op_lex_leq_refl. Qed. Lemma is_well_ordered_op_lex : forall z, set_of_ordinal_pairs z -> is_well_ordered (op_lex z). Proof. ir. uhg; ee. app is_linear_op_lex. ir. rwi U_op_lex H0. assert (set_of_ordinal_pairs b). uhg; ir. uh H; ap H. app H0. sh (op_lex_least b). uhg; ee. uhg; ee. app op_lex_axioms. rww U_op_lex. rw U_op_lex. ap H0. ap inc_op_lex_least. am. am. ir. rw leq_op_lex. ee. ap H0. app inc_op_lex_least. app H0. app op_lex_leq_op_lex_least. app inc_op_lex_least. Qed. Definition prod_reflexive z := are_isomorphic z (Cartesian.product z z). Lemma prod_reflexive_invariant : forall y z, are_isomorphic y z -> prod_reflexive y -> prod_reflexive z. Proof. ir. uh H0. uhg. assert (are_isomorphic (product y y) (product z z)). app cartesian_product_isomorphic. ap are_isomorphic_trans. sh (product y y). ee. ap are_isomorphic_trans. sh y. ee. app are_isomorphic_symm. am. am. Qed. Definition sub_prod_reflexive z := forall y, sub y z -> is_infinite y -> prod_reflexive y. Lemma sub_prod_reflexive_rw : forall z, sub_prod_reflexive z = (forall y, iso_sub y z -> is_infinite y -> prod_reflexive y). Proof. ir. ap iff_eq; ir. uh H0. nin H0. ee. apply prod_reflexive_invariant with x. app are_isomorphic_symm. uh H. ap H. am. uhg. uhg; ir. uh H1. ap H1. ap finite_invariant. sh x. ee; try am. app are_isomorphic_symm. uhg. ir. ap H. uhg. sh y. ee. ap are_isomorphic_refl. am. am. Qed. Lemma sub_prod_reflexive_invariant : forall y z, iso_sub y z -> sub_prod_reflexive z -> sub_prod_reflexive y. Proof. ir. uh H0. uhg. ir. assert (iso_sub y0 z). uh H. nin H. ee. uhg. cp (isotrans_bij H). sh (Image.create y0 (isotrans y x)). ee. rw iso_trans_ex_rw. sh (isotrans y x). uhg; dj. uhg. ir. rw Image.inc_rw. sh x0; ee; try am. tv. uhg; ee; try am. uhg; ir. rwi Image.inc_rw H6. nin H6. ee. sh x1; ee. am. am. uhg; ee; try am. uhg; ir. uh H4; ee. uh H11; ee. uh H12. ap H12. ap H1. am. app H1. am. uhg; ir. rwi Image.inc_rw H5. nin H5; ee. wr H6. uh H4; ee. uh H4. assert (inc x1 y). app H1. cp (H4 _ H9). app H3. assert (sub_prod_reflexive z). am. rwi sub_prod_reflexive_rw H4. ap H4. am. am. Qed. Lemma sub_prod_reflexive_prod_reflexive : forall z, is_infinite z -> sub_prod_reflexive z -> prod_reflexive z. Proof. ir. uh H0; ee. ap H0. uhg; ir; am. am. Qed. Lemma finite_sub_prod_reflexive : forall z, is_finite z -> sub_prod_reflexive z. Proof. ir. uhg; ir. assert False. uh H1; ap H1. ap subset_finite. sh z. ee; am. elim H2. Qed. Definition op_triangle z := Z (Cartesian.product z z) (fun y => (ordinal_leq (pr2 y) (pr1 y))). Lemma inc_op_triangle : forall y z, is_ordinal z -> inc y (op_triangle z) = (is_ordinal_pair y & ordinal_lt (pr1 y) z & ordinal_leq (pr2 y) (pr1 y)). Proof. ir. ap iff_eq; ir. ufi op_triangle H0. Ztac. uhg; ee. cp (product_pr H1); ee. am. cp (product_pr H1); ee. apply ordinal_inc_ordinal with z. am. am. cp (product_pr H1); ee. apply ordinal_inc_ordinal with z. am. am. rw ordinal_lt_rw. ee. am. cp (product_pr H1); ee; am. ee. uf op_triangle. Ztac. ap product_inc. uh H0; ee. am. rwi ordinal_lt_rw H1. ee. am. assert (ordinal_lt (pr2 y) z). cp (ordinal_if_leq_or H2). nin H3. ap ordinal_lt_trans. sh (pr1 y). ee; am. rww H3. rwi ordinal_lt_rw H3. ee; am. Qed. Lemma set_of_ordinal_pairs_op_triangle : forall z, is_ordinal z -> set_of_ordinal_pairs (op_triangle z). Proof. ir. uhg. ir. rwi inc_op_triangle H0. ee. am. am. Qed. Lemma iso_sub_op_triangle : forall z, is_ordinal z -> iso_sub z (op_triangle z). Proof. ir. rw iso_sub_trans_rw. sh (fun x => pair x emptyset). uhg; ee. uhg; ir. rw inc_op_triangle. ee. uhg; ee. ap pair_is_pair. rw pr1_pair. apply ordinal_inc_ordinal with z. am. am. rw pr2_pair. ap emptyset_ordinal. rw pr1_pair. rw ordinal_lt_rw. ee; am. rw pr2_pair. rw pr1_pair. uhg; ee. ap emptyset_ordinal. apply ordinal_inc_ordinal with z. am. am. uhg; ir. nin H1. nin x1. am. uhg; ir. transitivity (pr1 (pair x emptyset)). rww pr1_pair. rw H2. rww pr1_pair. Qed. Lemma sub_op_triangle_product : forall z, sub (op_triangle z) (product z z). Proof. ir. uhg; ir. ufi op_triangle H. Ztac. Qed. Lemma same_cardinality_op_triangle : forall z, is_infinite z -> is_ordinal z -> sub_prod_reflexive z -> cardinality (op_triangle z) = cardinality z. Proof. ir. assert (prod_reflexive z). app sub_prod_reflexive_prod_reflexive. uh H2. ap cardinality_invariant. ap bernstein_cantor_schroeder. ap iso_sub_trans. sh (product z z). ee. ap sub_iso_sub. ap sub_op_triangle_product. ap isomorphic_iso_sub. app are_isomorphic_symm. app iso_sub_op_triangle. Qed. Lemma op_triangle_sub : forall y z, sub y z -> sub (op_triangle y) (op_triangle z). Proof. ir. uf op_triangle. uhg; ir. Ztac. assert (inc x (product z z)). rwi inc_product H1; rw inc_product; ee; try am. app H. app H. app Z_inc. Qed. Definition op_triangle_lex z := op_lex (op_triangle z). Lemma U_op_triangle_lex : forall z, U (op_triangle_lex z) = op_triangle z. Proof. ir. uf op_triangle_lex. rww U_op_lex. Qed. Lemma leq_op_triangle_lex : forall z u v, leq (op_triangle_lex z) u v = (inc u (op_triangle z) & inc v (op_triangle z) & op_lex_leq u v). Proof. ir. uf op_triangle_lex. rww leq_op_lex. Qed. Lemma is_well_ordered_op_triangle_lex : forall z, is_ordinal z -> is_well_ordered (op_triangle_lex z). Proof. ir. uf op_triangle_lex. ap is_well_ordered_op_lex. app set_of_ordinal_pairs_op_triangle. Qed. Definition is_cardinal z := cardinality z = z. Lemma is_cardinal_rw : forall z, is_cardinal z = (is_ordinal z & (forall y, ordinal_lt y z -> ordinal_lt (cardinality y) (cardinality z))). Proof. ir. ap iff_eq; ir. ee. uh H. wr H. ap cardinality_ordinal. ir. uh H; ee. ufi cardinality H. assert (ordinal_leq (cardinality y) (cardinality z)). ap sub_cardinal_leq. assert (ordinal_leq y z). rw ordinal_leq_rw. app or_introl. uh H1; ee; am. rwi ordinal_leq_rw H1. nin H1. am. ee. assert (are_isomorphic y z). cp (card_isomorphic y). cp (card_isomorphic z). ap are_isomorphic_trans. sh (cardinality y). ee. am. rw H1. app are_isomorphic_symm. assert (ordinal_leq z y). wr H. ap sow_smallest. rwi ordinal_lt_rw H0. ee. apply ordinal_inc_ordinal with z. am. am. app are_isomorphic_symm. assert (y = z). ap ordinal_leq_leq_eq. ap ordinal_lt_leq. am. am. uh H0. ee. elim (H6 H5). ee. uhg. ap ordinal_leq_leq_eq. ap subset_ordinal_cardinal_leq. am. uhg; ir; am. assert (is_ordinal (cardinality z)). ap cardinality_ordinal. cp (ordinal_leq_leq_or H H1). nin H2. am. rwi ordinal_leq_rw H2. nin H2. cp (H0 _ H2). assert (cardinality (cardinality z) = cardinality z). ap cardinality_invariant. ap are_isomorphic_symm. ap card_isomorphic. rwi H4 H3. uh H3; ee. assert False. app H5. elim H6. ee. rw H2. uhg; ee. am. am. uhg; ir; am. Qed. Lemma is_cardinal_rw2 : forall z, is_cardinal z = (is_ordinal z & (forall y, is_ordinal y -> iso_sub z y -> ordinal_leq z y)). Proof. ir. ap iff_eq; ir. rwi is_cardinal_rw H. ee. am. ir. cp (ordinal_lt_lt_eq_or H H1). nin H3. app ordinal_lt_leq. nin H3. cp (H0 _ H3). assert (cardinality y = cardinality z). ap ordinal_leq_leq_eq. ap ordinal_lt_leq. am. app iso_sub_cardinal_leq. rwi H5 H4. uh H4; ee. assert False. app H6. elim H7. rw H3. uhg; ee. am. am. uhg; ir; am. ee. uhg. ap ordinal_leq_leq_eq. ap subset_ordinal_cardinal_leq. am. uhg; ir; am. ap H0. ap cardinality_ordinal. uhg. sh (cardinality z). ee. ap card_isomorphic. uhg; ir; am. Qed. Lemma is_cardinal_cardinality : forall z, is_cardinal (cardinality z). Proof. ir. rw is_cardinal_rw2. ee. ap cardinality_ordinal. ir. ap ordinal_leq_trans. sh (cardinality y). ee. ap iso_sub_cardinal_leq. ap iso_sub_trans. sh (cardinality z). ee. ap isomorphic_iso_sub. ap card_isomorphic. am. ap subset_ordinal_cardinal_leq. am. uhg; ir; am. Qed. Lemma infinite_cardinality_tack_on : forall x y, is_infinite x -> cardinality (tack_on x y) = cardinality x. Proof. ir. apply by_cases with (inc y x); ir. assert (tack_on x y = x). ap extensionality; uhg; ir. rwi tack_on_inc H1. nin H1. am. rww H1. rw tack_on_inc. ap or_introl. am. rww H1. ap ordinal_leq_leq_eq. ap iso_sub_cardinal_leq. rwi is_infinite_rw H. nin H. nin H. ee. rw iso_sub_trans_rw. sh (fun z => Y (z = y) x1 (x0 z)). uhg; ee. uhg; ir. rwi tack_on_inc H3. nin H3. rw Y_if_not_rw. uh H1; ee. uh H1. ap H1. am. uhg; ir. ap H0. wrr H4. rw Y_if_rw. am. am. uhg; ir. rwi tack_on_inc H3; rwi tack_on_inc H4; nin H3; nin H4. uh H1; ee. uh H6; ap H6. am. am. rwi Y_if_not_rw H5. rwi Y_if_not_rw H5. am. uhg; ir. ap H0. wrr H7. uhg; ir. ap H0. wrr H7. rwi Y_if_not_rw H5. rwi Y_if_rw H5. assert False. cp (H2 _ H3). ap H6. am. elim H6. am. uhg; ir. ap H0. wrr H6. rwi Y_if_rw H5. rwi Y_if_not_rw H5. unfold not in H2. assert False. apply H2 with y0. am. sy; am. elim H6. uhg; ir. ap H0. wrr H6. am. rww H4. ap sub_cardinal_leq. uhg; ir. rw tack_on_inc. app or_introl. Qed. Lemma cardinality_lt_ordinal_lt : forall y z, is_ordinal y -> is_ordinal z -> ordinal_lt (cardinality y) (cardinality z) -> ordinal_lt y z. Proof. ir. cp (ordinal_lt_lt_eq_or H H0). nin H2. am. nin H2. assert (cardinality y = cardinality z). ap cardinality_invariant. ap bernstein_cantor_schroeder. assert (sub (cardinality y) (cardinality z)). cp (ordinal_lt_leq H1). uh H3; ee; am. ap iso_sub_trans. sh (cardinality y). ee. uhg. sh (cardinality y). ee. ap card_isomorphic. uhg; ir; am. ap iso_sub_trans. sh (cardinality z). ee. app sub_iso_sub. uhg; sh z; ee. ap are_isomorphic_symm. ap card_isomorphic. ap sub_refl. ap sub_iso_sub. cp (ordinal_lt_leq H2). uh H3; ee; am. uh H1; ee. assert False. app H4. elim H5. uh H1; ee. assert False. ap H3. rww H2. elim H4. Qed. Lemma ord_card_leq_criterion : forall y z, is_ordinal y -> is_cardinal z -> (forall x, inc x y -> ordinal_lt x z) -> ordinal_leq y z. Proof. ir. uhg; ee. am. rwi is_cardinal_rw H0. ee; am. uhg; ir. cp (H1 _ H2). rwi ordinal_lt_rw H3. ee; am. Qed. Lemma inc_punctured_downward_subset : forall a x y, Order.Definitions.axioms a -> inc x (U a) -> inc y (punctured_downward_subset a x) = lt a y x. Proof. ir. ap iff_eq; ir. ufi punctured_downward_subset H1. Ztac. uf punctured_downward_subset. Ztac. uh H1; ee. uh H1; ee; am. Qed. Lemma punctured_downward_subset_wo_avatar : forall a x, is_well_ordered a -> inc x (U a) -> Transformation.bijective (punctured_downward_subset a x) (wo_avatar a x) (wo_avatar a). Proof. ir. wrr wo_punctured_downward. cp (wo_avatar_bijective H). set (k:= punctured_downward_subset a x). assert (sub k (U a)). uf k. uhg; ir. rwi inc_punctured_downward_subset H2. uh H2; ee. uh H2; ee. am. lu. am. uhg; dj. uhg; ir. rw Image.inc_rw. sh x0; ee; try am. tv. uhg; ee; try am. uhg; ir. rwi Image.inc_rw H4. nin H4. ee. sh x1; ee; am. uhg; ee; try am. uhg; ir. uh H1; ee. uh H9; ee. uh H10. ap H10. app H2. app H2. am. Qed. Lemma cardinality_punctured_downward_subset : forall a x, is_well_ordered a -> inc x (U a) -> (cardinality (punctured_downward_subset a x) = cardinality (wo_avatar a x)). Proof. ir. ap cardinality_invariant. apply trans_bij_isomorphic with (wo_avatar a). app punctured_downward_subset_wo_avatar. Qed. Lemma card_leq_criterion : forall a z, is_well_ordered a -> is_cardinal z -> (forall x, inc x (U a) -> ordinal_lt (cardinality (punctured_downward_subset a x)) z) -> ordinal_leq (cardinality (U a)) z. Proof. ir. ap ord_card_leq_criterion. ap cardinality_ordinal. am. ir. assert (ordinal_leq (cardinality (U a)) (wo_ordinal a)). app wo_ordinal_cardinal_leq. assert (inc x (wo_ordinal a)). uh H3; ee. app H5. ufi wo_ordinal H4. rwi Image.inc_rw H4. nin H4. ee. cp (H1 _ H4). rwi cardinality_punctured_downward_subset H6. ap cardinality_lt_ordinal_lt. wr H5. ap wo_avatar_is_ordinal. am. am. rwi is_cardinal_rw H0; ee; am. uh H0. rw H0. wrr H5. am. am. Qed. Lemma sub_punctured_downward_cone_op_triangle : forall y z, is_ordinal z -> inc y (op_triangle z) -> sub (punctured_downward_subset (op_triangle_lex z) y) (op_triangle (tack_on (pr1 y) (pr1 y))). Proof. ir. uhg; ir. rwi inc_punctured_downward_subset H1. uh H1. ee. rwi leq_op_triangle_lex H1. ee. assert (is_ordinal_pair x). rwi inc_op_triangle H1. ee; am. am. assert (is_ordinal_pair y). rwi inc_op_triangle H3. ee; am. am. rw inc_op_triangle. ee. am. rw ordinal_lt_rw. ee. ap ordinal_tack_on. uh H6; ee; am. uh H4; ee. nin H8. rw tack_on_inc. ap or_introl. rwi ordinal_lt_rw H8. ee; am. ee. rw H8. rw tack_on_inc. ap or_intror; tv. rwi inc_op_triangle H1. ee. am. am. ap ordinal_tack_on. uh H6; ee; am. assert (is_well_ordered (op_triangle_lex z)). app is_well_ordered_op_triangle_lex. lu. rw U_op_triangle_lex. am. Qed. Definition sub_prod_reflexive_below z := is_cardinal z & is_infinite z & (forall y, ordinal_lt y z -> sub_prod_reflexive y). Lemma ordinal_leq_lt_trans : forall x y, (exists z, (ordinal_leq x z & ordinal_lt z y)) -> ordinal_lt x y. Proof. ir. nin H. ee. uhg; ee. ap ordinal_leq_trans. sh x0. ee. am. app ordinal_lt_leq. uhg; ir. uh H0; ee. ap H2. ap ordinal_leq_leq_eq. am. wrr H1. Qed. Lemma is_finite_union2 : forall a b, is_finite a -> is_finite b -> is_finite (union2 a b). Proof. ir. cp (finite_induction (p:=fun x => (is_finite (union2 a x)))). cp (H1 b). ap H2. assert (union2 a emptyset = a). ap extensionality; uhg; ir. rwi inc_union2_rw H3. nin H3. am. nin H3. nin x0. rw inc_union2_rw. app or_introl. rw H3. am. ir. assert (union2 a (tack_on y z) = tack_on (union2 a y) z). ap extensionality; uhg; ir. rwi inc_union2_rw H4. rw tack_on_inc. rw inc_union2_rw. rwi tack_on_inc H4. intuition. rwi tack_on_inc H4. rwi inc_union2_rw H4. rw inc_union2_rw. rw tack_on_inc. intuition. rw H4. ap finite_tack_on. am. am. Qed. Lemma product_singleton_isomorphic : forall a x, are_isomorphic a (product a (singleton x)). Proof. ir. apply trans_bij_isomorphic with (fun y => pair y x). uhg; dj. uhg; ir. rw inc_product. ee. ap pair_is_pair. rww pr1_pair. rw pr2_pair. ap singleton_inc. uhg; ee; try am. uhg; ir. rwi inc_product H0. ee. cp (singleton_eq H2). sh (pr1 x0). ee. am. rwi is_pair_rw H0. sy. wrr H3. uhg; ee; try am. uhg; ir. transitivity (pr1 (pair x0 x)). rww pr1_pair. rw H3. rww pr1_pair. Qed. Lemma is_finite_product : forall a b, is_finite a -> is_finite b -> is_finite (product a b). Proof. ir. set (p := fun x => is_finite (product a x)). change (p b). apply finite_induction. uf p. assert (product a emptyset = emptyset). ap extensionality; uhg; ir. rwi inc_product H1. ee. nin H3. nin x0. nin H1. nin x0. rw H1. ap finite_emptyset. ir. uh H1. uhg. rw product_tack_on. ap is_finite_union2. am. ap finite_invariant. sh a. ee. ap product_singleton_isomorphic. am. am. Qed. Lemma infinite_tack_on_isomorphic: forall z x, is_infinite z -> are_isomorphic z (tack_on z x). Proof. ir. ap are_isomorphic_trans. sh (cardinality z). ee. ap card_isomorphic. ap are_isomorphic_trans. sh (cardinality (tack_on z x)). ee. rw infinite_cardinality_tack_on. ap are_isomorphic_refl. am. ap are_isomorphic_symm. ap card_isomorphic. Qed. Lemma sprb_op_triangle_leq : forall z, sub_prod_reflexive_below z -> ordinal_leq (cardinality (op_triangle z)) z. Proof. ir. assert (op_triangle z = U (op_triangle_lex z)). rww U_op_triangle_lex. rw H0. ap card_leq_criterion. ap is_well_ordered_op_triangle_lex. uh H; ee. rwi is_cardinal_rw H. ee; am. uh H; ee; am. ir. rwi U_op_triangle_lex H1. ap ordinal_leq_lt_trans. sh (cardinality (op_triangle (tack_on (pr1 x) (pr1 x)))). ee. ap sub_cardinal_leq. ap sub_punctured_downward_cone_op_triangle. uh H; ee. rwi is_cardinal_rw H; ee; am. am. set (k:= tack_on (pr1 x) (pr1 x)). ap ordinal_leq_lt_trans. sh (cardinality (product k k)). ee. ap sub_cardinal_leq. ap sub_op_triangle_product. apply by_cases with (is_finite k); ir. assert (is_finite (product k k)). ap is_finite_product. am. am. cp H3. rwi is_finite_inc_cardinality_nat H4. uh H; ee. rwi is_infinite_sub_nat_cardinality H5. cp H. uh H7. rwi H7 H5. rw ordinal_lt_rw. ee. rwi is_cardinal_rw H; ee; am. ap H5. am. assert (is_infinite k). am. uh H; ee. assert (sub_prod_reflexive (pr1 x)). ap H5. rwi inc_op_triangle H1. ee. am. rwi is_cardinal_rw H; ee; am. assert (sub_prod_reflexive k). apply sub_prod_reflexive_invariant with (pr1 x). uf k. uhg. sh (pr1 x). ee. ap are_isomorphic_symm. ap infinite_tack_on_isomorphic. uhg; uhg; ir. ap H2. uf k. ap finite_tack_on. am. uhg; ir; am. am. assert (prod_reflexive k). ap sub_prod_reflexive_prod_reflexive. am. am. uh H8; ee. assert (cardinality (product k k) = cardinality k). ap cardinality_invariant. app are_isomorphic_symm. rw H9. uf k. rw infinite_cardinality_tack_on. apply ordinal_leq_lt_trans. sh (pr1 x). ee. ap iso_sub_ordinal_leq. rwi inc_op_triangle H1. ee. uh H1; ee; am. rwi is_cardinal_rw H; ee; am. ap sub_iso_sub. uhg; ir; am. rw ordinal_lt_rw. ee. rwi is_cardinal_rw H; ee; am. rwi inc_op_triangle H1. ee. rwi ordinal_lt_rw H10. ee; am. rwi is_cardinal_rw H; ee; am. uhg; uhg; ir. ap H2. uf k. ap finite_tack_on. am. Qed. Lemma inc_tack_on_infinite_cardinal : forall z x, is_cardinal z -> is_infinite z -> inc x z -> inc (tack_on x x) z. Proof. ir. cp H. rwi is_cardinal_rw H2; ee. assert (ordinal_lt x z). rw ordinal_lt_rw. ee; am. assert (ordinal_lt (tack_on x x) z). apply cardinality_lt_ordinal_lt. ap ordinal_tack_on. uh H4; ee. uh H4; ee. am. am. apply by_cases with (is_finite x); ir. assert (is_finite (tack_on x x)). ap finite_tack_on. am. rwi is_finite_inc_cardinality_nat H6. rwi is_infinite_sub_nat_cardinality H0. rw ordinal_lt_rw. ee. ap cardinality_ordinal. ap H0. am. assert (is_infinite x). am. ap ordinal_leq_lt_trans. sh (cardinality x). ee. rw infinite_cardinality_tack_on. ap ordinal_leq_refl. ap cardinality_ordinal. am. au. rwi ordinal_lt_rw H5; ee; am. Qed. Lemma tack_on_injective : forall a b, is_ordinal a -> is_ordinal b -> tack_on a a = tack_on b b -> a = b. Proof. ir. assert (forall z, is_ordinal z -> union (tack_on z z) = z). ir. ap extensionality; uhg; ir. cp (union_exists H3). nin H4; ee. rwi tack_on_inc H5. nin H5. assert (ordinal_lt x0 z). rw ordinal_lt_rw. ee. am. am. uh H6; ee. uh H6; ee. ap H9. am. wrr H5. apply union_inc with z. am. rw tack_on_inc. app or_intror. cp (H2 _ H). cp (H2 _ H0). wr H3; wr H4. rww H1. Qed. Lemma iso_sub_double_op_triangle : forall z, is_cardinal z -> is_infinite z -> iso_sub (product z (R 2)) (op_triangle z). Proof. ir. rw iso_sub_trans_rw. sh (fun x => pair (tack_on (pr1 x) (pr1 x)) (pr2 x)). uhg; ee. uhg; ir. rwi inc_product H1. ee. assert (is_ordinal (pr1 x)). assert (ordinal_lt (pr1 x) z). rw ordinal_lt_rw. ee. rwi is_cardinal_rw H; ee; am. am. uh H4; ee. uh H4; ee; am. assert (is_ordinal (pr2 x)). assert (ordinal_lt (pr2 x) (R 2)). rw ordinal_lt_rw. ee. ap Naturals.nat_ordinal. am. uh H5; ee. uh H5; ee; am. rw inc_op_triangle. rw pr1_pair. rw pr2_pair. ee. uhg; ee. ap pair_is_pair. rw pr1_pair. ap ordinal_tack_on. am. rw pr2_pair. am. ap cardinality_lt_ordinal_lt. ap ordinal_tack_on. am. rwi is_cardinal_rw H; ee; am. apply by_cases with (is_finite (pr1 x)); ir. assert (is_finite (tack_on (pr1 x) (pr1 x))). ap finite_tack_on. am. rwi is_finite_inc_cardinality_nat H7. rwi is_infinite_sub_nat_cardinality H0. rw ordinal_lt_rw. ee. ap cardinality_ordinal. app H0. rw infinite_cardinality_tack_on. rwi is_cardinal_rw H. ee. ap H7. rw ordinal_lt_rw. ee. am. am. am. uhg; ee. am. ap ordinal_tack_on. am. uhg; ir. rwi inc_two H3. nin H3. rwi zero_emptyset H3. rwi H3 H6. nin H6. nin x1. rwi H3 H6. rwi inc_one H6. rw H6. assert (is_ordinal (R 0)). ap Naturals.nat_ordinal. cp (ordinal_lt_lt_eq_or H4 H7). nin H8. rwi ordinal_lt_rw H8. ee. rwi zero_emptyset H9. nin H9. nin x1. nin H8. rwi ordinal_lt_rw H8. ee. rw tack_on_inc; app or_introl. rw tack_on_inc. ap or_intror; sy; am. rwi is_cardinal_rw H; ee; am. uhg; ir. apply pair_extensionality. rwi inc_product H1; ee; am. rwi inc_product H2; ee; am. ap tack_on_injective. rwi inc_product H1. ee. assert (ordinal_lt (pr1 x) z). rw ordinal_lt_rw. ee. rwi is_cardinal_rw H; ee; am. am. uh H6; ee. uh H6; ee; am. rwi inc_product H2. ee. assert (ordinal_lt (pr1 y) z). rw ordinal_lt_rw. ee. rwi is_cardinal_rw H; ee; am. am. uh H6; ee. uh H6; ee; am. transitivity (pr1 (pair (tack_on (pr1 x) (pr1 x)) (pr2 x))). rww pr1_pair. rw H3. rww pr1_pair. transitivity (pr2 (pair (tack_on (pr1 x) (pr1 x)) (pr2 x))). rww pr2_pair. rw H3. rww pr2_pair. Qed. Lemma finite_ordinal_cardinal : forall x, is_ordinal x -> is_finite x -> is_cardinal x. Proof. ir. uhg. ap ordinal_leq_leq_eq. ap cardinality_smallest. am. ap are_isomorphic_refl. assert (is_ordinal (cardinality x)). ap cardinality_ordinal. cp (ordinal_lt_lt_eq_or H H1). nin H2. rw ordinal_leq_rw. app or_introl. nin H2. uh H2. ee. uh H2; ee. assert (iso_sub x (cardinality x)). uhg. sh (cardinality x). ee. ap card_isomorphic. uhg; ir; am. rwi iso_sub_trans_rw H6. nin H6. assert (Transformation.injective x x x0). uhg; ee. uhg; ir. uh H6; ee. uh H6. ap H5. au. uh H6; ee. am. uh H0. cp (H0 _ H7). assert (cardinality x = x). ap extensionality; uhg; ir. app H5. uh H8; ee. uh H10; ee. uh H12. cp (H12 _ H9). nin H13. ee. wr H14. uh H6; ee. uh H6. au. rw H9. ap ordinal_leq_refl. am. wr H2. app ordinal_leq_refl. Qed. Lemma ordinal_lt_finite_infinite : forall x y, is_ordinal x -> is_ordinal y -> is_finite x -> is_infinite y -> ordinal_lt x y. Proof. ir. assert (is_cardinal x). app finite_ordinal_cardinal. rwi is_finite_inc_cardinality_nat H1. rwi is_infinite_sub_nat_cardinality H2. assert (sub nat y). apply sub_trans with (cardinality y). am. assert (ordinal_leq (cardinality y) y). ap cardinality_smallest. am. ap are_isomorphic_refl. uh H4; ee; am. rw ordinal_lt_rw. ee. am. uh H3; ee. wr H3. app H4. Qed. Lemma dumb_sub_product : forall z, is_ordinal z -> is_infinite z -> sub (product z (R 2)) (product z z). Proof. ir. uhg; ir. rwi inc_product H1. ee. assert (is_finite (R 2)). assert (R 2 = tack_on (R 1) (R 1)). wr nat_succ_tack_on. trivial. rw H4. ap finite_tack_on. assert (R 1 = tack_on (R 0) (R 0)). wrr nat_succ_tack_on. rw H5. ap finite_tack_on. rw zero_emptyset. ap finite_emptyset. assert (ordinal_leq (R 2) z). assert (ordinal_lt (R 2) z). ap ordinal_lt_finite_infinite. ap Naturals.nat_ordinal. am. am. am. uh H5; ee; am. uh H5; ee. rw inc_product. ee. am. am. app H7. Qed. Definition lim_sprb z := sub_prod_reflexive_below (cardinality z) \/ sub_prod_reflexive z . Lemma cardinality_double : forall z, is_ordinal z -> is_infinite z -> lim_sprb z -> cardinality (product z (R 2)) = cardinality z. Proof. ir. uf lim_sprb. ap ordinal_leq_leq_eq. nin H1. cp (sprb_op_triangle_leq H1). ap ordinal_leq_trans. sh (cardinality (op_triangle (cardinality z))). ee. ap ordinal_leq_trans. sh (cardinality (product (cardinality z) (R 2))). ee. ap iso_sub_cardinal_leq. ap isomorphic_iso_sub. ap cartesian_product_isomorphic. ap card_isomorphic. ap are_isomorphic_refl. ap iso_sub_cardinal_leq. ap iso_sub_double_op_triangle. ap is_cardinal_cardinality. rww is_infinite_cardinality. am. assert (prod_reflexive z). app sub_prod_reflexive_prod_reflexive. uh H2. ap iso_sub_cardinal_leq. ap iso_sub_trans. sh (product z z). ee. ap sub_iso_sub. app dumb_sub_product. uhg. sh z. ee. app are_isomorphic_symm. uhg; ir; am. ap iso_sub_cardinal_leq. uhg. sh (product z (R 1)). ee. rw R_one_singleton_emptyset. app product_singleton_isomorphic. uhg; ir. rwi inc_product H2. rw inc_product; ee. am. am. rw Naturals.R_S_tack_on. rw tack_on_inc. app or_introl. Qed. Lemma cardinal_leq_image : forall z f, ordinal_leq (cardinality (Image.create z f)) (cardinality z). Proof. ir. ap iso_sub_cardinal_leq. rw iso_sub_trans_rw. sh (fun x => choose (fun y => (inc y z & f y = x))). uhg; ee. uhg; ir. set (p:= fun y : E => inc y z & f y = x). assert (p (choose p)). ap choose_pr. rwi Image.inc_rw H. am. uh H0. ee. am. uhg. intros x y H H0. set (px:= fun y0 : E => inc y0 z & f y0 = x). set (py:= fun y0 : E => inc y0 z & f y0 = y). assert (px (choose px)). rwi Image.inc_rw H. app choose_pr. assert (py (choose py)). rwi Image.inc_rw H0. app choose_pr. uh H1; uh H2; ee. ir. wr H4; wr H3. rww H5. Qed. Lemma cardinal_leq_iso_sub : forall a b, ordinal_leq (cardinality a) (cardinality b) -> iso_sub a b. Proof. ir. ap iso_sub_trans. sh (cardinality a). ee. ap isomorphic_iso_sub. ap card_isomorphic. ap iso_sub_trans. sh (cardinality b). ee. ap sub_iso_sub. uh H; ee; am. ap isomorphic_iso_sub. ap are_isomorphic_symm. ap card_isomorphic. Qed. Lemma ordinal_leq_cardinality_union2_double : forall a b z, ordinal_leq (cardinality a) (cardinality z) -> ordinal_leq (cardinality b) (cardinality z) -> ordinal_leq (cardinality (union2 a b)) (cardinality (product z (R 2))). Proof. ir. assert (iso_sub a z). app cardinal_leq_iso_sub. assert (iso_sub b z). app cardinal_leq_iso_sub. uh H1; uh H2; nin H1; nin H2; ee. set (y:= Z (product z (R 2)) (fun u => (inc (pr1 u) x & pr2 u = R 0) \/ (inc (pr1 u) x0 & pr2 u = R 1))). assert (yinc : forall v, inc v y = (is_pair v & ((inc (pr1 v) x & pr2 v = R 0) \/ (inc (pr1 v) x0 & pr2 v = R 1)))). ir. ap iff_eq; ir. ufi y H5. Ztac. rwi inc_product H6. ee; am. ee. uf y. ap Z_inc. rw inc_product. ee; try am. nin H6; ee. app H4. app H3. nin H6; ee. rw H7. rw Naturals.R_S_tack_on. rw tack_on_inc. ap or_introl. rw Naturals.R_S_tack_on. rw tack_on_inc. app or_intror. rw H7. assert (R 2 = tack_on (R 1) (R 1)). ap Naturals.R_S_tack_on. rw H8. rw tack_on_inc. app or_intror. am. assert (are_isomorphic x a). app are_isomorphic_symm. assert (are_isomorphic x0 b). app are_isomorphic_symm. rwi iso_trans_ex_rw H5. rwi iso_trans_ex_rw H6. nin H5; nin H6. set (f:= fun d => Y (pr2 d = R 0) (x1 (pr1 d)) (x2 (pr1 d))). assert (sub (union2 a b) (Image.create y f)). uhg; ir. rwi inc_union2_rw H7. nin H7. uh H5; ee. uh H8; ee. uh H10. cp (H10 _ H7). nin H11. ee. rw Image.inc_rw. sh (pair x4 (R 0)). ee. rw yinc. ee. ap pair_is_pair. ap or_introl. ee. rw pr1_pair. am. rww pr2_pair. uf f. rw Y_if_rw. rww pr1_pair. rww pr2_pair. uh H6; ee. uh H8; ee. uh H10; ee. cp (H10 _ H7). nin H11. ee. rw Image.inc_rw. sh (pair x4 (R 1)). ee. rw yinc. ee. ap pair_is_pair. ap or_intror. ee. rw pr1_pair. am. rww pr2_pair. uf f. rw Y_if_not_rw. rww pr1_pair. rw pr2_pair. uhg; ir. assert (1 = 0). app R_inj. discriminate H14. ap ordinal_leq_trans. sh (cardinality (Image.create y f)). ee. ap iso_sub_cardinal_leq. app sub_iso_sub. ap ordinal_leq_trans. sh (cardinality y). ee. ap cardinal_leq_image. ap iso_sub_cardinal_leq. ap sub_iso_sub. uhg; ir. ufi y H8. Ztac. Qed. Lemma lim_sprb_cardinal_union2 : forall a b z, lim_sprb z -> is_infinite z -> ordinal_leq (cardinality a) (cardinality z) -> ordinal_leq (cardinality b) (cardinality z) -> ordinal_leq (cardinality (union2 a b)) (cardinality z). Proof. ir. ap ordinal_leq_trans. sh (cardinality (product z (R 2))). ee. app ordinal_leq_cardinality_union2_double. ap ordinal_leq_trans. sh (cardinality (product (cardinality z) (R 2))). ee. ap iso_sub_cardinal_leq. ap isomorphic_iso_sub. ap cartesian_product_isomorphic. ap card_isomorphic. ap are_isomorphic_refl. set (k:= cardinality z). assert (is_cardinal k). uf k. ap is_cardinal_cardinality. assert (is_infinite k). uf k. rww is_infinite_cardinality. ap ordinal_leq_trans; sh (cardinality k). ee. ap ordinal_leq_trans; sh (cardinality (op_triangle k)); ee. ap iso_sub_cardinal_leq. ap iso_sub_double_op_triangle. am. am. cp H3. uh H5. rw H5. ap sprb_op_triangle_leq. uh H. nin H. am. uhg. ee. am. am. ir. apply sub_prod_reflexive_invariant with z. ap iso_sub_trans. sh k. ee. ap sub_iso_sub. uh H6; ee. uh H6; ee; am. ap isomorphic_iso_sub. ap are_isomorphic_symm. uf k. ap card_isomorphic. am. uf k. ap iso_sub_cardinal_leq. ap isomorphic_iso_sub. ap are_isomorphic_symm. ap card_isomorphic. Qed. Definition reflect_pair x := pair (pr2 x) (pr1 x). Definition reflected_op_triangle z := Image.create (op_triangle z) reflect_pair. Lemma cardinal_leq_reflected_op_triangle : forall z, ordinal_leq (cardinality (reflected_op_triangle z)) (cardinality (op_triangle z)). Proof. ir. uf reflected_op_triangle. ap cardinal_leq_image. Qed. Lemma inc_ordinal_prod_itself_or : forall z x, is_ordinal z -> inc x (product z z) = (inc x (op_triangle z) \/ inc x (reflected_op_triangle z)). Proof. ir. ap iff_eq; ir. rwi inc_product H0. ee. assert (is_ordinal (pr1 x)). apply ordinal_inc_ordinal with z. am. am. assert (is_ordinal (pr2 x)). apply ordinal_inc_ordinal with z. am. am. cp (ordinal_lt_lt_eq_or H3 H4). nin H5. ap or_intror. uf reflected_op_triangle. rw Image.inc_rw. sh (pair (pr2 x) (pr1 x)). ee. rw inc_op_triangle. ee. uhg; ee. ap pair_is_pair. rww pr1_pair. rww pr2_pair. rw pr1_pair. rw ordinal_lt_rw. ee; am. rw pr2_pair. rw pr1_pair. uh H5; ee; am. am. uf reflect_pair. rw pr2_pair. rw pr1_pair. rwi is_pair_rw H0. sy; am. nin H5. ap or_introl. rw inc_op_triangle. ee. uhg; ee. am. am. am. rw ordinal_lt_rw; ee; am. uh H5; ee; am. am. ap or_introl. rw inc_op_triangle. ee. uhg; ee. am. am. am. rw ordinal_lt_rw; ee; am. rw ordinal_leq_rw. ap or_intror; ee; try am. sy; am. am. nin H0. rwi inc_op_triangle H0. ee. assert (ordinal_lt (pr2 x) z). ap ordinal_leq_lt_trans. sh (pr1 x). ee; am. rw inc_product. ee. uh H0; ee; am. rwi ordinal_lt_rw H1; ee; am. rwi ordinal_lt_rw H3; ee; am. am. ufi reflected_op_triangle H0. rwi Image.inc_rw H0. nin H0. ee. assert (is_pair x). wr H1. uf reflect_pair. ap pair_is_pair. assert (pr1 x = pr2 x0). wr H1. uf reflect_pair. rww pr1_pair. assert (pr2 x = pr1 x0). wr H1. uf reflect_pair. rww pr2_pair. rwi inc_op_triangle H0. ee. assert (ordinal_lt (pr2 x0) z). ap ordinal_leq_lt_trans. sh (pr1 x0). ee. am. am. rw inc_product. ee. am. rw H3. rwi ordinal_lt_rw H7; ee; am. rw H4. rwi ordinal_lt_rw H5; ee; am. am. Qed. Lemma ordinal_prod_itself_decomposition : forall z, is_ordinal z -> product z z = union2 (op_triangle z) (reflected_op_triangle z). Proof. ir. ap extensionality; uhg; ir. rwi inc_ordinal_prod_itself_or H0. rw inc_union2_rw. intuition. am. rwi inc_union2_rw H0. rw inc_ordinal_prod_itself_or. intuition. am. Qed. Lemma lim_sprb_cardinal_product : forall z, lim_sprb z -> is_infinite z -> ordinal_leq (cardinality (product z z)) (cardinality z). Proof. ir. set (k:= cardinality z). assert (is_cardinal k). uf k. ap is_cardinal_cardinality. ap ordinal_leq_trans. sh (cardinality (product k k)). ee. ap iso_sub_cardinal_leq. ap isomorphic_iso_sub. ap cartesian_product_isomorphic. uf k. ap card_isomorphic. uf k. ap card_isomorphic. assert (is_infinite k). uf k. rww is_infinite_cardinality. rw ordinal_prod_itself_decomposition. ap ordinal_leq_trans. sh (cardinality z). ee. ap lim_sprb_cardinal_union2. am. am. assert (cardinality z = k). tv. rw H3. ap sprb_op_triangle_leq. uh H. nin H. am. uhg. ee. am. am. ir. apply sub_prod_reflexive_invariant with z. ap iso_sub_trans. sh k. ee. ap sub_iso_sub. uh H4; ee. uh H4; ee; am. ap isomorphic_iso_sub. ap are_isomorphic_symm. uf k. ap card_isomorphic. am. ap ordinal_leq_trans. sh (cardinality (op_triangle k)). ee. ap cardinal_leq_reflected_op_triangle. assert (cardinality z = k). tv. rw H3. ap sprb_op_triangle_leq. uh H. nin H. am. uhg. ee. am. am. ir. apply sub_prod_reflexive_invariant with z. ap iso_sub_trans. sh k. ee. ap sub_iso_sub. uh H4; ee. uh H4; ee; am. ap isomorphic_iso_sub. ap are_isomorphic_symm. uf k. ap card_isomorphic. am. uf k. ap ordinal_leq_refl. ap cardinality_ordinal. rwi is_cardinal_rw H1. ee; am. Qed. Lemma lim_sprb_sub_prod_reflexive : forall z, lim_sprb z -> sub_prod_reflexive z. Proof. ir. uh H; nin H; try am. uh H; ee. cp H0. rwi is_infinite_cardinality H2. uhg; ir. assert (ordinal_leq (cardinality y) (cardinality z)). app sub_cardinal_leq. rwi ordinal_leq_rw H5. nin H5. cp (H1 _ H5). assert (prod_reflexive (cardinality y)). ap sub_prod_reflexive_prod_reflexive. rww is_infinite_cardinality. am. uh H7; uhg. ap are_isomorphic_trans. sh (cardinality y). ee. ap card_isomorphic. ap are_isomorphic_trans. sh (product (cardinality y) (cardinality y)). ee. am. ap cartesian_product_isomorphic. ap are_isomorphic_symm. ap card_isomorphic. ap are_isomorphic_symm. ap card_isomorphic. ee. assert (lim_sprb y). uhg. ap or_introl. rw H5. uhg; ee; am. cp (lim_sprb_cardinal_product H7 H4). assert (cardinality (product y y) = cardinality y). ap ordinal_leq_leq_eq. am. ap iso_sub_cardinal_leq. assert (nonempty y). ap excluded_middle. uhg; ir. uh H4. ap H4. assert (y = emptyset). ap extensionality; uhg; ir. assert False. ap H9. sh x. am. elim H11. nin H10. nin x0. rw H10. ap finite_emptyset. nin H9. uhg. sh (product y (singleton y0)). ee. ap product_singleton_isomorphic. uhg; ir. rwi inc_product H10; rw inc_product; ee; try am. cp (singleton_eq H12). rw H13. am. uhg. ap are_isomorphic_trans. sh (cardinality y); ee; try (ap card_isomorphic). wr H9. ap are_isomorphic_symm. ap card_isomorphic. Qed. Lemma ordinal_lt_leq_trans : forall x z, (exists y, ordinal_lt x y & ordinal_leq y z) -> ordinal_lt x z. Proof. ir. nin H. ee. rw ordinal_lt_rw. ee. uh H0; ee. am. uh H0; ee. ap H2. rwi ordinal_lt_rw H. ee; am. Qed. Lemma all_ordinals_sub_prod_reflexive : forall z, is_ordinal z -> sub_prod_reflexive z. Proof. ap excluded_middle. uhg; ir. assert (exists z, is_ordinal z & ~(sub_prod_reflexive z)). ap excluded_middle. uhg; ir. ap H. ir. ap excluded_middle. uhg; ir. ap H0. sh z; ee; am. nin H0. ee. set (p:= fun y => ~(sub_prod_reflexive y)). set (u:= sow p). assert (p u). uf u. ap sow_property. sh x; ee; am. ufi p H2. assert (lim_sprb u). uhg. ap or_introl. uhg. ee. ap is_cardinal_cardinality. uhg; uhg; ir. ap H2. uhg. ir. assert False. uh H5; ap H5. assert (is_finite u). ap finite_invariant. sh (cardinality u); ee. ap are_isomorphic_symm. ap card_isomorphic. am. ap subset_finite. sh u. ee. am. am. elim H6. ir. assert (ordinal_leq (cardinality u) u). ap iso_sub_ordinal_leq. uf u. ap sow_ordinal. ap sub_iso_sub. uhg; ir; am. assert (ordinal_lt y u). ap ordinal_lt_leq_trans. sh (cardinality u). ee; am. ap excluded_middle. uhg; ir. assert (ordinal_leq u y). uf u. ap sow_smallest. uh H5; ee; uh H5; ee; am. am. rwi ordinal_leq_rw H7. nin H7. exact (not_ordinal_lt_lt H5 H7). ee. rwi H7 H5. exact (not_ordinal_lt_refl H5). (** now we have finished showing [lim_sprb u] **) ap H2. ap lim_sprb_sub_prod_reflexive. am. Qed. Lemma all_sub_prod_reflexive : forall z, sub_prod_reflexive z. Proof. ir. apply sub_prod_reflexive_invariant with (cardinality z). ap isomorphic_iso_sub. ap card_isomorphic. ap all_ordinals_sub_prod_reflexive. ap cardinality_ordinal. Qed. Lemma are_isomorphic_product : forall z, is_infinite z -> are_isomorphic z (product z z). Proof. ir. change (prod_reflexive z). assert (sub_prod_reflexive z). ap all_sub_prod_reflexive. uh H0. ap H0. uhg; ir; am. am. Qed. Lemma cardinality_product_infinite : forall z, is_infinite z -> cardinality (product z z) = cardinality z. Proof. ir. ap cardinality_invariant. ap are_isomorphic_symm. ap are_isomorphic_product. am. Qed. Lemma cardinality_union2_infinite : forall a b z, is_infinite z -> ordinal_leq (cardinality a) (cardinality z) -> ordinal_leq (cardinality b) (cardinality z) -> ordinal_leq (cardinality (union2 a b)) (cardinality z). Proof. ir. app lim_sprb_cardinal_union2. uhg. ap or_intror. ap all_sub_prod_reflexive. Qed. Lemma iso_sub_union2 : forall a b z, is_infinite z -> iso_sub a z ->iso_sub b z -> iso_sub (union2 a b) z. Proof. ir. ap cardinal_leq_iso_sub. ap cardinality_union2_infinite. am. app iso_sub_cardinal_leq. app iso_sub_cardinal_leq. Qed. (** This finishes the properties of cardinal arithemetic for unions and products of infinite cardinals. We use Russell's paradox to show that powerset is strictly bigger. ***) Lemma russell : forall z, ~(iso_sub (powerset z) z). Proof. ir. uhg; ir. rwi iso_sub_trans_rw H. nin H. set (rp:= fun y => (exists s, sub s z & x s = y & ~(inc y s))). set (t:= Z z rp). set (v:= x t). assert (sub t z). uf t. uhg; ir; Ztac. assert (inc v z). uh H; ee. uh H. uf v. ap H. rww powerset_inc_rw. apply by_cases with (inc v t); ir. (** the case [inc v t] **) cp H2. ufi t H3. Ztac. uh H5. nin H5. ee. assert (x0 = t). uh H; ee. uh H8. ap H8. rww powerset_inc_rw. rww powerset_inc_rw. am. ap H7. rww H8. (** the case [~(inc v t)] **) ap H2. uf t. Ztac. uhg. sh t. ee. am. tv. am. Qed. Lemma cardinal_lt_powerset : forall z, ordinal_lt (cardinality z) (cardinality (powerset z)). Proof. ir. assert (is_ordinal (cardinality z)). ap cardinality_ordinal. assert (is_ordinal (cardinality (powerset z))). ap cardinality_ordinal. cp (ordinal_lt_lt_eq_or H H0). nin H1. am. assert (ordinal_leq (cardinality (powerset z)) (cardinality z)). rw ordinal_leq_rw. intuition. assert False. cp (russell (z:=z)). ap H3. ap cardinal_leq_iso_sub. am. elim H3. Qed. End Infinite.