Library set7

Theory of Sets EIII-3 Equipotents Sets. Cardinals





Require Export set2.

Require Export set3.

Require Export set4.

Require Export set5.

Require Export set6.




Set Implicit Arguments.



Import Correspondence.

Import Bfunction.

Import Border.

Import Worder.




Module Cardinal.

EIII-3-1 The cardinal of a set

Singletons are equipotent, as well as doubletons


Lemma singletons_equipotent: forall x y, 

  equipotent (singleton x) (singleton y).

Proof. ir. rw equipotentC.

  exists (fun _:singleton x => (Bo(singleton_inc y))). split. red. ir.

  ap R_inj. rw (singleton_eq (R_inc u)). rw (singleton_eq (R_inc v)). tv.

  red. ir. exists (Bo(singleton_inc x)). ap R_inj. rw B_eq.

  rww (singleton_eq (R_inc u)).

Qed.




Hint Resolve singletons_equipotent: fprops.

Lemma doubleton_equipotent1: forall x y x' y',

  x <> x' -> y <> y' -> equipotent (doubleton x x')(doubleton y y').

Proof. ir. rw equipotentC. assert (Ha:=doubleton_first x x').

  assert (Hb:=doubleton_second x x').

  assert (Hc:Bo Ha <> Bo Hb). red. ir. cp (f_equal (@Ro (doubleton x x')) H1).

  repeat rwi B_eq H2. contradiction.

  assert (forall a:doubleton x x',  inc (Yo (a= Bo Ha) y y') (doubleton y y')).

  ir. nin (p_or_not_p (a = Bo Ha)); ir; [rww Y_if_rw| rww Y_if_not_rw ]; fprops.

  exists (fun a:doubleton x x' =>  Bo (H1 a)).

  split.

  red. ir. cp (f_equal (@Ro (doubleton y y')) H2). rwi B_eq H3. rwi B_eq H3.

  ap R_inj. nin (doubleton_or (R_inc u)); nin (doubleton_or (R_inc v)). ue.

  assert (u= Bo Ha). app R_inj. rww B_eq. rwii Y_if_rw H3.

  assert (v= Bo Hb). app R_inj. rww B_eq. rwii Y_if_not_rw H3. contradiction.

  rw H7. int.

  assert (u= Bo Hb). app R_inj. rww B_eq. rwii Y_if_not_rw H3.

  assert (v= Bo Ha). app R_inj. rww B_eq. rwii Y_if_rw H3. elim H0. sy; am. ue.

  ue.

  red. ir. nin (doubleton_or (R_inc u)). exists (Bo Ha). ap R_inj. rw B_eq.

  rw Y_if_rw. sy; am. tv. exists (Bo Hb). ap R_inj. rw B_eq.

  rw Y_if_not_rw. sy; am. intuition.

Qed.

Equipotency is compatible with products


Lemma equipotent_productf:  forall I p1 p2,

  (forall i, inc i I -> equipotent (p1 i) (p2 i)) ->

  equipotent (productf I p1) (productf I p2).

Proof. ir. set (g:= fun i => choose (fun z => bijective z & source z = (p1 i)

  & target z = (p2 i))).

  assert (forall i, inc i I ->  (bijective (g i) & source (g i) = (p1 i)

    & target (g i) = (p2 i))). ir. uf g. app choose_pr. app (H _ H0).

  set (f:= fun i=> (graph (g i))). assert (ext_map_prod_axioms I p1 p2 f).

  red. ir. cp (H0 _ H1). nin H2. nin H3. nin H2; nin H2. nin H2.

  uf f. ee. fprops. sy; ue. wr H4. fprops.

  exists (ext_map_prod I p1 p2 f). split. split. app ext_map_prod_injective.

  ir. uf f. red. cp (H0 _ H2). nin H3. nin H3. nin H3.

  split. fprops. nin H3. nin H7. wr H8. app H6.

  app ext_map_prod_surjective. ir. uf f. cp (H0 _ H2). ee. wr H5.

  app surjective_pr3. nin H3; am. uf ext_map_prod. aw. au.

Qed.




Lemma equipotent_productb:  forall x y, fgraph x -> fgraph y ->

  domain x = domain y ->

  (forall i, inc i (domain x) -> equipotent (V i x) (V i y)) ->

  equipotent (productb x) (productb y).

Proof. ir. cp (equipotent_productf (fun i=> V i x) (fun i=> V i y) H2).

  ufi productf H3. rwi (L_recovers H) H3. rwi H1 H3. rwii (L_recovers H0) H3.

Qed.




Lemma equipotent_product: forall a b a' b',

  equipotent a a' -> equipotent b b' -> equipotent (product a b)(product a' b').

Proof. intros a b a' b'. repeat (rw equipotentC). ir. nin H; nin H0.

  exists (ext_to_prodC x x0). app (bijective_ext_to_prod2C H H0).

Qed.




Hint Resolve equipotent_product equipotent_productb: fprops.

Hint Resolve disjoint_union_disjoint: fprops.

commutativity asssociativity distributivity of product equipotency





Lemma equipotent_product_sym: forall a b,

  equipotent (product a b)(product b a).

Proof. ir. red. exists (inv_graph_canon (product a b)). split.

  app inv_graph_canon_bijective. fprops. uf inv_graph_canon. aw. au.

Qed.




Lemma product2associative : forall a b c,

  equipotent (product a (product b c)) (product (product a b) c).

Proof. ir. set (g:=fun z => J (J (P z) (P (Q z))) (Q (Q z))).

  exists (BL g (product a (product b c)) (product (product a b) c)). ee; aw.

  uf g. app bl_bijective.

  red. ir. awi H. ee. aw. eee.

  ir. set (pr1_def H1). set (pr1_def e). set (pr2_def e). set (pr2_def H1).

  awi H. awi H0. ee. app pair_extensionality. app pair_extensionality.

  ir. awi H. ee. exists (J (P (P y)) (J (Q (P y)) (Q y))). aw. eee.

Qed.




Lemma distrib_inter_prod2: forall a b c,

  product (union2 a b) c = union2 (product a c) (product b c).

Proof. ir. set_extens. awi H. ee.

  nin (union2_or H0); [app union2_first | app union2_second]; app product_inc.

  nin (union2_or H); awi H0; aw; ee; tv; inter2tac.

Qed.




Lemma distrib_inter_prod3: forall a b c,

  product c (union2 a b) = union2 (product c a) (product c b).

Proof. ir. set_extens. awi H. ee.

  nin (union2_or H1); [app union2_first | app union2_second]; app product_inc.

  nin (union2_or H); awi H0; aw; ee; tv; inter2tac.

Qed.




Lemma equipotent_a_times_singl: forall a b, 

  equipotent a (product a (singleton b)).

Proof. ir. red. exists (BL (fun x=> J x b) a (product a (singleton b))).

  ee. app bourbaki_ex5_17. aw. aw.

Qed.




Hint Resolve equipotent_a_times_singl: fprops.




Lemma equipotent_singl_times_a: forall a b, 

  equipotent a (product (singleton b) a).

Proof. ir. apply equipotent_transitive with (product a (singleton b)).

  fprops. app equipotent_product_sym.

Qed.

Properties of disjoint sets


Lemma disjoint_union2_pr0: forall a b x y,

  disjoint x y -> disjoint (product a x) (product b y).

Proof. ir. app disjoint_pr. ir. awi H0; awi H1. ee.

  ap (nondisjoint H5 H3 H).

Qed.




Lemma disjoint_union2_pr1: forall x y,

  x <> y -> disjoint (singleton x) (singleton y).

Proof. ir. app disjoint_pr. ir. elim H. awi H0; awi H1. ue.

Qed.




Lemma disjoint_union2_pr: forall a b x y,

  x <> y ->  disjoint (product a (singleton x)) (product b (singleton y)).

Proof. ir. app disjoint_union2_pr0. app disjoint_union2_pr1.

Qed.




Hint Resolve disjoint_union2_pr: fprops.




Lemma equipotent_disjoint_union: forall X Y,

  fgraph X -> fgraph Y ->  domain X = domain Y ->

  (forall i, inc i (domain X) -> equipotent (V i X) (V i Y)) ->

  mutually_disjoint X ->  mutually_disjoint Y ->

  equipotent (unionb X) (unionb Y).

Proof. ir. set (g:= fun i => choose (fun z => bijective z & source z = (V i X)

   & target z = (V i Y))).

  assert (forall i, inc i (domain X) -> (bijective (g i) & source (g i) = V i X

    & target (g i) = (V i Y))). ir. uf g. app choose_pr. app (H2 _ H5).

  assert (partition_fam X (unionb X)). red. intuition.

  set (h:= fun i => corresp (source (g i)) (unionb Y) (graph (g i))).

  assert (forall i, inc i (domain X)-> function_prop (h i) (V i X) (unionb Y)).

  ir. cp (H5 _ H7). red. uf h. aw. eee. nin H8. nin H8. app is_function_pr.

  fprops. nin H8. apw sub_trans (target (g i)). fprops. rw H10.

  red; ir. union_tac. ue. red in H8. ee. am.

  nin (extension_partition _ H6 H7). clear H9. nin H8. ee. red in H8. ee.

  assert (injective x). red. ee. am. ir. rwi H10 H12; rwi H10 H13.

  red in H3. ee. srwi H12. srwi H13. nin H12; nin H13. ee.

  assert (W x0 x = W x0 (g x1)). cp (H9 _ H12). red in H17. ee. rw H19.

  assert (inc x0 (source (h x1))). app H18. cp (H7 _ H12). nin H21.

  cp (W_pr3 H21 H20). assert (graph (g x1) = graph (h x1)). uf h. aw.

  wri H24 H23. sy. app W_pr. cp (H5 _ H12). ee. fct_tac. am.

  assert (W y x = W y (g x2)). cp (H9 _ H13). red in H18. ee. rw H20.

  assert (inc y (source (h x2))). app H19. cp (H7 _ H13). nin H22.

  cp (W_pr3 H22 H21). assert (graph (g x2) = graph (h x2)). uf h. aw.

  wri H25 H24. sy. app W_pr. cp (H5 _ H13). ee. fct_tac. am.

  assert (inc (W x0 x) (V x1 Y)). cp (H5 _ H12). ee. rw H17. wr H21.

  app inc_W_target. fct_tac. rw H20. am.

  assert (inc (W y x) (V x2 Y)). cp (H5 _ H13). ee. rw H18. wr H22.

  app inc_W_target. fct_tac. rw H21. am.

  red in H4. wri H1 H4. nin (H4 _ _ H12 H13). rwi H17 H14. rwi H18 H14.

  wri H21 H14. cp (H5 _ H12). ee. red in H22. ee. red in H22. ee.

  app H26. rww H23. rww H23. rww H21. red in H21.

  empty_tac1 (W x0 x). app intersection2_inc. rww H14.

  assert (surjective x). app surjective_pr6. ir.

  rwi H11 H13. nin (unionb_exists H13). ee. wri H1 H14. cp (H5 _ H14). ee.

  red in H16. ee. wri H18 H15. cp (surjective_pr H19 H15). nin H20. ee.

  assert (graph (g x0) = graph (h x0)). uf h. aw. rwi H22 H21.

  cp (H9 _ H14). red in H23. ee. exists x1. ee. rwi H17 H20. app H23. rw H25.

  app W_pr. nin (H7 _ H14). am. wrr H17. red. exists x. ee. red. ee; am. am. am.

Qed.




Lemma equipotent_disjoint_union1: forall X Y,

  fgraph X -> fgraph Y ->  domain X = domain Y ->

  (forall i, inc i (domain X) -> equipotent (V i X) (V i Y)) ->

  equipotent (disjoint_union X) (disjoint_union  Y).

Proof. ir. uf disjoint_union. app equipotent_disjoint_union.

  uf disjoint_union_fam. gprops. uf disjoint_union_fam. gprops.

  uf disjoint_union_fam. bw. ir. uf disjoint_union_fam.

  ufi disjoint_union_fam H3. bwi H3. bw. fprops. wrr H1. fprops. fprops.

Qed.




Lemma equipotent_disjoint_union2: forall a b a' b',

  disjoint a b -> disjoint a' b' -> equipotent a a' -> equipotent b b' ->

  equipotent (union2 a b) (union2 a' b').

Proof. assert (forall a b, union2 a b = unionb (variantLc a b)).

  ir. uf unionb. bw. wr two_points_pr2. rw union_of_twosets_aux.

  rww variant_V_ca. rww variant_V_cb.

  ir. rw H. rw H.

  assert (Ht:forall a b, disjoint a b ->  mutually_disjoint (variantLc a b)).

  ir. red. bw. ir. try_lvariant H5; try_lvariant H6; au; right; 

  app disjoint_symmetric.

  ap equipotent_disjoint_union ; fprops; bw; ir; try_lvariant H4.

Qed.




Definition doubleton_fam f a b :=

  exists x, exists y, x<>y & fgraph f &  domain f = doubleton x y &

    V x f = a &   V y f = b.




Lemma two_terms_bij: forall a b f, doubleton_fam f a b ->

  let F := (variantLc a b) in

  exists g, (bijective g & target g = domain F & fgraph F &

    f = gcompose F (graph g)).

Proof. ir. nin H. nin H. ee. assert (Hu: x0 <> x). int.

  set (gr := variantL x x0 TPa TPb).

  set (nf:= corresp (doubleton x x0) two_points gr).

  assert (fgraph gr). uf gr. fprops. assert (is_graph gr). nin H4. am.

  assert (range gr = two_points). uf gr. uf variantL. set_extens.

  rwi L_range_rw H6. nin H6. nin H6. wr H7. nin (doubleton_or H6); rw H8.

  rww variant_if_rw. fprops. rww variant_if_not_rw. fprops.

  rw L_range_rw. try_lvariant H6. exists x. eee. rww variant_if_rw.

  exists x0. eee. rww variant_if_not_rw.

  assert (doubleton x x0 = domain gr). uf gr. sy. ap variant_domain.

  assert (is_function nf). uf nf. app is_function_pr. rw H6. fprops.

  assert (bijective nf). red. ee. split. am. uf nf. uf W. aw. uf gr. ir.

  nin (doubleton_or H9); nin (doubleton_or H10); 

  rw H12; rw H13; rwi H12 H11; rwi H13 H11;tv; rwii variant_V_a H11; 

  rwii variant_V_b H11; elim two_points_distinct; au.

  app surjective_pr4. uf nf. aw.

  exists nf. ee. am. uf F. uf nf. aw. bw. uf F. fprops.

  assert (is_function nf). fct_tac. uf nf. aw.

  assert (fcomposable (variantLc a b) gr). red. eee. bw. fprops.

  rww alternate_compose. uf F.

  app fgraph_exten. app fcompose_fgraph. rw fcomposable_domain. ue. am.

  ir. rwi H1 H12. bw. uf gr. nin (doubleton_or H12); rw H13.

  rww variant_V_a. rww variant_V_ca. rww variant_V_b. rww variant_V_cb. ue.

Qed.




Ltac eqtrans u:= apply equipotent_transitive with u.

Ltac eqsym:= apply equipotent_symmetric.

Cardinals, zero two and one





Definition cardinal x := choose (fun z => equipotent x z).



Definition card_zero := emptyset.

Definition card_one := cardinal (singleton emptyset).

Definition card_two := cardinal two_points.




Definition is_cardinal x:= exists y, x = cardinal y.




Lemma cardinal_cardinal: forall x, is_cardinal (cardinal x).

Proof. ir. red. exists x. tv.

Qed.




Hint Resolve cardinal_cardinal: fprops.




Lemma cardinal_pr0: forall x, equipotent x (cardinal x).

Proof. ir. uf cardinal. app choose_pr. exists x. fprops.

Qed.




Lemma cardinal_pr: forall x, equipotent (cardinal x) x.

Proof. ir. eqsym. app cardinal_pr0.

Qed.




Hint Resolve cardinal_pr0 cardinal_pr: fprops.




Theorem cardinal_equipotent: forall x y,

   (cardinal x = cardinal y) = (equipotent x y).

Proof. ir. app iff_eq. ir. eqtrans (cardinal x). fprops. rw H. fprops.

  ir. uf cardinal. app choose_equiv. ir. split; ir. eqtrans x. eqsym. am. am.

  eqtrans y. am. am.

Qed.




Hint Rewrite cardinal_equipotent: aw.




Lemma cardinal_of_cardinal: forall x, is_cardinal x -> cardinal x = x.

Proof. ir. red in H. nin H. rw H. aw. fprops.

Qed.

Hint Resolve cardinal_of_cardinal: fprops.




Lemma cardinal_equipotent1: forall x y, is_cardinal x -> is_cardinal y ->

  equipotent x y -> x = y.

Proof. ir. wr (cardinal_of_cardinal H). wr (cardinal_of_cardinal H0). aw.

Qed.




Lemma equipotent_to_emptyset:

  forall x, equipotent x emptyset -> x = emptyset.

Proof. ir. nin H. nin H. nin H. nin H0. app is_emptyset.

  red. ir. wri H0 H3. red in H. ee. cp (inc_W_target H H3). rwi H2 H5.

  elim (emptyset_pr H5).

Qed.




Lemma cardinal_zero: cardinal emptyset = emptyset.

Proof. app equipotent_to_emptyset. ap (cardinal_pr emptyset).

Qed.




Lemma cardinal_nonemptyset: forall x,

  cardinal x = card_zero -> x = emptyset.

Proof. uf card_zero. ir. wri cardinal_zero H. awi H. app equipotent_to_emptyset.

Qed.




Lemma cardinal_emptyset: cardinal emptyset = card_zero.

Proof. app cardinal_zero. Qed.




Lemma zero_is_emptyset: card_zero = emptyset.

Proof. tv.

Qed.




Lemma cardinal_nonemptyset1: forall x,

  nonempty x -> cardinal x <> card_zero.

Proof. ir. red. ir. cp (cardinal_nonemptyset H0). nin H. rwi H1 H.

  elim (emptyset_pr H).

Qed.




Lemma cardinal0: is_cardinal card_zero.

Proof. uf card_zero. wr cardinal_zero. fprops. Qed.




Lemma cardinal1: is_cardinal card_one.

Proof. uf card_one. fprops. Qed.

Lemma cardinal2: is_cardinal card_two.

Proof. uf card_two. fprops. Qed.




Lemma cardinal_singleton: forall x, cardinal(singleton x) = card_one.

Proof. ir. uf card_one. aw. fprops.

Qed.




Lemma cardinal_one_is_singleton: is_singleton(card_one).

Proof. uf card_one.

  assert(equipotent (singleton emptyset) (cardinal (singleton emptyset))).

  fprops. nin H. ee. red.

  exists (W emptyset x). wr H1. set_extens. nin H.

  cp (surjective_pr2 H3 H2). nin H4. ee. wr H5. rwi H0 H4. db_tac.

  clear H1. db_tac. app inc_W_target. fct_tac. ue.

Qed.




Lemma cardinal_doubleton: forall x x',

  x <> x' ->  cardinal(doubleton  x x') = card_two.

Proof. ir. uf card_two. aw. wr two_points_pr2.

  app doubleton_equipotent1. fprops.

Qed.




Lemma set_of_card_two: forall x, cardinal x = card_two  ->

  exists u, exists v, u<>v & x = doubleton u v.

Proof. ir. ufi card_two H. symmetry in H. awi H. red in H. nin H. ee.

  exists (W TPb x0). exists (W TPa x0). ee.

  red. ir. red in H. ee. red in H. ee.

  assert (TPb= TPa). app H4. rw H0. fprops. rw H0. fprops.

  elim two_points_distinctb. am.

  wr H1. set_extens. red in H. ee.

  nin (surjective_pr2 H3 H2). ee. wr H5. rwi H0 H4.

  rwi two_points_pr H4. nin H4;  rw H4; fprops. nin H; nin H.

  nin (doubleton_or H2);  rw H5; app inc_W_target; rw H0; fprops.

Qed.




Lemma cardinal_two_is_doubleton: exists x, exists x',

  x <> x' &  card_two = doubleton  x x'.

Proof. app set_of_card_two. uf card_two. aw. fprops.

Qed.




Lemma card_one_not_zero: card_one <> card_zero.

Proof. ir. red. ir. ufi card_one H. set (cardinal_nonemptyset H). fprops.

Qed.




Lemma card_two_not_zero: card_two <> card_zero.

Proof. ir. red. ir. nin cardinal_two_is_doubleton. nin H0. nin H0.

  elim (emptyset_pr (x:=x)). ufi card_zero H. wr H. rw H1. fprops.

Qed.




Lemma card_one_not_two: card_one <> card_two.

Proof. ir. nin cardinal_one_is_singleton. rw H.

  nin cardinal_two_is_doubleton. nin H0. nin H0. rw H1.

  red. ir. assert (inc x0 (singleton x)). rw H2. fprops.

  assert (inc x1 (singleton x)). rw H2. fprops. elim H0. awi H3; awi H4. ue.

Qed.

EIII-3-2 Order relation between cardinals





Lemma inj_compose1: forall f f',

  injective f-> injective f' -> source f' = target f ->

  injective (compose f' f).

Proof. ir. app compose_injective. red. eee; fct_tac.

Qed.




Definition restriction_to_image f := 

  restriction2 f (source f) (image_of_fun f).




Lemma restriction_to_image_axioms: forall f, is_function f ->

  restriction2_axioms f (source f) (image_of_fun f).

Proof. ir. red. ee. am. fprops. red. ir. ap (sub_image_target1 H H0).

  uf image_of_fun. uf image_by_fun. fprops.

Qed.




Lemma restriction_to_image_surjective: forall f, is_function f ->

  surjective (restriction_to_image f).

Proof. ir. cp (restriction_to_image_axioms H).

  uf restriction_to_image. app restriction2_surjective.

Qed.




Lemma restriction_to_image_bijective: forall f, injective f ->

  bijective (restriction_to_image f).

Proof. ir. red. ee. uf restriction_to_image. app restriction2_injective.

  nin H. ap (restriction_to_image_axioms H).

  nin H. ap (restriction_to_image_surjective H).

Qed.

The order on cardinals





Definition equipotent_to_subset x y:= exists z, sub z y & equipotent x z.

Definition cardinal_le x y := 

  is_cardinal x & is_cardinal y &equipotent_to_subset x y.

Definition cardinal_lt a b := cardinal_le a b & a <> b.




Lemma cardinal_le1: forall x y,

  equipotent_to_subset x y = 

  (exists f, injective f & source f = x & target f = y).

Proof. ir. uf equipotent_to_subset. app iff_eq. ir. nin H. nin H. nin H0. ee.

  exists (compose  (canonical_injection x0 y) x1). ee; tv. app inj_compose1.

  nin H0; am. app ci_injective. uf canonical_injection. aw. sy;am.

  aw. aw. uf canonical_injection. aw.

  ir. nin H. ee. exists (image_of_fun x0). split. wr H1. app sub_image_target.

  nin H; am. exists (restriction_to_image x0). ee; tv.

  app restriction_to_image_bijective. uf restriction_to_image.

  uf restriction2. aw. uf restriction_to_image. uf restriction2. aw.

Qed.




Lemma cardinal_le2: forall x y,

  equipotent_to_subset x y =  equipotent_to_subset (cardinal x) (cardinal y).

Proof. ir. rw cardinal_le1. rw cardinal_le1.

  cp (cardinal_pr x). cp (cardinal_pr y).

  app iff_eq. nin H. cp (equipotent_symmetric H0). nin H1.

  ir. nin H2. ee. set (f1:= compose x2 x0). assert (injective f1). uf f1.

  app inj_compose1. red in H; ee; am. rww H8. exists (compose x1 f1). ee.

  app inj_compose1. red in H1; ee; am. uf f1. aw. rww H4. uf f1. aw. aw.

  cp (equipotent_symmetric H). nin H1. nin H0. ir. nin H2. ee.

  set (f1:= compose x2 x0). assert (injective f1). uf f1.

  app inj_compose1. red in H1; ee; am. rww H6. exists (compose x1 f1). ee.

  app inj_compose1. red in H0; ee; am. uf f1. aw. rww H4. uf f1. aw. aw.

Qed.




Lemma cardinal_le3: forall x y, 

  equipotent_to_subset x y = cardinal_le (cardinal x) (cardinal y).

Proof. ir. uf cardinal_le. wr cardinal_le2. app iff_eq. ir. ee;fprops.

  ir. ee;am.

Qed.




Lemma cardinal_le9: forall f, injective f ->

  cardinal_le (cardinal (source f)) (cardinal (target f)).

Proof. ir. red. ee. fprops. fprops. wr cardinal_le2. rw cardinal_le1.

  exists f. split. am. split; tv.

Qed.




Lemma cardinal_le_reflexive: forall x, is_cardinal x -> cardinal_le x x.

Proof. ir. red. ee. am. am. exists x. ee. fprops. fprops.

Qed.




Hint Resolve cardinal_le_reflexive: fprops.




Lemma cardinal_le5: forall E, (forall x, inc x E -> is_cardinal x) ->

  substrate (graph_on cardinal_le E) = E.

Proof. ir. app substrate_graph_on. ir. set (H _ H0). fprops.

Qed.




Hint Rewrite  cardinal_le1: aw.




Lemma cardinal_le7: forall a b c,

  equipotent b c -> equipotent_to_subset a b ->

  equipotent_to_subset a c.

Proof. ir. awi H0. aw. red in H. nin H; nin H0. ee. exists (compose x x0).

  ee. app inj_compose1. red in H. ee. am. rww H2. aw. aw.

Qed.




Lemma cardinal_le8: forall a b, sub a b -> equipotent_to_subset a b.

Proof. ir. red. exists a. ee. am. fprops. Qed.




Lemma sub_smaller: forall a b, 

  sub a b -> cardinal_le (cardinal a) (cardinal b).

Proof. ir. red. ee. fprops. fprops. wr cardinal_le2. app cardinal_le8.

Qed.

The ordering on cardinals is a well-ordering





Lemma cardinal_le_transitive: forall a b c,

  cardinal_le a b -> cardinal_le b c -> cardinal_le a c.

Proof. uf cardinal_le. ir. eee. awi H4. awi H2. aw. nin H4; nin H2. ee.

  exists (compose x0 x). ee. app inj_compose1. ue. aw. aw.

Qed.




Theorem wordering_cardinal_le: worder_r cardinal_le.

Proof. assert (forall E, (forall x, inc x E -> is_cardinal x) ->

    worder (graph_on cardinal_le E)). ir.

  nin (Zermelo (union E)). nin H0.

  assert (Ha: order x). nin H0; am.

  assert (Ht:forall f a b, 

    order_isomorphism f (induced_order x a) (induced_order x b) ->

    sub a (substrate x) -> sub b (substrate x) -> equipotent a b).

  ir. red in H2. ee. exists f. ee. am. wr H7. aw. wr H8. aw.

  set (iph:= fun r => Zo (set_of_segments x) (fun a => equipotent a r)).

  cp (set_of_segments_worder H0).

  set (io:= inclusion_suborder (set_of_segments x)) in *.

  assert (Hc: order io). nin H2; am.

  assert (He: forall a, inc a E -> sub (iph a) (substrate io)).

  ir. uf io. aw. uf iph. app Z_sub.

  set (phi:=fun r=> the_least_element(induced_order io (iph r))).

  assert (forall r, inc r E -> least_element(induced_order io (iph r)) (phi r)).

  ir. uf phi. cp (He _ H3). nin H2.

  app the_least_element_pr. fprops. assert (nonempty (iph r)).

  uf iph. assert (sub r (substrate x)). rw H1. app union_sub.

  destruct (isomorphic_subset_segment H0 H6) as [x0 [x1 [H7 H8]]].

  exists x0. Ztac. wrr inc_set_of_segments. eqsym. app (Ht _ _ _ H8). nin H7;am.

  app (H5 _ H4 H6).

  assert (Hb: forall a, inc a E -> inc (phi a) (iph a)).

  ir. cp (H3 _ H4). nin H5. ee. awi H5. am. am. app He.

  assert (Hv:forall a, inc a E -> equipotent (phi a) a). ir.

  cp (Hb _ H4). ufi iph H5. Ztac. am.

  assert (forall a b, (inc a E & inc b E & equipotent_to_subset a b)

    = ((inc a E & inc b E & sub (phi a) (phi b)))).

  ir. app iff_eq. ir. nin H4; nin H5. ee. am. am.

  assert (equipotent_to_subset a (phi b)). awi H6. aw. cp (Hv _ H5).

  cp (equipotent_symmetric H7). nin H8. nin H6. ee.

  exists (compose x0 x1). ee. nin H8. app inj_compose1. ue. aw. aw.

  nin H7. nin H7.

  cp (H3 _ H4). cp (H3 _ H5). red in H9; red in H10. ee. awi H9. awi H10.

  ufi iph H9. Ztac. clear H9. ufi iph H10. Ztac. clear H10.

  assert (is_segment x (phi a)). wri inc_set_of_segments H13. am. am.

  assert (is_segment x (phi b)). wri inc_set_of_segments H9. am. am.

  assert (Hg:sub (phi b) (substrate x)). app sub_segment1.

  assert (Hf:sub (phi a) (substrate x)). app sub_segment1.

  assert (worder (induced_order x (phi b))). app worder_restriction.

  assert (sub x0 (substrate (induced_order x (phi b)))). aw.

  cp (isomorphic_subset_segment H17 H18). nin H19. nin H19. nin H19.

  assert (sub x1 (phi b)). red in H19. nin H19. awi H19. am. am. am.

  wrii induced_trans H20. wrii induced_trans H20.

  assert (is_segment x x1). apply subsegment_is_segment with (phi b); am.

  assert (equipotent x0 x1). app (Ht _ _ _ H20).

  apply sub_trans with (phi b). am. am. nin H22; am.

  assert (equipotent x1 a). eqsym. eqtrans x0. am. am.

  assert (inc x1 (substrate (induced_order io (iph a)))). aw. uf iph. Ztac.

  wr inc_set_of_segments. am. am. app He.

  cp (H12 _ H25). ufi io H26. awi H26. ee.

  apply sub_trans with x1. am. am. app Hb. awi H25. am.

  am. app He. am. app He. am. app He.

  ir. ee. am. am. cp (Hv _ H4). cp (Hv _ H5).

  cp (equipotent_symmetric H7). nin H8. nin H9. cp (ci_injective H6). ee.

  set (f1:= compose (canonical_injection (phi a) (phi b)) x1).

  assert (injective f1). uf f1. app inj_compose1. red in H9; ee; am. aw.

  uf canonical_injection. aw. sy; am. rw cardinal_le1.

  exists (compose x0 f1). ee.

  app inj_compose1. red in H8; ee; am. uf f1. aw. uf canonical_injection. aw.

  uf f1. aw. uf f1. aw.

  assert (is_graph (graph_on cardinal_le E)). app graph_on_graph.

  assert (forall a b, related (graph_on cardinal_le E) a b =

    (inc a E & inc b E & sub (phi a) (phi b))).

  ir. rw graph_on_rw1. wr H4. uf cardinal_le. app iff_eq; ir; eee.

  assert (substrate (graph_on cardinal_le E) = E). app cardinal_le5.

  assert (order (graph_on cardinal_le E)). red. ee; split;tv.

  rw H7. ir. rw H6. eee. intros a b c. repeat rw H6. ir. eee.

  ap (sub_trans H13 H11). intros a b. rw H6; rw H6. ir. ee.

  wr (cardinal_of_cardinal (H _ H8)). wr (cardinal_of_cardinal (H _ H12)). aw.

  eqtrans (phi a). eqsym. app Hv. rw (extensionality H13 H11). app Hv.

  red. split. am. ir. rwi H7 H9. red in H2. ee.

  set(F:= fun_image x0 phi).

  assert (sub F (substrate io)). red. ir. ufi F H12. awi H12. nin H12.

  ee. wr H13. cp (H9 _ H12). app (He _ H14). app Hb.

  assert (nonempty F). nin H10. exists (phi y). uf F. aw. exists y. au.

  nin (H11 _  H12 H13). red in H14. awii H14. ee. ufi F H14. awi H14.

  nin H14. ee. exists x2. red. ee. aw. ue. ir. awi H17.

  assert (inc (phi x3) F). uf F. aw. ex_tac. cp (H15 _ H18).

  cp (related_induced_order1 H19). ufi io H20. awi H20. ee. aw. rw H6. ee.

  app H9. app H9. ue. am. ue.




  red. ee. red. ee. red. app cardinal_le_transitive.

  red. ir. set (E:= doubleton  x y).

  assert (forall x : Set, inc x E -> is_cardinal x). uf E. ir.

  nin (doubleton_or H2); red in H0; ee; ue. nin (H _ H2). ee.

  assert (related (graph_on cardinal_le E) x y). rw graph_on_rw1. uf E. eee.

  assert (related (graph_on cardinal_le E) y x). rw graph_on_rw1. uf E. eee.

  order_tac. red. ir. red in H0. eee.

  ir. assert (forall a, inc a x -> is_cardinal a). ir. cp (H0 _ H2).

  red in H3. ee. am. cp (H _ H2). nin H3. set (cardinal_le5 H2).

  assert (sub x (substrate (graph_on cardinal_le x))). rw e. fprops.

  cp (H4 _ H5 H1). nin H6. red in H6. awi H6. ee.

  exists x0. red. rw e. ee. am. ir. cp (H7 _ H8). awii H9. am. ue.

Qed.

The previous theorem implies antisymmetry( which can be proved without the axiom of choice), and other properties (two cardinals are comparable, this needs the axiom of choice).





Lemma cardinal_antisymmetry1: forall x y, 

  cardinal_le x y -> cardinal_le y x -> x = y.

Proof. ir. cp wordering_cardinal_le. red in H1. ee. red in H1. ee. red in H3.

  app H3.

Qed.




Lemma not_card_le_lt: forall a b, cardinal_le a b -> cardinal_lt b a -> False.

Proof. ir. nin H0. elim H1. app (cardinal_antisymmetry1).

Qed.




Lemma cardinal_antisymmetry2: forall a b, 

  equipotent_to_subset a b -> equipotent_to_subset b a ->

  equipotent a b.

Proof. ir. rwi cardinal_le2 H. rwi cardinal_le2 H0.

  assert (cardinal_le (cardinal a) (cardinal b)). red. eee.

  assert (cardinal_le (cardinal b) (cardinal a)). red. eee.

  wr cardinal_equipotent. app cardinal_antisymmetry1.

Qed.




Lemma cardinal_lt_le_trans: forall a b c,

  cardinal_lt a b -> cardinal_le b c -> cardinal_lt a c.

Proof. ir. red in H. ee. red. ee. ap (cardinal_le_transitive H H0).

  dneg. wri H2 H0. app cardinal_antisymmetry1.

Qed.




Lemma cardinal_le_lt_trans: forall a b c,

  cardinal_le a b -> cardinal_lt b c -> cardinal_lt a c.

Proof. ir. red in H0. ee. split. ap (cardinal_le_transitive H H0).

  dneg. rwi H2 H. app cardinal_antisymmetry1.

Qed.




Ltac co_tac := match goal with

  | Ha:cardinal_le ?a ?b, Hb: cardinal_le ?b ?c |- cardinal_le ?a ?c  

     =>  ap (cardinal_le_transitive Ha Hb)

  | Ha:cardinal_lt ?a ?b, Hb: cardinal_le ?b ?c |- cardinal_lt ?a ?c  

     =>  ap (cardinal_lt_le_trans Ha Hb)

  | Ha:cardinal_le ?a ?b, Hb: cardinal_lt ?b ?c |- cardinal_lt ?a ?c  

     =>  ap (cardinal_le_lt_trans Ha Hb)

  | Ha:cardinal_lt ?a ?b, Hb: cardinal_lt ?b ?c |- cardinal_lt ?a ?c  

     =>  nin Ha; co_tac

  | Ha: cardinal_le ?a ?b, Hb: cardinal_lt ?b ?a |- _ 

    => elim (not_card_le_lt Ha Hb)

  | Ha:cardinal_le ?x ?y, Hb:  cardinal_le ?y ?x |- _ 

   => solve [ rw (cardinal_antisymmetry1 Ha Hb) ; fprops ]

  | Ha: cardinal_le ?a _ |- is_cardinal ?a => nin Ha; am

  | Ha: cardinal_le  _ ?a |- is_cardinal ?a 

   => destruct Ha as [_ [Ha _ ]]; exact Ha

  | Ha: cardinal_lt ?a _ |- is_cardinal ?a => nin Ha; co_tac

  | Ha: cardinal_lt  _ ?a |- is_cardinal ?a => nin Ha; co_tac

end.




Lemma wordering_cardinal_le_pr : forall x,

  (forall a, inc a x -> is_cardinal a) ->

  (substrate (graph_on cardinal_le x) = x &

  worder (graph_on cardinal_le x)).

Proof. ir. ap wordering_pr. ap wordering_cardinal_le.

  ir. pose (H _ H0). fprops.

Qed.




Lemma cardinal_le_total_order: forall a b, 

  equipotent_to_subset a b \/ equipotent_to_subset b a.

Proof. ir. set (A:= cardinal a). set (B:= cardinal b).

  assert (is_cardinal A). uf A. fprops. assert (is_cardinal B). uf B. fprops.

  set (x:=doubleton A B).

  assert (forall u, inc u x -> is_cardinal u). ir. ufi x H1.

  nin (doubleton_or H1); rw H2; am.

  cp (wordering_cardinal_le_pr H1). ee. cp (worder_total H3).

  red in H4. ee. rwi H2 H5.

  assert (inc A x). uf x. fprops. assert (inc B x). uf x. fprops.

  cp (H5 _ _ H6 H7). ufi gge H8. nin H8. rwi graph_on_rw1 H8. left. ee.

  ufi A H10; ufi B H10. red in H10; ee. rww cardinal_le2. right.

  rwi graph_on_rw1 H8. ee. ufi A H10; ufi B H10. red in H10; ee.

  rww cardinal_le2.

Qed.




Lemma cardinal_le_total_order1: forall a b, 

  is_cardinal a -> is_cardinal b ->

  a = b \/ cardinal_lt a b \/ cardinal_lt b a.

Proof. ir. nin (equal_or_not a b). left. am. right.

  nin (cardinal_le_total_order a b). left. ee. red. ee. red. intuition. am.

  right. red. ee. red. intuition. intuition.

Qed.




Lemma cardinal_le_total_order2: forall a b, 

  is_cardinal a -> is_cardinal b ->

  cardinal_le a b \/ cardinal_lt b a.

Proof. ir. nin (cardinal_le_total_order1 H H0). rw H1. left. fprops.

  nin H1. nin H1. left. am. right. am.

Qed.




Lemma cardinal_le_total_order3: forall a b, 

  is_cardinal a -> is_cardinal b ->

  cardinal_le a b \/ cardinal_le b a.

Proof. ir. nin (cardinal_le_total_order2 H H0). left. am. nin H1. right. am.

Qed.

Properties of 0 and 1


Lemma zero_smallest: forall x, is_cardinal x -> cardinal_le card_zero  x.

Proof. ir. wr cardinal_emptyset. wrr cardinal_of_cardinal. app sub_smaller.

  app emptyset_sub_any.

Qed.




Lemma zero_smallest1: forall x, cardinal_lt x card_zero -> False.

Proof. ir. assert (is_cardinal x). co_tac. set (zero_smallest H0). co_tac.

Qed.




Lemma zero_smallest2: forall a, cardinal_le a card_zero -> a = card_zero.

Proof. ir. assert (is_cardinal a). co_tac. set (zero_smallest H0). co_tac.

Qed.




Lemma one_small_cardinal: forall x, is_cardinal x -> x <> card_zero ->

  cardinal_le card_one  x.

Proof. ir. red. ee. app cardinal1. am. rwi zero_is_emptyset H0.

  nin (emptyset_dichot x). contradiction.

  nin H1. exists (singleton y). ee. app sub_singleton.

  wr cardinal_equipotent. rw cardinal_singleton. uf card_one. fprops.

Qed.




Lemma one_small_cardinal1: forall x, cardinal_lt card_zero x ->

   cardinal_le card_one x.

Proof. ir. red in H. ee. app one_small_cardinal. co_tac. intuition.

Qed.




Lemma card_le_one_prop:forall E,

  cardinal_le card_one (cardinal E) -> nonempty E.

Proof. ir. red in H. ee. ufi card_one H1.

  wri cardinal_le2 H1. rwi cardinal_le1 H1. nin H1. ee. nin H1.

  exists (W emptyset x). wr H3. app inc_W_target. rw H2. fprops.

Qed.




Lemma card_le_one_prop1:forall E,

  nonempty E-> cardinal_le card_one (cardinal E).

Proof. ir. app one_small_cardinal. fprops. red. ir.

  elim (cardinal_nonemptyset1 H). am.

Qed.




Lemma card_le_two_prop: forall E,

  cardinal_le card_two (cardinal E) ->

  exists a, exists b, inc a E & inc b E & a <> b.

Proof. ir. red in H. ee. ufi card_two H1.

  wri cardinal_le2 H1. rwi cardinal_le1 H1. nin H1. ee. nin H1.

  assert (inc TPb  (source x)). rw H2. fprops.

  assert (inc TPa  (source x)). rw H2. fprops.

  exists  (W TPa x). exists  (W TPb x).

  ee. wr H3. fprops. wr H3. fprops. red. ir.

  cp (H4 _ _ H6 H5 H7). elim two_points_distinct. am.

Qed.




Lemma card_le_two_prop1:forall E x y,

  inc x E -> inc y E -> x <> y -> cardinal_le card_two (cardinal E).

Proof. ir. assert (sub (doubleton x y) E). red. ir.

  nin (doubleton_or H2); rww H3. wr (cardinal_doubleton H1).

  app sub_smaller.

Qed.

There is a set containing all cardinals less or equal a. Each family of cardinals has an upper bound





Definition set_of_cardinals_le a:= 

  fun_image(powerset a)(fun x => cardinal x).




Lemma set_of_cardinals_pr: forall a b,  is_cardinal a -> 

  inc b (set_of_cardinals_le a) = (cardinal_le b a).

Proof. ir. uf set_of_cardinals_le. app iff_eq. ir. awi H0. nin H0. nin H0.

  awi H0. cp (sub_smaller H0). wr H1. wrr (cardinal_of_cardinal H).

  ir. aw. red in H0. ee. red in H2.

  nin H2. ee. exists x. ee. aw. wri cardinal_equipotent H3. wr H3. fprops.

Qed.




Lemma cardinal_supremum: forall x,

  (forall a, inc a x -> is_cardinal a) ->

  exists_unique (fun b => is_cardinal b & 

    (forall a, inc a x -> cardinal_le a b) &

    (forall c, is_cardinal c ->  (forall a, inc a x -> cardinal_le a c) -> 

      cardinal_le b c)).

Proof. ir. set (E:= union x). set (b:= cardinal E).

  assert (Ha: is_cardinal b). uf b. fprops.

  assert (forall a, inc a x ->  cardinal_le a b). ir.

  assert (sub a E). uf E. app union_sub. cp (sub_smaller H1).

  rwi cardinal_of_cardinal H2. am. app H.

  set(f:=  set_of_cardinals_le b).

  assert (Ht: forall u, inc u f = cardinal_le u b). ir. uf f.

  rww set_of_cardinals_pr.

  assert (sub x f). red. ir. rw Ht. app H0.

  assert(forall a, inc a f -> is_cardinal a). ir. rwi Ht H2. co_tac.

  assert(forall a, inc a f -> cardinal_le a a). ir. fprops.

  cp wordering_cardinal_le. cp (wordering_pr H4 H3). ee.

  set (wo:= graph_on cardinal_le f) in *.

  assert (Hs:forall u v, gle wo u v =(inc u f & inc v f & cardinal_le u v)).

  ir. uf wo. rww graph_on_rw1.

  assert (inc b f). rww Ht. fprops.

  assert (sub x (substrate wo)). rw H5. am.

  assert (Hb:upper_bound wo x b). red. rw H5. split. am. ir. rw Hs. eee.

  assert (bounded_above wo x). red. exists b. am.

  cp (worder_hassup H6 H8 H9). nin H10.

  rwi least_upper_bound_pr H10. ee.

  red. ee. exists x0. red in H10. ee. rwi H5 H10. app H2.

  ir. cp (H12 _ H13). rwi Hs H14. ee; am.

  ir. cp (H11 _ Hb). rwi Hs H15. ee.

  nin (cardinal_le_total_order3 Ha H13). ee. co_tac. wri Ht H18.

  assert (upper_bound wo x c). red. ee. ue. ir. rw Hs. eee.

  cp (H11 _ H19). rwi Hs H20. eee.

  ir. ee. pose (H15 _ H12 H16). pose (H17 _ H13 H14). co_tac. nin H6; am. am.

Qed.




Theorem cardinal_supremum1: forall x,

  fgraph x ->

  (forall a, inc a (domain x) -> is_cardinal (V a x)) ->

  exists_unique (fun b => is_cardinal b & 

    (forall a, inc a (domain x) -> cardinal_le (V a x) b) &

    (forall c, is_cardinal c -> 

      (forall a, inc a (domain x) -> cardinal_le (V a x) c) -> 

      cardinal_le b c)).

Proof. ir. set (y:=range x). assert (forall a, inc a y -> is_cardinal a). ir.

  ufi y H1. srwi H1. nin H1. ee. rw H2. app H0. am.

  nin (cardinal_supremum H1). ee. clear H3. nin H2. red. ee. exists x0.

  ee. am. ir. app H3. uf y. app inc_V_range. ir. app H4. ir. ufi y H7.

  srwi H7. nin H7. ee. rw H8. app H6. am.

  ir. ee. cp (H8 _ H5 H9). cp (H10 _ H6 H7). co_tac.

Qed.




Lemma surjective_cardinal_le: forall x y,

  (exists z, surjective z & source z = x & target z = y) -> 

  cardinal_le (cardinal y) (cardinal x).

Proof. ir. wr cardinal_le3. nin H. ee. nin (exists_right_inv_from_surj H).

  cp (right_inverse_injective  H2).

  cp (source_right_inverse H2). rwi H1 H4. red in H2. ee.

  aw. exists x1. ee. am. am. red in H2. ee. wrr H7.

Qed.




Lemma image_smaller_cardinal: forall f, is_function f ->

  cardinal_le (cardinal (image_of_fun f))(cardinal (source f)).

Proof. ir. cp (restriction_to_image_surjective H).

  app surjective_cardinal_le. exists (restriction_to_image f). ee; tv.

  uf restriction_to_image. uf restriction2. aw.

  uf restriction_to_image. uf restriction2. aw.

Qed.

EIII-3-3 Operations on Cardinals


Definition cardinal_sum x := cardinal (disjoint_union x).

Definition cardinal_prod x := cardinal (productb x).




Theorem cardinal_prod_pr: forall x, fgraph x ->

  cardinal (productb x) = 

  cardinal_prod (L (domain x) (fun a => cardinal (V a x))).

Proof. ir. uf cardinal_prod. aw. app equipotent_productb. gprops. bw. ir.

  bw. fprops.

Qed.




Theorem cardinal_sum_pr: forall x, fgraph x ->

  cardinal (disjoint_union x) = 

  cardinal_sum (L (domain x) (fun a => cardinal (V a x))).

Proof. ir. uf cardinal_sum. aw.

  app equipotent_disjoint_union1. gprops. bw. ir. bw. fprops.

Qed.




Lemma cardinal_sum_pr3: forall X Y, fgraph X -> fgraph Y ->

  domain X = domain Y ->

  (forall i, inc i (domain X) -> cardinal (V i X) = cardinal (V i Y)) ->

  cardinal_sum X = cardinal_sum Y.

Proof. ir. cp (cardinal_sum_pr H). cp (cardinal_sum_pr H0).

  assert ( L (domain X) (fun a : Set => cardinal (V a X)) = 

    (L (domain Y) (fun a : Set => cardinal (V a Y)))).

  app L_exten1. rwi H5 H3. wri H3 H4. sy; am.

Qed.




Lemma cardinal_sum_pr1: forall x, fgraph x ->

  cardinal_le (cardinal (unionb x))

  (cardinal_sum (L (domain x) (fun a => cardinal (V a x)))).

Proof. ir. cp (disjoint_union_pr H). nin H0. ee.

  assert (cardinal_le (cardinal (unionb x)) (cardinal (disjoint_union x))).

  app surjective_cardinal_le. exists x0. intuition. wrr (cardinal_sum_pr H).

Qed.




Theorem cardinal_sum_commutative: forall X f, 

  fgraph X ->  target f = domain X -> bijective f -> 

  cardinal_sum X = cardinal_sum (gcompose X (graph f)).

Proof. ir. uf cardinal_sum. aw. uf disjoint_union.

  uf disjoint_union_fam. cp (bij_is_function H1).

  assert (range (graph f) = target f). nin H1. app surjective_pr3.

  assert (fcomposable X (graph f)). red. ee. am. fprops. wr H0. ue.

  rww alternate_compose. rww fcomposable_domain.

  assert (Hb:source f = domain (graph f)). aw. wr Hb.

  set (h := (L (domain X) (fun i  => product (V i X) (singleton i)))) in *.

  set (g:= L (source f)

    (fun i => product (V i (fcompose X (graph f))) (singleton (W i f)))).

  assert (fcomposable h (graph f)). uf h. red. eee. gprops. bw. wr H0. ue.

  assert (Ha: source  f = domain g). uf g. bw.

  assert (g = fcompose h  (graph f)). uf h. uf g. app fgraph_exten. gprops.

  app fcompose_fgraph. rw fcomposable_domain. bw. am. bw. ir. bw. ue.

  wr H0. change (inc (W x f) (target f)). fprops. ue.

  eqtrans (unionb g). rw H6. wr unionb_rewrite1; fprops. uf h. gprops.

  uf h. bw. ue. uf g. app equipotent_disjoint_union. gprops.

  gprops. bw. bw. ir. bw. fprops. wrr Hb.

  app mutually_disjoint_prop2. ir. awi H9. awi H10. ee. rwi H14 H12.

  red in H1; ee; red in H1; ee. app H16.

  app mutually_disjoint_prop2. ir. awi H9. awi H10. ee. ue.

Qed.




Theorem cardinal_prod_commutative: forall X f,  

  fgraph X -> target f = domain X ->  bijective f -> 

  cardinal_prod X = cardinal_prod (gcompose X (graph f)).

Proof. ir. uf cardinal_prod. aw. red.

  exists (product_compose X f). ee. app pc_bijective. uf product_compose. aw.

  uf  product_compose. aw. uf productf. uf gcompose. uf W.

  red in H1. ee. red in H1. ee. red in H1. ee. rww H5.

Qed.




Hint Resolve equipotent_prod_singleton: fprops.




Theorem cardinal_sum_assoc: forall f g,

  fgraph f  -> partition_fam g (domain f) ->

  cardinal_sum f  = cardinal_sum (L (domain g) (fun l => 

    cardinal_sum (restr f (V l g)))).

Proof. ir. uf cardinal_sum. cp H.

  set (h:=fun l => cardinal (disjoint_union (restr f (V l g)))).

  assert (Ha: forall i, inc i (domain g) -> (domain (restr f (V i g))= V i g)).

  ir. rww restr_domain1. red in H0. ee. wr H4. red. ir. union_tac.

  aw. uf disjoint_union. uf disjoint_union_fam.

  set (a:= unionb (L (domain f) (fun i  => product (V i f) (singleton i)))).

  assert (a= unionf (domain f) (fun i => product (V i f) (singleton i))).

  uf a. uf unionb. bw. app unionf_extensionality. ir. bw. red in H0. ee.

  ufi unionf  H4. symmetry in H4.

  rwi (union_assoc  (fun i : Set => product (V i f) (singleton i)) H4) H2.

  assert (a=unionb (L (domain g) (fun l  =>

    unionf (V l g) (fun i => product (V i f) (singleton i))))).

  uf unionb. rw H2. bw. app unionf_extensionality. ir. bw. rw H5.

  clear H2. clear H5. bw. app equipotent_disjoint_union. gprops. gprops. bw.

  bw. ir. bw.

  assert (unionf (V i g) (fun i0  => product (V i0 f) (singleton i0)) =

    (unionb (L (V i g) (fun i0  => product (V i0 f) (singleton i0))))).

  uf unionb. bw. app unionf_extensionality. ir. bw. rw H5. clear H5.

  eqtrans (h i). uf h. eqtrans  (disjoint_union (restr f (V i g))).

  uf disjoint_union. uf disjoint_union_fam. ap equipotent_disjoint_union.

  gprops. gprops. bw. sy. app Ha. bw. ir. bw. app equipotent_product.

  fprops. fprops. rw H4.

  red. ir. union_tac. rww Ha.

  app mutually_disjoint_prop2. ir. awi H7. awi H8. ee. ue.

  app mutually_disjoint_prop2. ir. awi H7. awi H8. ee. ue. fprops. fprops.

  app mutually_disjoint_prop2. ir.

  srwi H6. nin H6. srwi H7. nin H7. ee.

  awi H8; awi H9; ee. rwi H13 H11. wri H11 H7. red in H3. ee.

  cp (H3 _ _ H2 H5). nin H14. am. red in H14.

  empty_tac1 x. app intersection2_inc.

  app mutually_disjoint_prop2. ir. awi H6. awi H7. ee. ue.

Qed.




Theorem cardinal_prod_assoc: forall f g,

  fgraph f  -> partition_fam g (domain f) ->

  cardinal_prod f  = cardinal_prod (L (domain g) (fun l => 

    cardinal_prod (restr f (V l g)))).

Proof. ir. uf cardinal_prod. aw.

  eqtrans (productb

    (L (domain g) (fun l  =>  (productb (restr f (V l g)))))).

  red. exists (prod_assoc_map f g). split. app pam_bijective. red. au.

  uf prod_assoc_map; aw. au.

  app equipotent_productb; gprops; bw. ir. bw. fprops.

Qed.




Theorem cardinal_distrib_prod_sum: forall f,

  fgraph f ->

  (forall l, inc l (domain f) -> fgraph (V l f)) ->

  cardinal_prod (L (domain f) (fun l => cardinal_sum (V l f))) =

  cardinal_sum (L (productf (domain f) (fun l => (domain (V l f))))

    (fun g => (cardinal_prod (L (domain f) (fun l => V (V l g) (V l f)))))).

Proof. ir. uf cardinal_prod. uf cardinal_sum. aw.

  eqtrans (productf (domain f) (fun l =>  (disjoint_union (V l f)))).

  uf productf. app equipotent_productb; gprops; bw. ir. bw. fprops.

  uf disjoint_union.

  set (g:= L (domain f) (fun l => disjoint_union_fam (V l f))).

  assert (domain g = domain f). uf g. bw. assert (fgraph g). uf g. gprops.

  assert (Ha:forall l, inc l (domain g) -> fgraph (V l g)). ir. uf g. bw.

  uf disjoint_union_fam. gprops. wrr H1. wr H1.

  assert(productf (domain g)

    (fun l  => unionb (disjoint_union_fam (V l f))) = 

    productf (domain g) (fun l => unionb (V l g))). uf productf. app uneq.

  app L_exten1. ir. uf g. bw. ue. rw H3. clear H3.

  rww distrib_prod_union.

  assert (unionf (productf (domain g) (fun l : Set => domain (V l g)))

    (fun g0=> productf (domain g) (fun l : Set => V (V l g0) (V l g))) =

    (unionb (L (productf (domain g) (fun l : Set => domain (V l g)))

    (fun g0 => productf (domain g) (fun l : Set => V (V l g0) (V l g)))))).

  uf unionb. bw. app unionf_extensionality. bw. ir. bw. rw H3. clear H3.

  app  equipotent_disjoint_union. gprops. uf disjoint_union_fam. gprops. bw.

  uf disjoint_union_fam. bw. uf productf. app uneq. app L_exten1.

  ir. uf g. bw. uf disjoint_union_fam. bw. ue.

  bw. ir. assert (Hb:inc i (productf (domain g) (fun l => domain (V l f)))).

  aw. awi H3. eee. ufi g H5. ir. cp (H5 _ H6). bwi H7.

  ufi disjoint_union_fam H7. bwi H7. am. wr H1. ue.

  uf disjoint_union_fam. bw.

  eqtrans (cardinal (productb (L (domain g) (fun l  => V (V l i) (V l f))))).

  eqtrans (productb (L (domain g) (fun l  => V (V l i) (V l f)))).

  uf productf. app equipotent_productb; gprops; bw. ir. bw.

  uf g. uf disjoint_union_fam. bw. eqsym. fprops. awi Hb. ee. app H7. ue. ue.

  fprops. fprops.

  assert (forall i j y, inc i (productf (domain g) (fun l=> domain (V l g)))

    -> inc y (productf (domain g) (fun l : Set => V (V l i) (V l g))) ->

  inc j (domain g) ->  Q (V j y) = V j i). uf g. uf disjoint_union_fam.

  bw. ir. bwi H5. bwi H4. awi H4. ee. rwi H6 H7. cp (H7 _ H5). bwi H8.

  awi H8. eee. awi H3. ee. rwi H9 H10. cp (H10 _ H5). bwi H11. am. am. am.

  app mutually_disjoint_prop. bw. ir. ap (productf_exten H4 H5).

  ir. bwi H6. wr (H3 _ _ _ H4 H6 H8). bwi H7. wrr (H3 _ _ _ H5 H7 H8). am. am.

  app disjoint_union_disjoint. gprops.

Qed.

Poduct and sums of two cardinals


Definition card_plus a b :=

  cardinal_sum (variantLc a b).




Definition card_mult a b :=

  cardinal_prod (variantLc a b).




Lemma card_plus_is_cardinal:forall a b, is_cardinal (card_plus a b).

Proof. uf card_plus. uf cardinal_sum. fprops. Qed.




Lemma card_mult_is_cardinal:forall a b, is_cardinal (card_mult a b).

Proof. uf card_mult. uf cardinal_prod. fprops. Qed.




Hint Resolve card_plus_is_cardinal card_mult_is_cardinal: fprops.




Lemma card_plus_pr: forall a b f,

  doubleton_fam f a b ->  card_plus a b = cardinal_sum f.

Proof. ir. cp (two_terms_bij H). nin H0. ee. rw H3.

  ap (cardinal_sum_commutative H2 H1 H0).

Qed.




Lemma card_mult_pr: forall a b f,

  doubleton_fam f a b ->  card_mult a b = cardinal_prod f.

Proof. ir. cp (two_terms_bij H). nin H0. ee. rw H3.

  ap (cardinal_prod_commutative H2 H1 H0).

Qed.




Lemma card_commutative_aux: forall a b,

   doubleton_fam (variantLc b a) a b.

Proof. ir. red. exists TPb. exists TPa. ee; fprops. bw. rw doubleton_symm.

  rww two_points_pr2. bw. bw.

Qed.




Lemma card_plus_commutative: forall a b,

  card_plus a b = card_plus b a.

Proof. ir. rww (card_plus_pr (card_commutative_aux a b)).

Qed.




Lemma card_mult_commutative: forall a b,

  card_mult a b = card_mult b a.

Proof. ir. rww (card_mult_pr (card_commutative_aux a b)).

Qed.




Lemma doubleton_fam_canon: forall (f:EE),

  doubleton_fam (L two_points f) (f TPa) (f TPb).

Proof. ir. red. exists TPa. exists TPb. bw. eee.

  gprops. wrr two_points_pr2. fprops. fprops.

Qed.




Lemma card_plus_pr0: forall f,

  cardinal_sum (L two_points f) = card_plus (f TPa) (f TPb).

Proof. ir. sy. app card_plus_pr. app  doubleton_fam_canon.

Qed.




Lemma card_mult_pr0: forall f,

  cardinal_prod (L two_points f) = card_mult (f TPa) (f TPb).

Proof. ir. sy. app card_mult_pr. app  doubleton_fam_canon.

Qed.




Lemma disjoint_union2_pr3: forall a b  x y, y <> x -> 

  equipotent (card_plus a b) 

  (union2 (product a (singleton x)) (product b (singleton y))).

Proof. ir. wrr disjoint_union2_rw. uf card_plus. uf cardinal_sum.

  assert (forall z t, t <> z -> doubleton_fam (variantL z t a b) a b).

  red. ir. exists z. exists t. ee. intuition. fprops. rww variant_domain.

  rww variant_V_a. rww variant_V_b.

  eqtrans  (disjoint_union (variantL TPa TPb a b)). eqsym. fprops.

  set (card_plus_pr (H0 _ _ H)).

  rwi (card_plus_pr (H0 _ _ two_points_distinctb)) e.

  wrr cardinal_equipotent.

Qed.




Definition TPas := singleton TPa.

Definition TPbs := singleton TPb.




Lemma disjoint_union2_pr4: forall a b, 

  equipotent (card_plus a b)  (union2 (product a TPas) (product b TPbs)).

Proof. ir. uf card_plus. uf cardinal_sum. wrr disjoint_union2_rw1. fprops.

Qed.




Ltac eq_aux:= match goal with

   H: is_cardinal ?a |- cardinal ?b = ?a => wr (cardinal_of_cardinal H); aw

 | H: is_cardinal ?a |- ?a = cardinal ?b => wr (cardinal_of_cardinal H); aw

end.




Lemma card_plus_pr1: forall a b a' b',

  disjoint a b -> equipotent a a' -> equipotent b b' ->

  cardinal (union2 a b) = card_plus a' b'.

Proof. ir. cp (card_plus_is_cardinal a' b'). eq_aux.

  cp (disjoint_union2_pr4 a' b'). cp (equipotent_symmetric H3).

  assert (L two_points (fun i => product (V i (variantLc a' b')) (singleton i))

    = variantLc  (product a' TPas) (product b' TPbs)).

  ap fgraph_exten. gprops. fprops. bw. bw. ir. bw. try_lvariant H5.

  cp (disjoint_union2_pr a' b' two_points_distinct).

  assert (equipotent a (product a' TPas)). eqtrans a'. am. uf TPas. fprops.

  assert (equipotent b (product b' TPbs)). eqtrans b'. am. uf TPbs. fprops.

  cp (equipotent_disjoint_union2 H H6 H7 H8).

  eapply equipotent_transitive. eexact H9. am.

Qed.




Lemma cardinal_sum_pr2: forall a b a' b', equipotent a a' -> equipotent b b' ->

  card_plus a b = card_plus a' b'.

Proof. ir. app cardinal_equipotent1; try app card_plus_is_cardinal.

  cp  (disjoint_union2_pr4 a b). cp  (disjoint_union2_pr4 a' b').

  eapply equipotent_transitive. eexact H1. eqsym.

  eapply equipotent_transitive. eexact H2. uf TPas. uf TPbs.

  app equipotent_disjoint_union2. fprops. fprops. eqsym. fprops.

  eqsym. fprops.

Qed.




Lemma card_plus_pr2: forall a b a' b',

  cardinal a = cardinal a' -> cardinal b = cardinal b' ->

  card_plus a b = card_plus a' b'.

Proof. ir. awi H. awi H0. app cardinal_sum_pr2.

Qed.




Lemma card_mult_pr1:forall a b,

  card_mult a b = cardinal (product a b).

Proof. ir. uf card_mult. uf cardinal_prod. aw.

  replace (productb (variantLc a b)) with (product2 a b). eqsym.

  cp (product2_canon_bijective a b).

  exists (product2_canon a b). ee. am. uf product2_canon. aw.

  uf product2_canon. aw. uf product2. uf productf.

  uf variantLc. uf variantL. rww two_points_pr2.

Qed.




Lemma card_mult_pr2: forall a b a' b',

  cardinal a = cardinal a' -> cardinal b = cardinal b' ->

  card_mult a b = card_mult a' b'.

Proof. ir. rw card_mult_pr1. rw card_mult_pr1. aw.

  app equipotent_product. awi H. am. awi H0. am.

Qed.




Lemma nonempty_card_ge2: forall E,

  cardinal_le card_two (cardinal E) -> nonempty E.

Proof. ir. nin (emptyset_dichot E). rwi H0 H. rwi  cardinal_zero  H.

  assert (cardinal_le card_zero  card_two).

  exact (zero_smallest cardinal2). elim card_two_not_zero. co_tac. am.

Qed.




Lemma card_mult_associative: forall a b c,

  card_mult a (card_mult b c) = card_mult (card_mult a b) c.

Proof. ir. repeat (rw card_mult_pr1). aw. eqtrans (product a (product b c)).

  fprops. eqtrans (product (product a b) c).

  app product2associative. fprops.

Qed.




Lemma card_plus_associative: forall a b c, 

  card_plus a (card_plus b c) = card_plus (card_plus a b) c.

Proof. assert (forall u v w  a b c,  v <> u-> u <> w -> w <> v -> 

  card_plus a (card_plus b c) = 

  cardinal (union2 (product a (singleton u))

    (union2 (product b (singleton v)) (product c (singleton w))))).

  ir. cp (disjoint_union2_pr3 a (card_plus b c) H).

  cp (disjoint_union2_pr3 b c H1).

  assert (is_cardinal (card_plus a (card_plus b c))). fprops.

  eq_aux. eapply equipotent_transitive. eexact H2.

  app equipotent_disjoint_union2. app disjoint_union2_pr. intuition.

  app disjoint_pr. ir. awi H5. nin (union2_or H6); awi H7; ee. elim H. ue.

  elim H0. ue. fprops. eqtrans (card_plus b c). eqsym. fprops. am.

  ir. cp card_one_not_zero.

  assert (card_two <> card_one). cp card_one_not_two. intuition.

  assert (card_zero <> card_two). cp card_two_not_zero. intuition.

  wr (card_plus_commutative c (card_plus a b)).

  rw (H _ _ _ a b c  H0 H2 H1). rw (H _ _ _ c a b H2 H1 H0).

  app uneq. rw union2assoc. rww union2comm.

Qed.




Lemma equipotent_product1: forall a b c, 

  equipotent a b -> equipotent (product a c) (product b c).

Proof. ir. fprops. Qed.




Lemma cardinal_distrib_prod_sum3 : forall a b c,

  card_mult a (card_plus b c) =

  card_plus (card_mult a b) (card_mult a c).

Proof. assert (Hu: forall a b c,

  equipotent (product a (product b (singleton c)))

  (product (card_mult a b) (singleton c))).

  ir. eqtrans (product (product a b) (singleton c)). app product2associative.

  app equipotent_product1. rw card_mult_pr1. fprops.

  ir. rw card_mult_pr1. aw.

  assert (is_cardinal (card_plus (card_mult a b) (card_mult a c))). fprops.

  eq_aux.

  eqtrans (product a (union2 (product b TPas) (product c TPbs))).

  app equipotent_product. fprops. ap disjoint_union2_pr4.

  rw distrib_inter_prod3. uf TPas. uf TPbs.

  eqtrans (disjoint_union (variantLc (card_mult a b) (card_mult a c))).

  rw disjoint_union2_rw1. app equipotent_disjoint_union2.

  app disjoint_union2_pr0. app disjoint_union2_pr. fprops.

  ap disjoint_union2_pr. fprops.

  eqsym. rw disjoint_union2_rw1. ap disjoint_union2_pr4.

Qed.




Lemma cardinal_distrib_prod_sum2 : forall a b c,

  card_mult (card_plus b c) a =

  card_plus (card_mult b a) (card_mult c a).

Proof. ir. rewrite card_mult_commutative.

  rewrite (card_mult_commutative b a).

  rewrite (card_mult_commutative c a). ap cardinal_distrib_prod_sum3.

Qed.




Lemma distrib_prod2_sum: forall A f, 

  product A (unionb f) = unionb (L (domain f) (fun x => product A (V x f))).

Proof. ir. set_extens. awi H. ee. srwi H1. nin H1. ee.

  srw. bw. ex_tac. bw. aw. ee; am. srwi H.

  nin H. bwi H. ee. awi H0. ee. aw. ee. am. am. union_tac. ee; am.

Qed.




Lemma cardinal_distrib_prod2_sum: forall a f, is_cardinal a -> fgraph f ->

  card_mult a (cardinal_sum f) = 

  cardinal_sum (L (domain f) (fun i => (card_mult a (V i f)))).

Proof. ir. rw card_mult_pr1. uf cardinal_sum. aw.

  eqtrans (product a  (disjoint_union f)). fprops. uf disjoint_union.

  rw distrib_prod2_sum. uf disjoint_union_fam. bw.

  app equipotent_disjoint_union. gprops. gprops. bw. bw. ir. bw.

  eqtrans (product (product a (V i f)) (singleton i)).

  app product2associative. app equipotent_product1. rw card_mult_pr1.

  fprops. app mutually_disjoint_prop2. ir. bwi H3. bwi H4. awi H3. awi H4. ee.

  ue. am. am. app mutually_disjoint_prop2. ir. bwi H3. bwi H4.

  awi H3. awi H4. ee. ue. am. am.

Qed.

EIII-3-4 Properties of the cardinals 0 and 1





Lemma trivial_cardinal_sum: forall f, domain f = emptyset ->

  cardinal_sum f = card_zero.

Proof. ir. uf cardinal_sum. assert (disjoint_union f = emptyset).

  ap is_emptyset. ir. red. uf disjoint_union. uf disjoint_union_fam. ir.

  srwi H0. nin H0. nin H0. bwi H0. rwi H H0. elim (emptyset_pr H0).

  rww H0. app cardinal_zero.

Qed.




Lemma trivial_cardinal_prod: forall f, fgraph f -> domain f = emptyset ->

  cardinal_prod f = card_one.

Proof. ir. uf cardinal_prod. uf card_one. wr (L_recovers H). rw H0.

  rww product2_trivial.

Qed.




Lemma trivial_cardinal_sum1: forall x f, domain f = singleton x ->

  is_cardinal (V x f) -> cardinal_sum f =  V x f.

Proof. ir. uf cardinal_sum. uf disjoint_union. uf disjoint_union_fam.

  assert (cardinal (V x f) = V x f). app cardinal_of_cardinal. wr H1.

  aw. uf unionb. bw. rw H. rw unionf_singleton. bw. eqsym. fprops. fprops.

Qed.




Lemma trivial_cardinal_prod1: forall x f, fgraph f -> domain f = singleton x ->

  is_cardinal (V x f) -> cardinal_prod f =  V x f.

Proof. ir. uf cardinal_prod. assert (cardinal (V x f) = V x f). fprops.

  wr H2. aw. eqsym. exists (product1_canon (V x f) x).

  ee. app product1_canon_bijective. uf product1_canon. aw.

  uf product1_canon. aw. app product1_pr2.

Qed.




Theorem zero_unit_sum: forall f j,

  fgraph f -> sub j (domain f) ->

  (forall i, inc i (complement (domain f) j) -> (V i f) = card_zero) ->

  cardinal_sum f = cardinal_sum (restr f j).

Proof. uf cardinal_sum. ir. aw.

  assert (Ha: domain (restr f j) = j). rww restr_domain1.

  assert (disjoint_union f = disjoint_union (restr f j)).

  uf disjoint_union. uf disjoint_union_fam.

  set_extens; srwi H2; nin H2; nin H2; bwi H2; bwi H3.

  nin (inc_or_not x0 j). ir. srw. bw. rw Ha. ex_tac. bw.

  assert (inc x0 (complement (domain f) j)). srw. au.

  rwi (H1 _ H5) H3. awi H3. ee. elim (emptyset_pr H6). am.

  rwi Ha H2. srw. bw. exists x0. split. app H0. bw. app H0. am. am. ue.

  am. ue.

Qed.




Theorem one_unit_prod: forall f j,

  fgraph f -> sub j (domain f) ->

  (forall i, inc i (complement (domain f) j) -> (V i f) = card_one) ->

  cardinal_prod f = cardinal_prod (restr f j).

Proof. ir. uf cardinal_prod. ir. aw. exists (pr_j f j).

  split. app prj_bijective. ir. rw H1. app cardinal_one_is_singleton.

  am. uf pr_j. aw. au.

Qed.




Lemma zero_unit_sumr: forall a, is_cardinal a -> 

  card_plus a card_zero = a.

Proof. ir. app cardinal_equipotent1. fprops.

  assert (union2 (product a TPas) emptyset = product a TPas).

  set_extens. nin (union2_or H0). am. elim (emptyset_pr H1). inter2tac.

  cp (disjoint_union2_pr4 a card_zero). rwi empty_product1 H1. rwi H0 H1.

  eqtrans (product a TPas). am. uf TPas. eqsym. fprops.

Qed.




Lemma one_unit_prodr: forall a, is_cardinal a -> 

  card_mult a card_one = a.

Proof. ir. rw card_mult_pr1. eq_aux.

  eqsym. nin (cardinal_one_is_singleton). rw H0.

  eqtrans (cardinal a). fprops. fprops.

Qed.




Hint Rewrite zero_unit_sumr one_unit_prodr: aw.




Lemma zero_unit_suml: forall a, is_cardinal a -> 

  card_plus card_zero a = a.

Proof. ir. rw card_plus_commutative. aw.

Qed.




Lemma one_unit_prodl: forall a, is_cardinal a -> 

  card_mult card_one a = a.

Proof. ir. rw card_mult_commutative. aw.

Qed.




Hint Rewrite zero_unit_suml one_unit_prodl: aw.




Lemma zero_prod_absorbing: forall a, 

  card_mult a card_zero = card_zero.

Proof. ir. rw card_mult_pr1. rw zero_is_emptyset. aw.

  srw. rww cardinal_zero.

Qed.




Lemma zero_product_absorbing:  forall f,

  fgraph f ->  (exists i, inc i (domain f) & cardinal (V i f) = card_zero)

  -> cardinal_prod f = card_zero.

Proof. ir. uf cardinal_prod. nin H0. nin H0.

  assert(productb f = emptyset). app is_emptyset. ir. red. ir.

  awi H2. ee. rwi H3 H4. cp (H4 _ H0).

  rwi (cardinal_nonemptyset H1) H5. elim (emptyset_pr H5). am. rw H2.

  app cardinal_emptyset.

Qed.




Lemma trivial_card_plus: forall x a, is_cardinal a ->

  cardinal_sum (cst_graph (singleton x) a) = a.

Proof. ir. uf cst_graph. set (f:= (L (singleton x) (fun _ : Set => a))).

  assert (a = V x f). uf f. bw. fprops. rw H0. app trivial_cardinal_sum1.

  uf f. bw. wrr H0.

Qed.




Lemma sum_of_ones: forall b j, is_cardinal b -> equipotent b j ->

  cardinal_sum (cst_graph j card_one) = b.

Proof. ir. uf cardinal_sum. eq_aux. eqsym. eqtrans j. am.

  uf disjoint_union. uf disjoint_union_fam.

  assert (domain (cst_graph j card_one) = j). uf cst_graph. bw. rw H1.

  set (f:= L j  (fun i => product (V i (cst_graph j card_one))(singleton i))).

  assert (f= L j (fun i=> product card_one (singleton i))). uf f. uf cst_graph.

  app L_exten1. ir. bw.

  assert (unionb f = product card_one j). rw H2. set_extens. srwi H3.

  nin H3. bwi H3. ee. awi H4. ee. aw. eee. ee; am. srw. bw. awi H3. ee.

  exists (Q x). ee. am. bw. aw. eee. rw H3.

  nin (cardinal_one_is_singleton). rw H4. app equipotent_singl_times_a.

Qed.




Lemma sum_of_ones1: forall b,

   equipotent (cardinal_sum (cst_graph b card_one))  b.

Proof. ir. set (c:= cardinal b). assert (is_cardinal c). uf c. fprops.

  assert (equipotent c b). uf c. eqsym. fprops. rw (sum_of_ones H H0). am.

Qed.




Lemma sum_of_same: forall a b j, is_cardinal a -> is_cardinal b ->

  equipotent b j ->

  cardinal_sum (cst_graph j a) = card_mult a b.

Proof. ir. cp (sum_of_ones H0 H1). cp (f_equal (card_mult a) H2). wr H3.

  rw cardinal_distrib_prod2_sum. bw.

  assert (L j  (fun i =>  card_mult a (V i (cst_graph j card_one)))

    = (L j  (fun _ => a))). app L_exten1. ir.

  uf cst_graph. bw. aw. uf cst_graph. bw. ufi cst_graph H4. rww H4. am.

  uf cst_graph. gprops.

Qed.




Lemma sum_of_same1: forall a b, 

  cardinal_sum (cst_graph b a) = card_mult a b.

Proof. ir. replace  (cardinal_sum (cst_graph b a)) with

  (cardinal_sum (cst_graph b (cardinal a))).

  assert (equipotent (cardinal b) b). eqsym. fprops.

  rw (sum_of_same  (cardinal_cardinal a)  (cardinal_cardinal b) H).

  app card_mult_pr2. fprops. fprops.

  uf cardinal_sum. aw. uf cst_graph.

  ap equipotent_disjoint_union1; gprops; bw. ir. bw. fprops.

Qed.




Theorem zero_cardinal_product: forall f,

  fgraph f ->  (forall i, inc i (domain f) -> V i f <> card_zero) =

  (cardinal_prod f <> card_zero).

Proof. ir. app iff_eq. ir. uf cardinal_prod. ufi card_zero H0.

  assert (forall i, inc i (domain f) -> nonempty (V i f)). ir.

  cp (H0 _ H1). nin (emptyset_dichot (V i f)). elim H2. am. am.

  cp (product_nonempty H H1). app cardinal_nonemptyset1.

  ir. dneg. app zero_product_absorbing. ex_tac. rw H2. app cardinal_zero.

Qed.




Lemma zero_cardinal_product2: forall a b, a <> card_zero  -> b <> card_zero ->

  card_mult a b <> card_zero.

Proof. ir. uf card_mult. wr zero_cardinal_product. bw.

  ir. try_lvariant H1. fprops.

Qed.




Lemma disjoint_with_singleton: forall a b, 

  ~ (inc b a) -> disjoint a (singleton b).

Proof. ir. red. ap is_emptyset. ir. red. ir. nin (intersection2_both H0).

  awi H2. rwi H2 H1. contradiction.

Qed.




Theorem succ_injective: forall a b, is_cardinal a ->

  is_cardinal b -> card_plus a card_one = card_plus b card_one ->

  a = b.

Proof. ir. set (X:=card_plus a card_one).

  cp (disjoint_union2_pr4 a card_one).

  cp (disjoint_union2_pr4 b card_one). wri H1 H3.

  cp (equipotent_symmetric H2). cp (equipotent_symmetric H3).

  nin H4. nin H5. ee. set (A0:= image_by_fun x (product a TPas)).

  set (B0:= image_by_fun x0 (product b TPas)).

  nin cardinal_one_is_singleton. rwi H10 H8; rwi H10 H6.

  assert (forall c xx, bijective xx -> source xx =

    union2 (product c TPas) (product (singleton x1) TPbs) ->

    let w:= image_by_fun xx (product c TPas) in

      let v:= W (J x1 TPb) xx in

        (  ~(inc v w) &  target xx = union2 w (singleton v) & equipotent c w)).

  ir. cp (bij_is_function H11). uf v.

  assert (Hb:sub (product c TPas) (source xx)). rw H12. app union2sub_first.

  assert (Ha: inc (J x1 TPb) (source xx)). rw H12. app union2_second.

  uf TPbs. aw. ee; fprops.

  ee. red. ir. ufi w H14. awi H14. nin H14. ee. assert (x2 = J x1 TPb).

  nin H11. nin H11. app H17. rw H12. inter2tac. rwi H16 H14. awi H14. ee.

  ufi TPas H18. awi H18. elim two_points_distinctb. am. am. am.

  set_extens. nin H11. ee. nin (surjective_pr2 H15 H14). nin H16.

  rwi H12 H16. wr H17. nin (union2_or H16). ap union2_first. uf w. aw.

  ex_tac. ufi TPbs H18. awi H18. ee. assert (x3 = J x1 TPb).

  assert (J (P x3) (Q x3) = x3). aw. wr H21. ue. ue.

  rw H21. app union2_second. fprops. nin (union2_or H14). ufi w H15. awi H15.

  nin H15. ee. wr H16. app inc_W_target. rw H12. inter2tac. am. am. awi H15.

  rw H15. app inc_W_target.

  eqtrans (product c TPas). uf TPas. fprops.

  exists (restriction1 xx (product c TPas)). ee;tv. app restriction1_bijective.

  nin H11; am. uf restriction1. aw. uf restriction1. aw.

  cp (H11 _ _ H4 H8). simpl in H12. fold A0 in H12. ee.

  cp (H11 _ _ H5 H6). simpl in H15. fold B0 in H15. ee.

  assert (equipotent A0 B0). rwi H7 H16. wri H9 H16.

  nin (equal_or_not (W (J x1 TPb) x) (W (J x1 TPb) x0)).

  assert (A0 = B0). set_extens. assert (inc x2 (target x)). rw H13. inter2tac.

  rwi H16 H20. nin (union2_or H20). am. awi H21. elim H12. rw H18. wrr H21.

  assert (inc x2 (target x)). rw H16. inter2tac. rwi H13 H20.

  nin (union2_or H20). am. elim H15. wr H18. awi H21. wrr H21. ue.

  set (C0:= intersection2 A0 B0).

  assert (A0 = union2 C0 (singleton (W (J x1 TPb) x0))).

  set_extens. assert (inc x2 (target x)). rw H13. inter2tac. rwi H16 H20.

  nin (union2_or H20). app union2_first. uf C0. app intersection2_inc.

  inter2tac. nin (union2_or H19). ufi C0 H20. inter2tac. awi H20. rw H20.

  assert (inc (W (J x1 TPb) x0) (target x)). rw H16. app union2_second. fprops.

  rwi H13 H21. nin (union2_or H21). am. elim H18. rww (singleton_eq H22).

  assert (B0 = union2 C0 (singleton (W (J x1 TPb) x))).

  set_extens. assert (inc x2 (target x)). rw H16. inter2tac. rwi H13 H21.

  nin (union2_or H21). app union2_first. uf C0. app intersection2_inc.

  inter2tac. nin (union2_or H20). ufi C0 H21. inter2tac. rw (singleton_eq H21).

  assert (inc (W (J x1 TPb) x) (target x)). rw H13. app union2_second. fprops.

  rwi H16 H22. nin (union2_or H22). am. elim H18. rww (singleton_eq H23).

  rw H19. rw H20. ap equipotent_disjoint_union2.

  ap disjoint_with_singleton. red. ir. ufi C0 H21. elim H15. inter2tac.

  ap disjoint_with_singleton. red. ir. ufi C0 H21. elim H12. inter2tac. fprops.

  fprops. assert (equipotent a b). eqtrans A0. am. eqtrans B0. am. eqsym. am.

  wri cardinal_equipotent H19. rwi (cardinal_of_cardinal H) H19.

  rwi (cardinal_of_cardinal H0) H19. am.

Qed.

EIII-3-5 Exponentiation of cardinals





Definition card_pow a b := cardinal (set_of_functions b a).




Lemma card_pow_pr: forall a b a' b',

  equipotent a a' -> equipotent b b' ->

  card_pow a b = card_pow a' b'.

Proof. ir. uf card_pow. aw. cp (equipotent_symmetric H0).

  nin H; nin H1. ee. red. exists (compose3function x0 x). split.

  app c3f_bijective. uf compose3function. aw. split; ue; ue.

Qed.




Theorem card_pow_pr1: forall x y, 

  cardinal (set_of_functions y x) = card_pow (cardinal x) (cardinal y).

Proof. ir. replace (cardinal (set_of_functions y x)) with (card_pow x y).

  ap card_pow_pr. fprops. fprops. tv.

Qed.




Lemma card_pow_pr2: forall a b,  

  cardinal_prod (cst_graph b a) = card_pow a b.

Proof. ir. uf card_pow. uf cardinal_prod. aw. uf cst_graph.

  set (f:=L b (fun _ : Set => a)). rw (product_eq_graphset (f:=f) (x:=a)).

  uf f. bw. eqsym. app set_of_functions_equipotent. uf f. gprops.

  uf f. bw. ir. bw.

Qed.




Theorem card_pow_pr3: forall a b j,  cardinal j = b->

  cardinal_prod (cst_graph j a) = card_pow a b.

Proof. ir. transitivity  (card_pow a j). ap  card_pow_pr2.

  app card_pow_pr. fprops. wr H. fprops.

Qed.




Lemma power_of_sum: forall a f, fgraph f ->

  card_pow a (cardinal_sum f) = 

  cardinal_prod (L (domain f) (fun i => card_pow a (V i f))).

Proof. ir. transitivity (card_pow a (disjoint_union f)).

  ap card_pow_pr. fprops. uf cardinal_sum. eqsym. fprops.

  wr card_pow_pr2. uf disjoint_union. set (S:= disjoint_union_fam f).

  set (f0:= cst_graph (unionb S) a).

  assert (fgraph f0). uf f0. uf cst_graph. gprops.

  assert (partition_fam S (domain f0)). cp (partion_union_disjoint H). uf f0.

  uf cst_graph. bw. rw (cardinal_prod_assoc H0 H1). uf S.

  uf disjoint_union_fam. bw. ap uneq.

  app L_exten1. ir. bw.

  replace (restr f0 (product (V x f) (singleton x))) with

    (cst_graph (product (V x f) (singleton x)) a). rw card_pow_pr2.

  ap card_pow_pr. fprops. eqsym. fprops.

  uf cst_graph. set (D:= product (V x f) (singleton x)).

  assert (sub D (unionb S)). red. uf D. ir. uf S. ee.

  uf disjoint_union_fam. srw. bw. ex_tac. bw.

  assert (domain (restr f0 D) = D). uf f0. uf cst_graph. rww restr_domain1.

  bw. sy. app fgraph_exten. fprops. gprops. bw. rw H4. ir. uf f0.

  uf cst_graph. bw. app H3.

Qed.




Lemma power_of_prod: forall b f, fgraph f ->

  card_pow (cardinal_prod f) b = 

  cardinal_prod (L (domain f) (fun i => card_pow (V i f) b)).

Proof. ir. wr card_pow_pr2.

  assert (Ha: is_graph f). red in H; ee; am.

  set(g:= L(product (domain f) b)(fun z=>  V (P z) f)).

  assert (fgraph g). uf g. gprops.

  set (h0:= L (domain f) (fun i => product (singleton i) b)).

  assert (partition_fam h0 (domain g)). red. uf h0. ee.

  gprops. app mutually_disjoint_prop2. ir. awi H3; awi H4. ee. ue.

  set_extens. srwi H1.

  nin H1. bwi H1. uf g. bw. nin H1. awi H2. ee. app product_inc. ue. ee; am.

  ufi g H1. bwi H1. awi H1. ee.

  apply unionb_inc with (P x). bw. aw. bw. aw. eee. aw. am.

  cp (cardinal_prod_assoc H0 H1).

  assert (domain h0 = domain f). uf h0. bw. rwi H3 H2. clear H3.

  assert (L (domain f) (fun l  => cardinal_prod (restr g (V l h0))) =

    L (domain f)  (fun i => card_pow (V i f) b)).

  app L_exten1. ir. uf h0. bw. set (T:= product (singleton x) b).

  assert (restr g T =  cst_graph T (V x f)). uf cst_graph.

  assert (sub T (product (domain f) b)). red; ir. ufi T H4. awi H4. ee.

  app product_inc. ue.

  assert(domain (restr g T) = T). rww restr_domain1. uf g. bw.

  ap fgraph_exten. fprops. gprops. bw. rw H5. ir. uf g. bw. ufi T H6. awi H6.

  ee. ue. app H4. rw H4. rw card_pow_pr2.

  app card_pow_pr. fprops. uf T. eqsym. app equipotent_singl_times_a.

  wr H3. wr H2. clear H2; clear H3.

  set (h:= L b (fun i => product (domain f) (singleton i))).

  assert (partition_fam h (domain g)). red. uf h. ee.

  gprops. app mutually_disjoint_prop2. ir. awi H4; awi H5. ee. ue. am. am.

  am. set_extens. srwi H2. nin H2.

  bwi H2. uf g. bw. nin H2. awi H3. ee. aw. ee. am. am. rww H5.

  am. ee;am. ufi g H2. bwi H2. awi H2. ee. apply unionb_inc with (Q x). bw.

  bw. aw. ee. am. am. fprops. am. cp (cardinal_prod_assoc H0 H2).

  assert (domain h = b). uf h. bw. rwi H4 H3.

  assert (L b (fun l  => cardinal_prod (restr g (V l h)))=

    (cst_graph b (cardinal_prod f))). uf cst_graph. app L_exten1. ir.

  assert (restr g (V x h) = L (product (domain f) (singleton x)) 

    (fun z => V (P z) f)). uf h. bw. set (T:= product (domain f) (singleton x)).

  assert (sub T (product (domain f) b)). red. ir. ufi T H6. awi H6. ee.

  app product_inc. aw. ue. am. uf g. app fgraph_exten. fprops. gprops. bw.

  rww restr_domain1. bw. rww restr_domain1. ir. bw. app H6. bw. rw H6.

  set (ff:=BL (fun u=> J u x) (domain f) (product (domain f) (singleton x))).

  set (X :=L (product (domain f) (singleton x)) (fun z : Set => V (P z) f)).

  assert (fgraph X). uf X. gprops. assert (target ff = domain X).

  uf ff. uf X. aw. bw. assert (bijective ff). uf ff. app  bourbaki_ex5_17. aw.

  cp (cardinal_prod_commutative H7 H8 H9).

  assert (gcompose X (graph ff) = f). uf ff. uf X. app fgraph_exten.

  gprops. uf gcompose. gprops. uf gcompose. bw.

  cp (bij_is_function H9). red in H11. ee. ufi ff H13. wr H13. aw.

  tv. uf gcompose. fold ff. cp (bij_is_function H9). red in H11. ee. wr H13.

  bw. ir. bw. change (V (P (W x0 ff)) f = V x0 f). uf ff. rw bl_W.

  aw. red. ir. app product_pair_inc. fprops. ufi ff H14.

  rwi bl_source H14. am.

  change (inc (W x0 ff) (product (domain f) (singleton x))).

  uf ff. rw bl_W. app product_pair_inc. ufi ff H14.

  rwi bl_source H14. am. fprops. red. ir.

  app product_pair_inc. fprops. ufi ff H14. rwi bl_source H14. am.

  rwi H11 H10. am. wr H5. sy. am.

Qed.




Lemma power_of_sum2: forall a b c, 

  card_pow a (card_plus b c) = 

  card_mult (card_pow a b) (card_pow a c).

Proof. ir. uf card_plus. rw power_of_sum. sy. app card_mult_pr. bw.

  cp (doubleton_fam_canon (fun i  => card_pow a (V i (variantLc b c)))).

  simpl in H. bwi H. am. fprops.

Qed.




Lemma power_of_prod2: forall a b c, 

  card_pow (card_mult a b) c = 

  card_mult (card_pow a c) (card_pow b c).

Proof. ir. sy. set (x:= card_mult (card_pow a c) (card_pow b c)).

  uf card_mult. rw power_of_prod. bw. uf x. app card_mult_pr.

  cp (doubleton_fam_canon (fun i  => card_pow  (V i (variantLc a b)) c)).

  simpl in H. bwi H. am. fprops.

Qed.




Lemma power_of_prod3: forall a b c, 

  card_pow a (card_mult b c)  = 

  card_pow (card_pow a b) c.

Proof. ir. wr sum_of_same1. rw power_of_sum.

  wr card_pow_pr2. ap uneq. uf cst_graph. bw. app L_exten1. ir.

  bw. uf cst_graph. gprops.

Qed.




Lemma power_x_0: forall a, card_pow a card_zero =  card_one.

Proof. ir. set  emptyset_fgraph.

  wr (trivial_cardinal_sum  emptyset_domain).

  rww power_of_sum. app trivial_cardinal_prod. gprops. bw. ap emptyset_domain.

Qed.




Lemma power_0_0: card_pow card_zero card_zero =  card_one.

Proof. ap power_x_0. Qed.




Lemma power_x_1: forall a, is_cardinal a -> card_pow a card_one = a.

Proof. ir. wr card_pow_pr2. set (f:=L card_one (fun _  => a)).

  assert (fgraph f). uf f. gprops. cp cardinal_one_is_singleton.

  nin H1. assert (domain f = singleton x). uf f. bw.

  assert (V x f = a). uf f. bw. rw H1. fprops. uf cst_graph. fold f. wr H3.

  assert (is_cardinal (V x f)). rww H3.

  ap (trivial_cardinal_prod1 H0 H2 H4).

Qed.




Lemma power_1_x: forall a, card_pow  card_one  a = card_one.

Proof. ir. set emptyset_domain. set emptyset_fgraph.

  wr (trivial_cardinal_prod f e). rww power_of_prod. rw e. rww trivial_fgraph.

Qed.




Lemma power_0_x: forall a, a <> card_zero ->

  card_pow  card_zero  a = card_zero.

Proof. ir. uf card_pow. assert (set_of_functions a card_zero = emptyset).

  ap is_emptyset. ir. red. ir. awi H0. ee.

  ufi card_zero H2. ufi card_zero H.

  cp (empty_target_graph H0 H2). red in H0. ee. rwi H3 H5.

  rwi emptyset_domain H5. elim H. ue. rw H0. app cardinal_zero.

Qed.




Lemma card_two_pr: card_two = card_plus card_one card_one.

Proof. uf card_plus.

  assert (variantLc card_one card_one = L two_points (fun _ => card_one)).

  app fgraph_exten. fprops. gprops. bw. bw. ir. try_lvariant H.

  fprops. fprops. rw H. cp cardinal2.

  sy. assert (equipotent card_two two_points). uf card_two. fprops.

  ap (sum_of_ones H0 H1).

Qed.




Lemma power_x_2: forall a, is_cardinal a -> card_pow a card_two = card_mult a a.

Proof. ir. rw card_two_pr. rw power_of_sum2. rww power_x_1.

Qed.




Lemma card_powerset: forall X, 

  cardinal (powerset X) = card_pow card_two X.

Proof. set (a:=emptyset); set (b:= singleton emptyset). ir.

  assert (b <> a). uf b. uf a. fprops. wr (cardinal_doubleton H).

  set (d:= doubleton b a). transitivity (card_pow d X).

  uf card_pow. ir. aw. set (K:= (set_of_functions X d)).

  set (u:=BL (fun z => BL (fun y => Yo (inc y z) a b) X d) (powerset X) K).

  assert (source u = (powerset X)). uf u. aw.

  assert (target u = K). uf u. aw.

  assert (forall z, inc z (powerset X) -> transf_axioms (fun y 

    => Yo (inc y z) a b) X d). red. ir. uf d. nin (inc_or_not c z).

  rww Y_if_rw. fprops. rww Y_if_not_rw. fprops.

  assert (forall z, inc z (powerset X) -> 

    is_function (BL (fun y : Set => Yo (inc y z) a b) X d)). ir.

  ap bl_function. app H2.

  assert (transf_axioms (fun z =>  (BL (fun y  => 

    Yo (inc y z) a b) X d))  (powerset X) K). red. ir. uf K. aw. eee.

  assert (is_function u). uf u. app bl_function.

  set (v:= BL (fun z => inv_image_by_fun z (singleton a))  K (powerset X)).

  assert (source v = K). uf v. aw. assert (target v = powerset X). uf v. aw.

  assert (transf_axioms (fun z  => inv_image_by_fun z

    (singleton a)) K (powerset X)).

  red. ir. ap powerset_inc. ufi K H8. awi H8. ee.

  wr H9. uf inv_image_by_fun. ap sub_inv_im_source. am. rw H10.

  uf d. fprops. red. ir. rw (singleton_eq H11). fprops.

  assert (is_function v). uf v. app bl_function.

  assert (composable u v). red. ee. am. am. rww H7.

  assert (composable v u). red. ee. am. am. rww H1.

  assert (compose u v  = identity (source v)).

  ap function_exten. fct_tac. fprops. aw. aw. ue. aw. ir.

  rww identity_W. aw. rwi H6 H12. cp H12. uf u. aw. ufi K H12. awi H12. ee.

  sy. ap function_exten. am. ap bl_function. ap H2. aw.

  wr H14. uf inv_image_by_fun. uf v. bw. rw bl_W. uf inv_image_by_fun.

  ap sub_inv_im_source. am. rw H15. uf d. red. ir. rw (singleton_eq H16).

  fprops. am. am. aw. aw. ir. aw. rwi H14 H16.

  assert (inc (W x0 x) d). wr H15. app inc_W_target. ue. ufi d H17.

  nin (doubleton_or H17). rw Y_if_not_rw. am. red. ir. ufi v H19.

  rwi bl_W H19. ufi inv_image_by_fun H19.

  ufi  inv_image_by_fun  H19. awi H19. nin H19.

  ee. cp (W_pr H12 H20). elim H. wr H18. rw H21. awi H19. am. am. am.

  rw Y_if_rw. am. uf v. uf inv_image_by_fun. aw.

  exists a. ee. fprops. wr H18. ap W_pr3. am. rww H14. app H2.

  wr H7. app inc_W_target. ue. ue. cut (inc (W x v) (target v)). ir.

  rwi H7 H14. awi H14. am. app inc_W_target. ue.

  assert (compose v u = identity (source u)). app function_exten. fct_tac.

  fprops. aw. aw. ue. ir. awi H13. rww identity_W. aw. uf u. rwi H0 H13. aw.

  uf v. aw. uf inv_image_by_fun. set_extens. awi H14. nin H14. ee.

  set (vv:= (BL (fun y : Set => Yo (inc y x) a b) X d)).

  fold vv in H15. assert (is_function vv). uf vv. ap bl_function. app H2.

  cp (W_pr H16 H15). cp (inc_pr1graph_source H16 H15). ufi vv H17.

  nin (inc_or_not x0 x). tv. awi H17. ir. rwi Y_if_not_rw H17.

  elim H. rw H17. rw (singleton_eq H14). tv. am. ap H2. am. ufi vv H18.

  awi H18. am. aw. exists a. ee. fprops.

  uf BL. set (LL:= L X (fun y : Set => Yo (inc y x) a b)).

  assert (fgraph LL). uf LL. gprops. assert (inc x0 (domain LL)).

  cp (powerset_sub H13). uf LL. bw. app H16.

  assert (a = V x0 LL). uf LL. bw. rww  Y_if_rw. awi H13. app H13. rw H17. aw.

  app fdomain_pr1. uf K. aw. eee. awi H13. am.

  cp (bijective_from_compose H10 H11 H12 H13).

  exists u. eee.

  app card_pow_pr. fprops. fprops.

Qed.

EIII-3-6 Order relation and operations on cardinals





Theorem cardinal_le_when_complement: forall a b,

  is_cardinal a -> is_cardinal b ->

  (cardinal_le b a) = (exists c, is_cardinal c & card_plus b c = a).

Proof. ir. ap iff_eq. ir. red in H1. ee. red in H3. nin H3. ee.

  set (c:= cardinal (complement a x)). exists c. ee. uf c. fprops.

  assert (TPb <> TPa). fprops.

  cp (disjoint_union2_pr3 b c H5).

  assert (disjoint (product b TPas) (product c TPbs)). uf TPas; uf TPbs.

  app disjoint_union2_pr. intuition.

  assert (disjoint x (complement a x)). red. ir. app disjoint_complement.

  assert (equipotent (product b TPas) x). eqtrans b. eqsym. uf TPas. fprops. am.

  assert (equipotent (product c TPbs) (complement a x)). eqtrans c. eqsym.

  uf TPbs. fprops. uf c. eqsym. fprops.

  cp (equipotent_disjoint_union2 H7 H8 H9 H10).

  assert (union2 x (complement a x) = a). set_extens. nin (union2_or H12).

  app H3. ap (sub_complement H13). nin (inc_or_not x0 x).

  ir. inter2tac. app union2_second. srw. ee; am.

  rwi H12 H11. wr (cardinal_of_cardinal H).

  assert (is_cardinal (card_plus b c)). uf card_plus.

  uf cardinal_sum. fprops. eq_aux.

  eapply equipotent_transitive. eexact H6. am.

  ir. nin H1. ee. assert (TPb <> TPa). fprops. cp (disjoint_union2_pr3 b x H3).

  rwi H2 H4. cp (equipotent_symmetric H4). nin H5. ee.

  set (f:=restriction x0 (product b TPas)).

  assert (sub (product b TPas)  (source x0)).

  red. ir. rw H6. app union2_first. cp (bij_is_function H5).

  assert (source f = product b TPas). uf f. uf restriction. aw.

  assert (target f = a). uf f. uf restriction. aw.

  assert (is_function f). uf f. app restriction_function.

  assert (injective f). red. ee. am. ir. ufi f H15.

  rwi H10 H13; rwi H10 H14. rwi restriction_W H15. rwi restriction_W H15.

  red in H5. ee. red in H5. ee. app H17. app H8. app H8. am. am. am. am. am.

  am. assert (equipotent b (product b TPas)). uf TPas. fprops.

  red. ee. am. am. fprops. nin H14. ee. aw.

  exists (compose f x1). ee. app inj_compose1. red in H14; ee; am.

  rww H16. aw. aw.

Qed.




Theorem sum_increasing: forall f g,

  fgraph f -> fgraph g -> domain f = domain g -> 

  (forall x, inc x (domain f) -> cardinal_le (V x f) (V x g)) ->

  cardinal_le (cardinal_sum f) (cardinal_sum g).

Proof. ir. set (df:= domain f).

  set (h:=L df (fun x =>choose (fun z => sub z (V x g)&equipotent (V x f) z))).

  assert (forall x, inc x df -> (sub (V x h) (V x g) & 

    equipotent (V x f) (V x h))). ir. uf h. bw. app choose_pr.

  ufi df H3. cp (H2 _ H3). red in H4; ee; am.

  set (hh:= disjoint_union_fam h). set (ff:= disjoint_union_fam f).

  set (gg:= disjoint_union_fam g).

  assert (Ha:domain ff = df). uf ff. uf disjoint_union_fam. bw.

  assert (Hb:domain hh = df). uf hh. uf disjoint_union_fam. bw. uf h. bw.

  assert (fgraph ff). uf ff. uf disjoint_union_fam. gprops.

  assert (fgraph hh). uf hh. uf disjoint_union_fam. gprops.

  assert (domain ff = domain hh). rw Ha; rww Hb.

  assert (forall x, inc x (domain ff) -> equipotent (V x ff) (V x hh)).

  ir. uf ff; uf hh. uf disjoint_union_fam. bw. app equipotent_product1.

  rwi Ha H7. cp (H3 _ H7). ee; am. uf h. bw. wrr Ha. rwi Ha H7. am.

  assert (mutually_disjoint ff). uf ff. app disjoint_union_disjoint.

  assert (mutually_disjoint hh). uf hh. app disjoint_union_disjoint. uf h.

  gprops. cp (equipotent_disjoint_union H4 H5 H6 H7 H8 H9).

  assert (sub (unionb hh) (unionb gg)). red. uf  gg; uf hh.

  uf disjoint_union_fam. ir. srwi H11. nin H11. bwi H11. ee.

  ufi h H11. bwi H11. cp (H3 _ H11). ee. apply unionb_inc with x0. bw.

  wrr H1. bw. aw. awi H12. ee. am. app H13. am. wrr H1. ee. am.

  uf cardinal_sum. red. ee. fprops. fprops. wr cardinal_le2.

  uf disjoint_union. fold ff. fold gg. exists (unionb hh). ee; am.

Qed.




Theorem product_increasing: forall f g,

  fgraph f -> fgraph g -> domain f = domain g -> 

  (forall x, inc x (domain f) -> cardinal_le (V x f) (V x g)) ->

  cardinal_le (cardinal_prod f) (cardinal_prod g).

Proof. ir. set (df:= domain f).

  set (h:=L df (fun x =>choose (fun z => sub z (V x g)&equipotent (V x f) z))).

  assert (forall x, inc x df -> (sub (V x h) (V x g) & 

    equipotent (V x f) (V x h))). ir. uf h. bw. app choose_pr.

  ufi df H3. cp (H2 _ H3). red in H4; ee; am.

  assert (fgraph h). uf h. gprops. assert (sub (productb h) (productb g)).

  app productb_monotone1. uf h. bw. ir. ufi h H5. bwi H5. cp (H3 _ H5). ee; am.

  assert (equipotent (productb f) (productb h)). app equipotent_productb.

  uf h. bw. ir. cp (H3 _ H6). ee; am. uf cardinal_prod. red. ee. fprops.

  fprops. wr cardinal_le2. exists (productb h). ee; am.

Qed.




Lemma sum_increasing1: forall f j, fgraph f ->

  (forall x, inc x (domain f) -> is_cardinal (V x f)) ->

  sub j (domain f) -> cardinal_le (cardinal_sum (restr f j)) (cardinal_sum f).

Proof. ir.

  set (g:= L (domain f)  (fun z => Yo (inc z j) (V z f) card_zero)).

  assert (Ha: fgraph g). uf g. gprops.

  assert (Hb: domain g = domain f). uf g. bw.

  assert (cardinal_sum g = cardinal_sum (restr g j)). uf g.

  app zero_unit_sum. bw. bw. ir. srwi H2. ee. bw. rww Y_if_not_rw.

  assert (restr f j = restr g j). app fgraph_exten. fprops. fprops.

  rww restr_domain. rww restr_domain. ue.

  ir. rwi restr_domain H3. nin (intersection2_both H3). bw. bw. uf g. bw.

  rw Y_if_rw. tv. am. rww Hb. am.

  rw H3. wr H2. app sum_increasing. uf g. bw. ir. bw.

  nin (inc_or_not x j). ir. rww Y_if_rw. fprops.

  rww Y_if_not_rw. app zero_smallest. app H0.

Qed.




Lemma product_increasing1: forall f j, fgraph f ->

  (forall x, inc x (domain f) -> is_cardinal (V x f)) ->

  (forall x, inc x (domain f) -> V x f <> card_zero) ->

  sub j (domain f) -> cardinal_le (cardinal_prod (restr f j)) (cardinal_prod f).

Proof. ir.

  set (g:= L(domain f)  (fun z => Yo (inc z j) (V z f) card_one)).

  assert (Ha: fgraph g). uf g. gprops.

  assert (Hb: domain g = domain f). uf g. bw.

  assert (cardinal_prod g = cardinal_prod (restr g j)). uf g.

  app one_unit_prod. bw. bw. ir. srwi H3. ee. bw. rww Y_if_not_rw.

  assert (restr f j = restr g j). app fgraph_exten; fprops.

  rww restr_domain. rww restr_domain. rww Hb. ir.

  rwi restr_domain H4. nin (intersection2_both H4). bw. bw. uf g. bw.

  rww Y_if_rw. rww Hb. am. rw H4. wr H3.

  app product_increasing. uf g. bw. ir. bw.

  nin (inc_or_not x j). rww Y_if_rw. fprops.

  ir. rww Y_if_not_rw. app one_small_cardinal. app H0. app H1.

Qed.




Lemma sum_increasing2: forall a b a' b',

  cardinal_le a a' -> cardinal_le b b' -> 

  cardinal_le (card_plus a b)  (card_plus a' b').

Proof. ir. uf card_plus. app sum_increasing. fprops. fprops. bw. bw.

  ir. try_lvariant H1.

Qed.




Lemma product_increasing2: forall a b a' b',

  cardinal_le a a' -> cardinal_le b b' -> 

  cardinal_le (card_mult a b)  (card_mult a' b').

Proof. ir. uf card_mult. app product_increasing. fprops. fprops. bw. bw.

  ir. try_lvariant H1.

Qed.




Lemma sum_increasing3: forall a b, is_cardinal a ->is_cardinal b ->

  cardinal_le a (card_plus a b).

Proof. ir. set (x:= (card_plus a b)). wr (zero_unit_sumr H).

  uf x. app sum_increasing2. fprops. app zero_smallest.

Qed.




Lemma product_increasing3: forall a b, is_cardinal a ->is_cardinal b ->

  b <> card_zero ->

  cardinal_le a (card_mult a b).

Proof. ir. set (x:= (card_mult a b)). wr (one_unit_prodr H).

  uf x. app product_increasing2. fprops. app one_small_cardinal.

Qed.




Lemma power_increasing1: forall a b a' b',

  a <> card_zero -> cardinal_le a a' -> cardinal_le b b' ->

  cardinal_le (card_pow a b)  (card_pow a' b').

Proof. ir. apply cardinal_le_transitive with  (card_pow a' b).

  wr card_pow_pr2. wr card_pow_pr2. uf cst_graph.

  app product_increasing. gprops. gprops. bw. bw. ir. bw.

  red in H1. ee. red in H3. nin H3. ee.

  assert (Ha:fgraph (cst_graph b' a')). uf cst_graph. gprops.

  assert (Hb:fgraph (cst_graph x a')). uf cst_graph. gprops.

  assert (card_pow a' b = card_pow a' x). app card_pow_pr.

  fprops. rw H5. wr card_pow_pr2. wr card_pow_pr2. uf cst_graph.

  assert (L x (fun _  => a') = restr (L b' (fun _  => a')) x).

  app fgraph_exten. gprops. fprops. gprops.

  rw restr_domain1. bw. gprops. bw. bw. ir. bw. bw. app H3.

  rw H6. app product_increasing1. bw. ir. bw. red in H0; ee; am.

  bw. ir. bw. red. ir. rwi H8 H0. elim H. app cardinal_antisymmetry1.

  app zero_smallest. red in H0; ee; am. bw.

Qed.




Theorem cantor: forall a, is_cardinal a ->

  cardinal_lt a (card_pow card_two a).

Proof. ir. wr card_powerset. set (x:= cardinal (powerset a)).

  wr (cardinal_of_cardinal H). uf x. red. ee. red. ee. fprops. fprops.

  wr cardinal_le2. aw.

  exists (BL (fun x => singleton x) a (powerset a)). ee.

  app bl_injective. red. ir. aw. red. ir. rw (singleton_eq H1). am.

  ir. app singleton_inj. aw. aw.

  red. ir. awi H0. nin H0. ee.

  set (X:= Zo a (fun x => (~ inc x (W x x0)))). red in H0. ee.

  assert (inc X (target x0)). rw H2. aw. uf X. app Z_sub.

  nin (surjective_pr2 H3 H4). ee.

  assert (~ (inc x1 X)). red; ir. cp H7. ufi X H7. Ztac. clear H7.

  rwi H6 H10. contradiction. elim H7. uf X. Ztac. ue. ue.

Qed.




Lemma cantor_bis: ~ (exists a, forall x, is_cardinal x -> inc x a).

Proof. red. ir. nin H. set (s:= union x). set (e:= cardinal s).

  assert  (cardinal_le  (card_pow card_two e) e).

  set (w:= (card_pow card_two e)). assert (is_cardinal w). uf w.

  uf card_pow. fprops. assert (sub w s). uf s. app union_sub. app H.

  cp (cardinal_le8 H1). red. ee. am. uf e. fprops. wr (cardinal_of_cardinal H0).

  uf e. wr cardinal_le2. am. assert (is_cardinal e). uf e. fprops.

  cp (cantor H1). red in H2. ee. elim H3. co_tac.

Qed.




End Cardinal.

Export Cardinal.