(** * Theory of Sets : Ordinals
Copyright INRIA (2011-2013) Marelle Team (Jose Grimm).
*)
(* $Id: sset15.v,v 1.37 2016/05/18 14:54:53 grimm Exp $ *)
Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Require Export sset14.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Module Ordinals5.
Lemma infinite_power1 a b: \2c <=c a -> a <=c (\2c ^c b) -> infinite_c b ->
a ^c b = \2c ^c b.
Proof.
move=> le1 le2 ic.
have bb:= (cleR (proj1 ic)).
have ap:= nesym (proj2 (clt_leT clt_02 le1)).
move: (cpow_Mlele ap le2 bb)(cpow_Mlele card2_nz le1 bb).
rewrite - cpow_pow (csquare_inf ic).
apply: cleA.
Qed.
Lemma infinite_power1_a a b: \2c <=c a -> a <=c b -> infinite_c b ->
a ^c b = \2c ^c b.
Proof.
move => pa pb pc; apply: infinite_power1 => //.
exact: (cleT pb (proj1 (cantor (proj1 pc)))).
Qed.
Lemma infinite_power1_b x: infinite_c x -> x ^c x = \2c ^c x.
Proof.
move => ix; apply: infinite_power1_a => //.
apply: finite_le_infinite => //; apply /NatP; fprops.
exact (cleR (proj1 ix)).
Qed.
Lemma infinite_power1_c x: infinite_c x ->
(cnext x) ^c x = \2c ^c x.
Proof.
move=> ix; move:(ix) =>[cx _].
apply: infinite_power1 => //; last by apply: (cnext_pr3 cx).
exact: (cleT (finite_le_infinite finite_2 ix) (proj1 ((cnext_pr2 cx)))).
Qed.
Section Exercise3_3.
Variables f g :Set.
Hypothesis (fgf: fgraph f)(fgg: fgraph g).
Hypothesis sd: domain f = domain g.
Hypothesis hg: (forall i, inc i (domain g) -> \2c <=c (Vg g i)).
Lemma compare_sum_prod1: (csum g) <=c (cprod g).
Proof.
case: (emptyset_dichot (domain g)) => dge.
rewrite csum_trivial // cprod_trivial //; fprops.
move: dge => [i idg].
case: (equal_or_not (domain g) (singleton i)) => dgs.
have c1: cardinalp (Vg g i) by move: (hg idg) => [_ le1 _].
rewrite (csum_trivial2 dgs c1) (cprod_trivial1 dgs) (card_card c1); fprops.
pose h j := choose (fun z => [/\ (inc (P z) (Vg g j)), (inc (Q z) (Vg g j))
& P z <> Q z]).
have gp: forall j, inc j (domain g) ->
[/\ inc (P (h j)) (Vg g j), (inc (Q (h j)) (Vg g j)) & P (h j) <> Q (h j)].
move=> j jdf; apply choose_pr.
have aux:=(hg jdf).
move: (aux); rewrite - {1} (card_card (proj32 aux)).
move/cle2P => [a [b [ae be ab]]].
exists (J a b); aw;split => //.
rewrite /cprod /csum.
set Pr := (productb g); set (Sr := (disjointU g)).
suff [h2 [hp6 hp8]]: exists h2,
( (forall j x, inc j (domain g) -> inc x (Vg g j) -> inc (h2 j x) Pr)
/\ (forall j k x y, inc j (domain g) ->inc k (domain g) ->
h2 j x = h2 k y -> (x = y /\ j = k))).
set hh:= Lf (fun z => h2 (Q z) (P z)) (disjointU g) (productb g).
rewrite /Sr /Pr.
have ->: (disjointU g) = source hh by rewrite /hh; aw.
have ->: (productb g) = target hh by rewrite /hh; aw.
apply: incr_fun_morph; apply: lf_injective.
by move=> z zf; move: (disjointU_hi zf) => [p1 p2 p3]; apply: hp6.
move=> u v ud vd; move: (disjointU_hi ud) => [p1 p2 p3].
move: (disjointU_hi vd) => [p4 p5 p6] eq.
by move: (hp8 _ _ _ _ p1 p4 eq) => [sp sq]; apply: pair_exten.
have [k1 kdf1 ki1]: exists2 k, inc k (domain g) & k <> i.
ex_middle ne; case: dgs; set_extens t.
move=> tdf; apply /set1_P; ex_middle ti; case: ne; ex_tac.
by move /set1_P => ->.
case: (p_or_not_p (exists k2, [/\ inc k2 (domain g), k2 <> i & k2 <> k1])).
move=> [k2 [k2df k2i k12]].
(* at least three elements in the domain of g *)
pose hh j x:= Lg (domain g) (fun z => Yo (z = j) x (P (h z))).
have hp1: forall j x, inc j (domain g) -> inc x (Vg g j) -> inc (hh j x) Pr.
move => j x jdf xv; apply /setXb_P;rewrite /hh;bw;split;fprops.
by move => z zdf; bw; Ytac zj; [ ue |move: (gp _ zdf) => [] ].
have hp2: forall j x y, inc j (domain g) -> (hh j x = hh j y) -> x = y.
by move=> j x y jdf sh;move:(f_equal (Vg^~j) sh);rewrite/hh; bw;Ytac0;Ytac0.
have hp3: forall j k x y, inc j (domain g) -> inc k (domain g)-> j <> k ->
(hh j x = hh k y) -> (x = P (h j) /\ y = P (h k)).
move=> j l x y jdf ldf jl sh;split.
by move: (f_equal (Vg^~ j) sh); rewrite /hh; bw; Ytac0; Ytac0.
by move: (f_equal (Vg^~ l) sh); rewrite /hh; bw; Ytac0; Ytac0.
pose h1 j := Lg (domain g) (fun z : Set => Yo (z = j) (P (h z)) (Q (h z))).
have hp4: forall j, inc j (domain g) -> inc (h1 j) Pr.
move => j jdf; apply /setXb_P;rewrite /h1;bw;split;fprops.
by move=> z zdf; bw; move:(gp _ zdf) => [za zb _]; Ytac zj.
have hp5: forall j j', inc j (domain g) -> (h1 j = h1 j') -> j = j'.
move=> j j' jdf sh;ex_middle jj'; move: (f_equal (Vg ^~j) sh).
rewrite /h1; bw;Ytac0; Ytac0.
by move:(gp _ jdf) => [_ _ zc].
pose h2 j x := Yo (x = P (h j)) (h1 j) (hh j x).
exists h2; split.
move=> j x jdf xV; rewrite /h2; Ytac e1; [by apply: hp4 | by apply: hp1].
have hp7: forall j k x, inc j (domain g) ->inc k (domain g) ->
hh j x <> h1 k.
move=> j k x jdf kdf; rewrite /hh /h1; bw.
suff [z [zdf z1 z2]]: (exists z, [/\ inc z (domain g), z <> j & z <> k]).
move=> eq; move: (f_equal (Vg ^~z) eq); bw; Ytac0; Ytac0.
by move: (gp _ zdf) => [_ _].
case: (equal_or_not j i) => ji.
case: (equal_or_not k k1) => kk1.
exists k2; rewrite ji kk1;split => //.
by exists k1; rewrite ji;split => //; apply: nesym.
case: (equal_or_not k i) => kk1; last by exists i; split => //;apply: nesym.
case: (equal_or_not j k1) => jk2.
by exists k2; rewrite kk1 jk2.
by exists k1; rewrite kk1; split => //; apply: nesym.
move=> j k x y jdf kdf; rewrite /h2; Ytac e1.
Ytac e2.
by move=> sh1; move: (hp5 _ _ jdf sh1) => aux; rewrite e1 e2 aux.
by move => aux; case: (hp7 _ _ y kdf jdf).
Ytac e2 => sh1; first by case: (hp7 _ _ x jdf kdf).
case: (equal_or_not j k) => e3.
split => //;rewrite e3 in sh1; apply: (hp2 _ _ _ kdf sh1).
by move: (hp3 _ _ _ _ jdf kdf e3 sh1) => [aux1 aux2].
(* there are two elements in the domain of g *)
move=> aux.
have dfp: forall j, inc j (domain g) -> j = i \/ j = k1.
move=> j jdf; case: (equal_or_not j i); first by left.
case: (equal_or_not j k1); first by right.
move=> jk1 ji; case: aux; exists j;split => //.
clear aux.
move: (gp _ idg) (gp _ kdf1).
set a1:= (P _); set a2 := (Q _);set b1:= (P _); set b2 := (Q _).
move=> [a1v a2v a12] [b1v b2v b12].
pose F x y := Lg (domain g) (fun z => (Yo (z = i) x y)).
have fP: forall x y, inc x (Vg g i) -> inc y (Vg g k1) -> inc (F x y) Pr.
move=> x y xv yx; apply /setXb_P; rewrite /F /Pr; split;fprops; bw.
move=> j jdf; bw; Ytac jv; try ue.
case: (dfp _ jdf) => // -> //.
pose h2 j x := Yo (j = i) (Yo (x = a1) (F a1 b1)
(Yo (x = a2) (F a2 b1) (F x b1)))
(Yo (x = b1) (F a1 b2)
(Yo (x = b2) (F a2 b2) (F a1 x))).
exists h2; split.
move => j x jdf xv; rewrite /h2; Ytac ji.
Ytac xa1; [ by apply: fP | Ytac xa2; [ by apply: fP |apply: fP => //; ue]].
Ytac xb1; [ by apply: fP | Ytac xb2; [ by apply: fP| apply: fP => //]].
by case: (dfp _ jdf) => //; move=> <-.
have Fi1: forall x y x' y', F x y = F x' y' -> x = x'.
by move=> x y x' y' eq;move:(f_equal (Vg^~i) eq); rewrite /F; bw;Ytac0; Ytac0.
have Fi2: forall x y x' y', F x y = F x' y' -> y = y'.
by move=> x y x' y' eq;move:(f_equal (Vg^~k1) eq);rewrite /F; bw;Ytac0; Ytac0.
move=> j k x y jdf kdf; rewrite /h2; bw.
Ytac ij.
Ytac xa1.
Ytac ki.
Ytac ya1; first by rewrite ij ki xa1 ya1//.
Ytac ya2; move=> eq; move:(Fi1 _ _ _ _ eq) ; first by done.
by move => eql; case: ya1; rewrite eql.
Ytac yb1; first by move=> eq; move: (Fi2 _ _ _ _ eq).
Ytac yb2; move=> eq; move: (Fi2 _ _ _ _ eq); first done.
by move => eql; case: yb1; rewrite eql.
Ytac xa2.
Ytac ki.
Ytac ya1; first by move=> eq; move:(Fi1 _ _ _ _ eq) => eql; case: a12.
Ytac ya2; first by rewrite ij ki xa2 ya2//.
by move=> eq; move:(Fi1 _ _ _ _ eq)=> eql; case: ya2; rewrite eql.
Ytac yb1; first by move=> eq; move: (Fi2 _ _ _ _ eq).
Ytac yb2; move=> eq; move: (Fi2 _ _ _ _ eq); first by done.
by move => eql; case: yb1; rewrite eql.
Ytac ki.
Ytac ya1; first by move=> eq; move:(Fi1 _ _ _ _ eq) => eql; case: a12.
Ytac ya2; first by move=> eq; move:(Fi1 _ _ _ _ eq) => eql; case: a12.
move=> eq; move:(Fi1 _ _ _ _ eq) => eql; rewrite ij ki; split => //.
Ytac yb1; first by move=> eq; move: (Fi2 _ _ _ _ eq).
Ytac yb2; move=> eq; move: (Fi2 _ _ _ _ eq); first by done.
by move => eql; case: yb1; rewrite eql.
case: (dfp _ jdf) => // jk1.
Ytac xb1.
Ytac ki.
Ytac ya1; first by move=> eq; move:(Fi2 _ _ _ _ eq) => eql; case: b12.
Ytac ya2; by move=> eq; move:(Fi2 _ _ _ _ eq) => eql; case: b12.
case: (dfp _ kdf) => // kk1.
Ytac yb1; first by rewrite jk1 kk1 xb1 yb1; split => //.
Ytac yb2; first by move=> eq; move: (Fi1 _ _ _ _ eq).
by move=> eq; move:(Fi2 _ _ _ _ eq) => eql; case: yb2.
Ytac xb2.
Ytac ki.
by Ytac ya1; [| Ytac ya2 ];
move=> eq; move:(Fi2 _ _ _ _ eq) => eql; case: b12.
Ytac yb1; first by move=> eq; move:(Fi1 _ _ _ _ eq) => eql; case: a12.
case: (dfp _ kdf) => // kk1.
Ytac yb2; first by rewrite jk1 kk1 xb2 yb2; split => //.
by move=> eq; move:(Fi1 _ _ _ _ eq) => eql; case: a12.
Ytac ki.
by Ytac ya1; [| Ytac ya2 ]; move=> eq;move:(Fi2 _ _ _ _ eq) => eql; case: xb1.
rewrite jk1;case: (dfp _ kdf) => // -> aux; split => //; move: aux.
Ytac yb1; [ | Ytac yb2 ];move=> eq; move: (Fi2 _ _ _ _ eq) => //.
Qed.
Lemma compare_sum_prod2:
(forall i, inc i (domain f) -> (Vg f i) <=c (Vg g i)) ->
(csum f) <=c (cprod g).
Proof.
move=> ale1.
exact: (cleT (csum_increasing sd ale1) (compare_sum_prod1)).
Qed.
Lemma compare_sum_prod3:
(forall i, inc i (domain f) -> (Vg f i)
(csum f) alt1.
have ale1: (forall i, inc i (domain f) -> (Vg f i) <=c (Vg g i)).
by move => i idf; move: (alt1 _ idf) => [ok _].
split; first by apply: compare_sum_prod2.
move /card_eqP=> [h [bh sh th]].
pose D i := (Vg f i) *s1 i.
have Dp1: forall i, inc i (domain f) -> sub (D i) (source h).
move=> i idf t td. rewrite sh; apply /setUb_P.
rewrite /disjointU_fam; bw; ex_tac; bw.
pose A i := Vfs h (D i).
have Dp2: forall i, inc i (domain f) -> (cardinal (A i)) [ih _].
move=> i idf;move: (Eq_restriction1 (Dp1 _ idf) ih).
move /card_eqP; rewrite -/ (A i).
have: cardinal (D i) = cardinal (Vg f i) by apply:cardinal_indexed.
move: (alt1 _ idf) => aux.
by rewrite (card_card (proj31_1 aux)) => -> <-.
have fh: function h by fct_tac.
have Dp3: forall i, inc i (domain f) -> sub (A i) (target h).
by move=> i idf; apply: fun_image_Starget1.
have Dp4: forall i F, inc i (domain f) -> sub F (target h) ->
(cardinal (Vfs (pr_i g i) F)) <=c (cardinal F).
rewrite th; move=> i F idf Fp; apply: surjective_cle.
have idg: inc i (domain g) by ue.
exists (restriction1 (pr_i g i) F); split => //; rewrite /restriction1; aw.
apply: restriction1_fs; first by apply: pri_f => //.
rewrite /pr_i; aw.
have Dp5: forall i, inc i (domain f) ->
(cardinal (Vfs (pr_i g i) (A i))) i idf; exact:(cle_ltT (Dp4 _ _ idf (Dp3 _ idf)) (Dp2 _ idf) ).
have Dp6: forall i, inc i (domain f) -> exists xi, inc xi (Vg g i) /\
(forall y, inc y (A i) -> Vf (pr_i g i) y <> xi).
move=> i idf; move: (Dp5 _ idf); set T := Vfs _ _.
have fp: function (pr_i g i) by apply: pri_f => //; ue.
have st: sub T (Vg g i).
by move: (@fun_image_Starget1 _ fp (A i)); rewrite {2} /pr_i lf_target.
rewrite -{1} (card_card (proj32_1 ( (alt1 _ idf)))); move=> [_ neq].
ex_middle nex; case: neq;apply:f_equal; apply:extensionality =>//.
have sAi: sub (A i) (source (pr_i g i)).
by rewrite /pr_i; aw; rewrite -th; apply: Dp3.
move=> x xv; apply /(Vf_image_P fp sAi).
ex_middle ney; case: nex; exists x; split => //.
move=> y yA;case: (equal_or_not (Vf (pr_i g i) y) x) => //.
move=> wy; case: ney; ex_tac.
pose k i:= choose (fun xi => inc xi (Vg g i) /\
(forall y : Set, inc y (A i) -> Vf (pr_i g i) y <> xi)).
have kp: forall i, inc i (domain f) ->
(inc (k i) (Vg g i) /\ (forall y, inc y (A i) -> Vf (pr_i g i) y <> (k i))).
move=> i idf; apply choose_pr; apply: (Dp6 _ idf).
set x := Lg (domain g) k.
have xth: inc x (target h).
rewrite th /x; apply /setXb_P; split;fprops; bw; move=> i idg; bw.
by rewrite - sd in idg; move: (kp _ idg) => [p1 _].
move: bh => [ih sjh]; move: ((proj2 sjh) _ xth) => [y ysg Wy].
move: ysg; rewrite sh; move /setUb_P.
rewrite/disjointU_fam; bw.
move=> [i idf]; bw => yd.
have xA: inc x (A i).
by rewrite /A -Wy; apply /(Vf_image_P (proj1 ih)(Dp1 _ idf)); exists y.
move: (kp _ idf) => [_ p2]; move: (p2 _ xA).
rewrite sd in idf; rewrite th in xth.
by rewrite pri_V // /x; bw.
Qed.
End Exercise3_3.
Lemma compare_sum_prod f g:
fgraph f -> fgraph g -> domain f = domain g ->
(forall i, inc i (domain f) -> (Vg f i)
(csum f) fgf fgg sd ale1.
set K:= Zo (domain f) (fun i => \2c <=c (Vg g i)).
have kdf: sub K (domain f) by apply: Zo_S.
have kdg: sub K (domain g) by ue.
have aux: forall i, inc i ((domain f) -s K) ->
(Vg f i = \0c /\ Vg g i = \1c).
move=> i => /setC_P [idf] /Zo_P aux.
have le1:=(ale1 _ idf).
case: (cleT_el CS2 (proj32_1 le1)); first by move=> h; case: aux;split => //.
rewrite - succ_one ; move /(cltSleP NS1) => h1.
have p1:=(clt1 (clt_leT le1 h1)).
split => //; apply: (cleA h1).
by move: le1; rewrite p1; move/cge1P.
have pf:(forall i, inc i ((domain f) -s K) -> Vg f i = \0c).
by move=> i ic; move: (aux _ ic) => [].
have pg:(forall i, inc i ((domain g) -s K) -> Vg g i = \1c).
by rewrite - sd;move=> i ic; move: (aux _ ic) => [].
rewrite (csum_zero_unit kdf pf) (cprod_one_unit kdg pg).
apply: compare_sum_prod3; bw.
by move=> i iK; bw; move: iK => /Zo_P //; case.
by move=> i iK; bw; apply: ale1; apply: kdf.
Qed.
Lemma exists_ordering X: cardinal_fam X ->
exists f,
[/\ bijection f, ordinalp (source f), target f = domain X &
fg_Mle_lec (X \cf (graph f))].
Proof.
move => pb.
set d := domain X.
have [w wp]: exists t, ~(inc t d).
ex_middle h.
set z := Zo d (fun z => ~ (inc z z)).
case: (p_or_not_p (inc z z)) => h2.
by move: (h2) => /Zo_hi bad.
by case: (h2); apply: Zo_i => //; ex_middle h1; case: h; exists z.
pose lev Y:= choose(fun z => inc z Y /\ forall u, inc u Y -> Vg X z <=c Vg X u).
have lep: forall Y, sub Y d -> nonempty Y ->
(inc (lev Y) Y /\ forall u, inc u Y -> Vg X (lev Y) <=c Vg X u).
move => Y yd [y yY]; apply choose_pr.
set Z := fun_image Y (Vg X).
have neZ: nonempty Z by exists (Vg X y); apply /funI_P; exists y.
have cz: cardinal_set Z.
by move => t /funI_P [z zy ->]; apply: pb; apply: yd.
move: (wordering_cle_pr cz)=> [ [qb qc] qa].
have qd: sub Z (substrate (graph_on cardinal_le Z)) by rewrite qa; fprops.
rewrite qa in qc; move: (qc _ (@sub_refl Z) neZ) => [z []].
rewrite iorder_sr //; move/funI_P => [t ty ->] tmin; exists t; split => //.
move => u uy.
have h1: inc (Vg X u) (fun_image Y (Vg X)) by apply/funI_P ; ex_tac.
by move: (iorder_gle1 (tmin _ h1)); move /graph_on_P1=> [_ _ ok].
pose lew Y:= Yo (nonempty (d -s Y)) (lev (d -s Y)) w.
have lewe: forall Y, nonempty (d -s Y) ->
(inc (lew Y) (complement d Y) /\
(forall u : Set, inc u (d -s Y) -> Vg X (lew Y) <=c Vg X u)).
by move => y ye; rewrite /lew; Ytac0; apply: lep => //; apply: sub_setC.
have lewb: forall Y, inc (lew Y) (d +s1 w).
move => Y; case: (p_or_not_p (nonempty (d -s Y))) => h.
move: (lewe _ h) => [] /setC_P [ok _] _; fprops.
rewrite /lew; Ytac0; fprops.
move: (cantor (CS_cardinal d)); set a := _ ^c _ => lt1.
move: (lt1) =>[[_ ca _] _]; move: (ca) => [oa _].
move: (ordinal_o_wor oa); set r := ordinal_o _ => wor.
have sr: substrate r = a by rewrite /r ordinal_o_sr.
pose lef f := lew (Imf f).
have ts: (forall f, function f -> segmentp r (source f) ->
sub (target f) (d +s1 w)-> inc (lef f) (d +s1 w)).
move=> f ff srf sta; apply: lewb.
move: (transfinite_defined_pr lef wor); rewrite /transfinite_def sr.
move: (transfinite_definition_stable wor ts).
set f := transfinite_defined _ _; move=> stf [sjf sf fv].
have ff: function f by fct_tac.
have fi: forall i, inc i a -> Vf f i <> w ->
forall j, inc j i -> Vf f i <> Vf f j.
move => i ia fw; move: (fv _ ia); rewrite /lef.
set E := (Imf (restriction_to_segment r i f)) => eq1.
move: eq1; case: (p_or_not_p (nonempty (d -s E))) => nt;
last by rewrite /lew; Ytac0.
move: (lewe _ nt) => [] /setC_P [_ s1] _ eq; move => j ji sv.
case: s1; rewrite -eq sv /E.
have sr1 : (source (restriction_to_segment r i f)) = i.
rewrite /restriction_to_segment /restriction1; aw.
rewrite /r ordinal_segment //.
have sa1: sub (segment r i) (source f) by rewrite sf - sr ;apply: sub_segment.
have ji1: inc j (segment r i).
apply /segmentP; apply /ordo_ltP => //.
by apply: (ordinal_transitive oa ia).
move : (proj1 (restriction1_fs ff sa1)) => fr.
apply /(Vf_image_P1 fr).
by rewrite sr1;exists j => //; rewrite (restriction1_V ff sa1 ji1).
case: (p_or_not_p (inc w (target f))) => wt; last first.
have bf: (bijection f).
split; last by exact.
split; first by fct_tac.
move => x y xsf ysf sv.
case: (equal_or_not (Vf f x) w) => le1.
case: wt; rewrite -le1; Wtac.
rewrite sf in xsf ysf.
have ox:= (ordinal_hi oa xsf).
have oy:= (ordinal_hi oa ysf).
case: (oleT_ell ox oy) => //.
move /(oltP oy) => lt2.
by rewrite sv in le1; move: (fi _ ysf le1 _ lt2); rewrite sv.
by move /(oltP ox) => lt2; move: (fi _ xsf le1 _ lt2).
have /sub_smaller: sub (target f) d.
move=> t td; move: (stf _ td); case/setU1_P => // tw; case: wt;ue.
have <-: (cardinal (source f) = cardinal (target f))
by apply /card_eqP; exists f;split => //.
by rewrite sf (card_card ca) => /(cltNge lt1).
pose pri i := (inc i (source f) /\ Vf f i = w).
have [i0 oi0 iv0]: exists2 i, ordinalp i & pri i.
rewrite /pri;move: ((proj2 sjf) _ wt) => [i iv1 iv2]; exists i => //.
by move: iv1;rewrite sf => /(ordinal_hi oa).
move: (least_ordinal4 oi0 iv0).
set qi :=least_ordinal _ _;move=> [oq [qsf qv] ql].
rewrite sf in qsf;move: qv; rewrite (fv _ qsf) /lef /lew.
set c := complement _ _ => qv.
case: (p_or_not_p (nonempty c)) =>h.
move: (lewe _ h) => [] /setC_P [wd _] _; case: wp.
by move: wd;rewrite /lew -/c qv.
set e := Imf (restriction_to_segment r qi f).
have sr1 : (source (restriction_to_segment r qi f)) = qi.
rewrite /restriction_to_segment /restriction1; aw.
rewrite /r ordinal_segment //.
have sa1: sub (segment r qi) (source f) by rewrite sf - sr ;apply: sub_segment.
have fr:=(proj1 (restriction1_fs ff sa1)).
have pa1: forall i, inc i qi ->(inc (Vf f i) d /\ Vf f i <> w).
move => t tq.
move: (ordinal_transitive oa qsf tq); rewrite - sf => tf.
have tw:inc (Vf f t) (target f) by apply: Vf_target.
move: (stf _ tw) => /setU1_P.
case: (equal_or_not (Vf f t) w) => ww; last by case.
have prt : (pri t) by split.
have h1:= (ql _ (ordinal_hi oq tq) prt).
by move: tq => /(oltP (proj31 h1)) /(oleNgt h1).
have fv1: forall u, inc u qi -> (Vf (restriction_to_segment r qi f)u) = Vf f u.
move => i iq.
have ji1: inc i (segment r qi).
apply /segmentP; apply /ordo_ltP => //.
by apply: (ordinal_transitive oa qsf).
by rewrite (restriction1_V ff sa1 ji1).
have de: d = e.
set_extens t.
move: h; rewrite /c -/e => qa qb; ex_middle tne; case: qa.
exists t; apply /setC_P;split => //.
move /(Vf_image_P1 fr); rewrite sr1; move => [u uq ->].
by rewrite (fv1 _ uq); move: (pa1 _ uq) => [].
have ij1: forall i j, inc i qi -> inc j qi -> Vf f i = Vf f j -> i = j.
move => i j iq jq sv.
move: (pa1 _ iq) (pa1 _ jq)=> [_ xa1] [_ ya1].
have ia:= ordinal_transitive oa qsf iq.
have ja:=ordinal_transitive oa qsf jq.
have oi:= ordinal_hi oa ia.
have oj:= ordinal_hi oa ja.
case: (oleT_ell oi oj) => //.
by move /(oltP oj) => lt2; move: (fi _ ja ya1 _ lt2); rewrite sv.
by move /(oltP oi) => lt2; move: (fi _ ia xa1 _ lt2).
have ij2: injection (restriction_to_segment r qi f).
split; first by exact.
rewrite sr1; move => x y xsf ysf /=.
by rewrite (fv1 _ xsf) (fv1 _ ysf); apply: ij1.
move: (restriction_to_image_fb ij2).
set g := restriction_to_image (restriction_to_segment r qi f).
have tg: target g = d.
by rewrite /g de /restriction_to_image/ restriction2; aw.
have osd: ordinalp (source g).
rewrite /g /restriction_to_image/ restriction2 sr1; aw.
move: (restriction_to_image_fb ij2) => bg.
have fg: function g by fct_tac.
have r2a: restriction2_axioms (restriction_to_segment r qi f)
(source (restriction_to_segment r qi f))
(Imf (restriction_to_segment r qi f)).
by split => //; apply: fun_image_Starget.
have gV : forall i, inc i qi -> Vf g i = Vf f i.
move => i iq; rewrite/g /restriction_to_image restriction2_V // ? fv1 ? sr1//.
exists g; split => // u v.
rewrite composef_domain => us vs uv; bw; rewrite -/(Vf g u) -/ (Vf g v).
have aux: domain (graph g) = qi.
rewrite (f_domain_graph fg) /g /restriction_to_image /restriction2 corresp_s.
aw; rewrite sr1.
rewrite aux in us vs; rewrite (gV _ us) (gV _ vs).
move: (pa1 _ us) => [wfu wfuw].
case: (equal_or_not u v) => euv.
by rewrite - euv; apply: cleR; apply: pb.
move: (ordinal_transitive oa qsf us) => ua.
rewrite (fv _ ua) /lef /lew; set c1:= nonempty _.
case: (p_or_not_p c1) => c1e; last first.
by case: wfuw; rewrite (fv _ ua) /lef /lew; Ytac0.
move: (lewe _ c1e); rewrite /lew.
set f0:= (restriction_to_segment r u f); set x := Yo _ _ _; move=> [qa qb].
suff: inc (Vf f v)(d -s (Imf f0)).
move => qc; apply: (qb _ qc).
have sa2: sub (segment r u) (source f) by rewrite sf - sr ;apply: sub_segment.
have sr2 : (source (restriction_to_segment r u f)) = u.
rewrite /restriction_to_segment /restriction1; aw.
rewrite /r ordinal_segment //.
have fr2:=(proj1 (restriction1_fs ff sa2)).
move: (pa1 _ vs) => [wfv _]; apply /setC_P;split => //.
move /(Vf_image_P1 fr2); rewrite sr2; move => [t tu].
have tu1: inc t (segment r u).
by apply/segmentP; apply/ordo_ltP => //; move:(ordinal_transitive oa ua tu).
rewrite (restriction1_V ff sa2 tu1) => sv1; symmetry in sv1.
have tqi:=(ordinal_transitive oq us tu).
move: tu; rewrite (ij1 _ _ tqi vs sv1).
by move /(oltP (ordinal_hi oa ua)) => /(oleNgt uv).
Qed.
Definition cardinal_pos_fam g := (allf g (fun z => \0c cardinal_pos_fam x ->
(\csup (range x)) <=c (cprod x).
Proof.
move => fx xi.
set A := Zo (domain x) (fun a => \2c <=c (Vg x a)).
have pa: (forall i, inc i ((domain x) -s A) -> (Vg x i) = \1c).
move=> i /setC_P [idx ] /Zo_P h.
move: (xi _ idx) => [xx yy]; ex_middle x1; case: h; split => //.
apply: (cge2 (proj32 xx) (nesym yy) x1).
have Ax: sub A (domain x) by apply: Zo_S.
set g := (Lg A (Vg x)).
have fgg: fgraph g by rewrite /g ; fprops.
have dg: domain g = A by rewrite /g; bw.
have gs: (forall i : Set, inc i (domain g) -> \2c <=c Vg g i).
by rewrite /g dg => i iA; bw; move: iA => /Zo_P [_].
move: (compare_sum_prod1 gs); rewrite (cprod_one_unit Ax pa) - /g.
have cs: cardinal_set (range x).
move => t /(range_gP fx) [z zy ->]; exact: (proj32_1(xi _ zy)).
case: (emptyset_dichot A) => Ae.
move => _.
have pb: union (range x) <=c \1c.
apply: card_ub_sup => //; fprops.
move => i /(range_gP fx) [j jy ->].
have ja: inc j ((domain x) -s A)
by apply /setC_P;split => //;rewrite Ae;case; case.
rewrite (pa _ ja); fprops.
rewrite /cprodb cprod_trivial //; bw.
apply: cleT.
have pb: (forall a, inc a (domain g) -> cardinalp (Vg g a)).
by move => a /gs /proj32.
move: Ae => [a Aa]; move: (Aa) => /Zo_P [ay].
have ->: Vg x a = Vg g a by rewrite /g;bw.
rewrite -dg in Aa; move: (csum_increasing6 pb Aa).
move => le1 le2; move: (cleT le2 le1) => le3.
apply: card_ub_sup => //; first by rewrite /csum; fprops.
move=> i /(range_gP fx) [j jdx ->].
have s1:= (cleT (proj1 (clt_12)) le3).
case: (inc_or_not j A) => jA.
rewrite -dg in jA; move: (csum_increasing6 pb jA).
rewrite {1}/g; bw; ue.
have jc: inc j ((domain x) -s A) by apply /setC_P;split => //.
by rewrite (pa _ jc).
Qed.
Lemma infinite_increasing_power_bound1 X:
fgraph X -> ordinal_fam X ->
limit_ordinal (\osup (range X)) ->
cprod (Lg (domain X) (fun z => \aleph (Vg X z))) <=c
\aleph (\osup (range X)) ^c (cardinal (domain X)).
Proof.
move => fX ogx ob.
have ->: omega_fct (union (range X)) ^c cardinal (domain X) =
omega_fct (union (range X)) ^c (domain X).
apply cpow_pr; fprops.
rewrite - cpow_pr2 /cst_graph; apply: cprod_increasing; bw; fprops.
move => i idx; bw; apply: aleph_le_lec.
apply: ord_sup_ub.
move => t tx; move: tx => /(range_gP fX) [z zi ->]; apply: (ogx _ zi).
apply /(range_gP fX); exists i => //;ue.
Qed.
Lemma infinite_increasing_power4 X (Y:= Lg (domain X)(fun z => \aleph (Vg X z)))
(a := \osup (range X)):
ofg_Mlt_lto X -> limit_ordinal (domain X) ->
(cardinal (domain X) <=c \aleph a /\ \aleph a pa pb.
move: (increasing_sup_limit4 pa pb);rewrite -/Y -/a; move => [pc pd pe].
move: pa => [fgx xo xi].
move: (pc)(pb) => [oa _ _] [odx _ ldx].
have pa: cardinal (domain X) <=c (cardinal a).
set f := Lf (Vg X) (domain X) (range X).
have bf:bijection f.
apply: lf_bijective.
move => t td; apply /(range_gP fgx); ex_tac.
move => u v ud vd sv.
case: (oleT_ell (ordinal_hi odx ud)(ordinal_hi odx vd)) => // cuv.
by move: (xi _ _ ud vd cuv); rewrite sv;move => [_].
by move: (xi _ _ vd ud cuv); rewrite sv;move => [_].
move => y /(range_gP fgx) [x xd ->]; ex_tac.
have ->: (cardinal (domain X)) = (cardinal (range X)).
apply /card_eqP; exists f;split => //; rewrite /f; aw.
apply: (sub_smaller pd).
move: (ocle1 (aleph_pr6 oa)).
rewrite (card_card (CS_aleph oa)) => lt1.
move: (cleT pa lt1) => le1 {pa lt1}.
split; first by exact.
have ia:=(CIS_aleph (proj31 pc)).
have cfy: cardinal_fam Y.
rewrite /Y;hnf;bw; move => i idx; bw; apply: CS_aleph;fprops.
have fgY: fgraph Y by rewrite /Y; fprops.
have cd1: cardinal (domain Y) <=c omega_fct a by rewrite /Y; bw.
have <-: csum Y = \aleph a.
by rewrite /Y - pe; apply: csum_of_small_b4 => //; rewrite pe.
set Z := Lg (domain X) (fun z => (omega_fct (Vg X (osucc z)))).
have fgZ: fgraph Z by rewrite /Z; fprops.
have sd: domain Y = domain Z by rewrite /Y /Z; bw.
have inc1: (forall i, inc i (domain Y) -> Vg Y i i idx; bw; apply: aleph_lt_ltc.
apply: xi => //; [ by apply: ldx | apply: (oltS (ordinal_hi odx idx)) ].
apply: (clt_leT (compare_sum_prod fgY fgZ sd inc1)).
set X1 := fun_image (domain X) osucc.
have scx1: sub X1 (domain X) by move =>t /funI_P [z zd ->]; apply: ldx.
have <-: cprod (restr Y X1) = cprod Z.
have ->: cprod (restr Y X1) = cprodb X1 (fun z => \omega (Vg X z)).
by apply:cprodb_exten => i ii; rewrite /Y;bw; apply: scx1.
rewrite /Z -/(cprodb _ _); apply:cprod_Cn2; split.
+ move => t td; apply /funI_P; ex_tac.
+ move => u v ud vd.
exact: (ord_succ_inj (ordinal_hi odx ud)(ordinal_hi odx vd)).
+ by move => y /funI_P.
apply: cprod_increasing1 => //; last by rewrite /Y; bw.
by hnf;rewrite /Y; bw;move => x xd; bw; apply: aleph_nz; apply: xo.
Qed.
Lemma infinite_increasing_power5 X (Y:= Lg (domain X)(fun z => \aleph (Vg X z)))
(a := \osup (range X)):
ofg_Mlt_lto X -> limit_ordinal (domain X) ->
[/\ omega_fct a pa pb.
move: (infinite_increasing_power4 pa pb) => [qa qb].
move: (increasing_sup_limit4 pa pb);rewrite -/Y -/a; move => [pc pd pe].
move: pa => [fgx xo xi].
move: (infinite_increasing_power_bound1 fgx xo pc); rewrite -/Y -/a => le1.
split; [exact | exact |].
move: (cpow_Meqle (aleph_nz (proj31 pc)) qa).
rewrite -/a infinite_power1_b //; apply: (CIS_aleph (proj31 pc)).
Qed.
Lemma infinite_increasing_power x (y := domain x):
fgraph x -> infinite_c y -> cardinal_pos_fam x ->
fg_Mle_lec x ->
cprod x = (\csup (range x)) ^c y.
Proof.
move => fx cy alz xi.
have osr: cardinal_set (range x).
move => t /(range_gP fx) [z zy ->]; exact: (proj32_1(alz _ zy)).
apply: cleA.
rewrite - cpow_pr2 /cst_graph; apply: cprod_increasing => //; fprops; bw.
move=>t td; bw; apply: card_sup_ub => //; apply /(range_gP fx); ex_tac.
move: (infinite_product_prop2 cy) => [f [bf sf tf] fp].
set g:= Lg y (fun z=> fun_image y (fun t => (Vf f (J t z)))).
have ff: function f by fct_tac.
have pa: partition_w_fam g (domain x).
rewrite /g; split;fprops.
apply: mutually_disjoint_prop; bw.
move=> i j z iy jy; bw.
move=> /funI_P [a ay av] /funI_P [b iby bv].
rewrite av in bv.
have asf: inc (J a i) (source f) by rewrite sf; fprops.
have bsf: inc (J b j) (source f) by rewrite sf; fprops.
exact (pr2_def (bij_inj bf asf bsf bv)).
set_extens t.
move /setUb_P; bw; move => [a ay];bw; move /funI_P => [b ny ->].
rewrite -/y -tf; Wtac; rewrite sf; fprops.
rewrite -/y -tf => ytf; move: (bij_surj bf ytf) => [z zs zv].
move: zs; rewrite sf => /setX_P; rewrite -tf; move => [pz za zb].
apply /setUb_P; exists (Q z) => //;bw; apply /funI_P.
by exists (P z) => //; rewrite pz.
rewrite (cprod_An pa).
rewrite {1} /g; bw.
rewrite - cpow_pr2 /cst_graph; apply: cprod_increasing => //; fprops; bw.
move=> a ay; bw.
set h := (restr x (Vg g a)).
have fgr: fgraph (restr x (Vg g a)) by rewrite /h;fprops.
have s1: sub (Vg g a) (domain x).
rewrite /g => t; bw; move /funI_P => [z zy ->]; rewrite -/y - tf.
Wtac; rewrite sf; fprops.
have pb: (forall b, inc b (domain h) -> \0c b bv.
rewrite restr_ev //; exact: (alz _ (s1 _ bv)).
move: (compare_sum_prod5 fgr pb); rewrite -/h => le1.
have csh: cardinal_set (range h).
move => t /(range_gP fgr) [u ud ->]; exact: (proj32_1 (pb _ ud)).
apply: (cleT _ le1).
apply card_ub_sup => //; first by apply: CS_sup.
move => i /(range_gP fx) [j jdx ->].
rewrite -/y -tf in jdx; move:(bij_surj bf jdx) => [z zf <-].
move: (zf); rewrite sf => /setX_P [pz py qy].
move: (infinite_card_limit2 cy) => [oy _ yp].
have op: ordinal_pair z by split => //; apply: (ordinal_hi (proj1 (proj1 cy))).
set b0 := ((P z) \cup (Q z)); set b := osucc b0.
have ib0y: inc b0 y by rewrite /b0;case: (ordering_pair1 op); move=> [_ -> ].
have iby: inc b y by apply yp.
move: (ordinal_hi oy iby) (ordinal_hi oy ay) => ob oa.
have opab: ordinal_pair (J b a) by split => //; aw; fprops.
have bsba: b <=o (b \cup a).
by case: (ordering_pair1 opab); aw; move => [le ->] //; apply oleR.
have ult: (P z) \cup (Q z) J b a by move => zj; case: (proj2 ult); rewrite zj; aw.
have sa: inc (Vf f (J b a)) (Vg g a)
by rewrite /g; bw; apply /funI_P; ex_tac.
have wy: inc (Vf f z) y by rewrite - tf; Wtac.
have wy': inc (Vf f (J b a)) y by rewrite - tf; Wtac; rewrite sf; fprops.
have jsf: inc (J b a) (source f) by rewrite sf; fprops.
have sb: Vf f z //.
apply /graph_on_P1; split => //;
[ apply /setX_P;split => // | fprops | by split => //; aw; left].
apply: (cleT (xi _ _ wy wy' (proj1 sb))).
apply: card_sup_ub => //; apply /(range_gP fgr).
exists (Vf f (J b a)); rewrite /h => //; bw.
Qed.
Lemma power_cofinality x: \2c <=c x -> x x1; move: (cofinality_c_rw x1) => [pb pc _].
move: pc => [f [[pc pd] pe pf]].
set g := cst_graph (domain f) x.
have pg: fgraph g by rewrite /g/cst_graph; fprops.
have ph: domain f = domain g by rewrite /g/cst_graph; bw.
have pi: (forall i, inc i (domain f) -> (Vg f i) i idf; rewrite /g/cst_graph; bw;apply:pd.
by move: (compare_sum_prod pc pg ph pi); rewrite /g cpow_pr2 pe pf.
Qed.
Lemma power_cofinality1 x: infinite_c x -> x icx; rewrite -(cofinality_card icx); apply: power_cofinality.
by apply: infinite_ge2.
Qed.
Lemma power_cofinality2 x: infinite_c x -> x xi;move: (infinite_powerset xi).
set y:= (\2c ^c x); move => iy.
have cx:= proj1 xi.
have ia := (cofinality_infinite_cardinal iy).
case: (cleT_el (proj1 ia) cx) => le2 //.
have ynz: y <> \0c by apply: infinite_nz.
move: (cpow_Meqle ynz le2).
rewrite {3} /y - cpow_pow (csquare_inf xi) -/y => le3.
case: (cleNgt le3 (power_cofinality1 iy)).
Qed.
Lemma power_cofinality3: aleph0 infinite_c b ->
b ia ib.
have pi: infinite_c (a ^c b) by apply: CIS_pow2.
rewrite -(cofinality_card pi).
have p1: \2c <=c (a ^c b) by apply: infinite_ge2.
move: (cofinality_c_rw p1); set c:= cofinality_c (a ^c b).
move=> [le1 pa pb].
move: pa => [f [[qa qb qc] qd]].
set g := cst_graph (domain f) (a ^c b).
have fgf: fgraph f by move: qa => [].
have fgg: fgraph g by rewrite /g /cst_graph; fprops.
have sd: domain f = domain g by rewrite /g/cst_graph; bw.
have ltv: (forall i, inc i (domain f) -> (Vg f i) i idf; rewrite /g/cst_graph; bw; apply: qb.
move: (compare_sum_prod fgf fgg sd ltv).
rewrite /g cpow_pr2 qd qc - cpow_pow => lt1.
case: (cleT_el (proj31 le1) (proj1 ib)) => // cb.
have pa:= (cprod_inf1 cb ib).
case: (cltNge lt1); apply: cpow_Mlele => //; first by apply: infinite_nz.
move: ia => [ca _]; fprops.
Qed.
Lemma power_cofinality5 x y: \2c <=c x -> infinite_c y ->
y x2 icy.
have cx:= proj32 x2.
case: (cleT_ee cx (proj1 icy)) => aux.
by rewrite (infinite_power1_a x2 aux icy); apply: power_cofinality2.
exact: (power_cofinality4 (ge_infinite_infinite icy aux) icy).
Qed.
Lemma infinite_power7b x y:
infinite_c x -> y
x ^c y <=c cardinal (unionb (Lg x (functions y))).
Proof.
move=> icx yc.
have cx:= proj1 icx.
have ox:= OS_cardinal cx.
have ha:(forall f, function_prop f y x -> inc (\osup (Imf f)) x).
move => f fp; move: (fp) => [ff sf tf].
set T := (Imf f).
have osT: ordinal_set T.
move=> t /(Vf_image_P1 ff) [u usf ->].
by apply: (ordinal_hi ox); rewrite - tf;Wtac.
have ou: ordinalp (union T) by apply: OS_sup.
apply /(oltP ox);case: (oleT_el ox ou) => // le1.
have eq1: union T = x.
apply: oleA => //; apply: ord_ub_sup => //.
move=> i => /(Vf_image_P1 ff) [u usf ->].
by move: (Vf_target ff usf); rewrite tf => /(oltP ox) [].
have cox: cofinal_function_ex x y.
exists f; split => // => t tx.
have ls: t [z].
move /(Vf_image_P1 ff) => [u usf ->] [tw _].
rewrite - sf; ex_tac.
move: (cofinality_rw ox) => [_ _ h].
have oy:= (proj1 (proj31_1 yc)).
case: (oleNgt (h _ oy cox) (oclt yc)).
pose sf f := \osup (Imf f).
pose sf1 f := osucc (sf f).
have pa: forall f, inc f (functions y x) -> (sf1 f) [qa qb qc].
move => f /functionsP fp; apply /(oltP ox); apply: qc; exact: (ha _ fp).
have pb:forall f, inc f (functions y x) ->
(forall t, inc t (source f) -> inc (Vf f t) (sf1 f)).
move => f /functionsP [ff srf tf] t tsf.
have osT: ordinal_set (Imf f).
move=> z /(Vf_image_P1 ff) [u usf ->].
by apply: (ordinal_hi ox); rewrite - tf;Wtac.
apply /oleP; first by apply: OS_sup.
apply: ord_sup_ub => //; apply /(Vf_image_P1 ff); ex_tac.
pose R f := restriction2 f (source f) (sf1 f).
have pc: forall f, inc f (functions y x) ->
restriction2_axioms f (source f) (sf1 f).
move=> f fp; move: (fp) => /functionsP [qc qd qe].
split => //.
by rewrite qe; move: (pa _ fp) => [[_ _ ok] _].
by move=>t /(Vf_image_P1 qc) [u usf ->]; apply: (pb _ fp).
have pd: forall f, inc f (functions y x) ->
inc (R f) (functions y (sf1 f)).
move=> f fh; move: (restriction2_prop (pc _ fh)) => [p1 p2 p3].
apply /functionsP;split => //; rewrite /R p2.
by move: fh => /functionsP [q1 q2 q3].
set t1:= unionb _.
have pe: forall f, inc f (functions y x) -> inc (R f) t1.
move=> f fi; move: (pd _ fi) => sa.
have sb:inc (sf1 f) x by apply /(oltP ox); exact: (pa _ fi).
apply /setUb_P; bw; exists (sf1 f) => //; bw.
set g := Lf R (functions y x) t1.
suff ig: injection g by move: (incr_fun_morph ig); rewrite /g; aw.
apply: lf_injective => // u v us vs eq.
move: (pc _ us) (pc _ vs) => axf axg.
move: us vs => /functionsP [fu su tu] /functionsP [fv sv tv].
apply: function_exten => //; try ue.
move => t tsu; move: (f_equal (Vf ^~ t) eq);rewrite /R restriction2_V //.
by rewrite restriction2_V // sv - su.
Qed.
Lemma infinite_power2 n m (x:=\aleph n) (y:= \aleph (osucc n)):
ordinalp n -> m <> \0c ->
y ^c m = (x ^c m) *c y.
Proof.
move => on mnz.
rewrite -(cpowcr) -(cpowcr x);set m':= cardinal m.
have cm': cardinalp m' by rewrite /m'; fprops.
have m'nz: m' <> \0c by dneg cmz; move: (card_nonempty cmz).
have osn:= (OS_succ on).
move: (CIS_aleph on) (CIS_aleph osn) (aleph_pr10c on).
rewrite -/x -/y => icx icy ap.
have m1: \1c <=c m' by apply: cge1; fprops.
have p1: forall z, ordinalp z -> (\aleph z) <=c ((\aleph z) ^c m').
move=> z oz; move: (CIS_aleph oz) => iz; move: (iz) => [cz _].
apply: cpow_Mle1 => // coz.
have ipx: infinite_c (x^c m') by apply: (CIS_pow).
move: (ap) => [lexy _].
have cxy := (cpow_Mleeq m' (proj1 ap) (aleph_nz on)).
move: (icy) => [cy _]; move:(cy) => [oy _].
apply: cleA; last first.
by apply: cprod_inf4 => //; [apply: p1 | apply:CIS_pow].
case: (cleT_el cy cm') => cmx.
have im:= (ge_infinite_infinite icy cmx).
have lex2:=(infinite_ge2 icx).
rewrite (infinite_power1_a lex2 (cleT lexy cmx) im).
rewrite (infinite_power1_a (cleT lex2 lexy) cmx im).
apply: cprod_M1le => //.
rewrite /cpow; fprops.
apply: (aleph_nz (OS_succ on)).
have ha: m' /regular_cardinalP [_ ->].
have hb:= (infinite_power7b icy ha).
apply: (cleT hb); apply: (cleT (csum_pr1 (Lg y (functions m')))).
rewrite /csumb; bw; set f := Lg _ _.
have df: domain f = y by rewrite /f; bw.
rewrite - df /f; apply:csum_of_small_b1.
split; [ fprops | hnf; bw; move =>i ix; bw].
rewrite -/(cpow i m') - cpowcl.
case: (equal_or_not (cardinal i) \0c) => iz.
rewrite iz (cpow0x m'nz);apply: czero_least; rewrite /cpow; fprops.
by apply: (cpow_Mleeq _ _ iz); apply: (aleph_pr12d on); apply /(oltP oy).
Qed.
Lemma infinite_power2_bis x (y:= cnext x) m:
infinite_c x -> m <> \0c ->
y ^c m = (x ^c m) *c y.
Proof.
move=> ix mnz; rewrite /y;move: (ord_index_pr1 ix)=> [on <-].
rewrite (cnextE on); apply: (infinite_power2 on mnz).
Qed.
Lemma infinite_power3 n m (x:=\aleph n):
natp n -> m <> \0c ->
x ^c m = (\2c ^c m) *c x.
Proof.
move=> nN mz.
set m':= cardinal m.
have cm': cardinalp m' by rewrite /m'; fprops.
have m'nz: m' <> \0c by dneg cmz; move: (card_nonempty cmz).
have ->: \2c ^c m = \2c ^c m' by rewrite /m';apply: cpow_pr; fprops.
have ->: x ^c m = x ^c m' by rewrite /m';apply: cpow_pr; fprops.
rewrite /x; clear x.
case: (finite_dichot cm') => fm.
have mN: inc m' Nat by apply /NatP.
have on:=(ordinal_hi OS_omega nN).
have io:=(CIS_aleph on).
rewrite (cpow_inf io mN m'nz) cprodC.
symmetry; apply: cprod_inf => //; last by apply: cpow2_nz.
apply: finite_le_infinite => //; bw.
apply /NatP; apply: NS_pow; fprops.
have io: infinite_c omega0 by rewrite - aleph0E; apply: CIS_aleph; fprops.
have pa: \2c <=c omega0 by apply: infinite_ge2.
have onz:= omega_nz.
move: n nN; apply: Nat_induction.
rewrite aleph0E.
have le1: omega0 <=c m' by split => //;[ apply: CS_omega|apply: omega_limit3].
have le2:= (cleT le1 (proj1 (cantor cm'))).
rewrite infinite_power1_a // cprod_inf //.
apply: (ge_infinite_infinite io le2).
move=> n nN hrec.
rewrite succ_of_finite; last by apply /NatP.
have on:= (ordinal_hi OS_omega nN).
rewrite (infinite_power2 on m'nz) hrec - cprodA.
have pc := proj1 (aleph_pr10c on).
move: (cprod_inf pc (CIS_aleph (OS_succ on)) (aleph_nz on)).
by rewrite cprodC; move => ->.
Qed.
Lemma aleph_pow_prop1: (\aleph \1c) ^c aleph0 = \aleph \1c ->
forall n, natp n -> n <> \0c -> (\aleph n) ^c aleph0 = \aleph n.
Proof.
move => H0 n nN nz.
move: (cpred_pr nN nz) => [ cp ->]; move: (cpred n) cp; clear n nN nz.
apply: Nat_induction; first by rewrite succ_zero.
move => n nN.
rewrite (succ_of_Nat (NS_succ nN)) (succ_of_Nat nN) => Hrec.
have on :=(ordinal_hi OS_omega nN).
have osn := (OS_succ on).
rewrite (infinite_power2 osn omega_nz) Hrec cprodC cprod_inf //.
- by apply: aleph_le_lec; apply /oleSSP; apply: (oleS on).
- exact: (CIS_aleph (OS_succ osn)).
- exact: (aleph_nz osn).
Qed.
Lemma infinite_power4 a (b:= \2c ^c a): infinite_c a ->
[/\ b ^c a = b, b ^c a c ^c a = c -> b <=c c) &
(forall c, infinite_c c -> c ^c a b <=c c)].
Proof.
move=> ica.
have anz: a <> \0c by apply: infinite_nz.
have ib: infinite_c b by apply: infinite_powerset.
have p1: b ^c a = b by rewrite/b - cpow_pow csquare_inf.
have p3: (forall c, \2c <=c c -> c ^c a = c -> b <=c c).
move =>c c2 cp.
have cc:=proj32 c2.
case: (cleT_el (proj1 ib) cc) => //; move=> [le1 ne1].
move: (infinite_power1 c2 le1 ica); rewrite cp -/b //.
have p2: b ^c a h; move: (proj1 h) => le1.
move: (infinite_nz ib) => bnz.
have isc: infinite_c (cnext b) by apply: (ge_infinite_infinite ib le1).
by rewrite cprodC (cprod_inf le1 isc bnz).
split => //.
move=> c ic; rewrite (infinite_power2_bis ic anz) => ha.
have c1: cardinalp (c ^c a) by fprops.
have c2 := (CS_cnext (proj1 ic)).
case: (cleT_el c2 c1) => h.
have ip: infinite_c (c ^c a) by apply: CIS_pow2.
by move: (cleNgt (cprod_inf1 h ip) ha).
move: (cnext_pr4 (proj1 ic) h) => h1.
apply: (p3 _ (infinite_ge2 ic)).
apply: cleA => //; apply: (cpow_Mle1 (proj32 h1) anz).
Qed.
Lemma infinite_power5 n p m (x:=\aleph n) (y:= \aleph (n +o p)):
ordinalp n -> ordinalp p -> m <> \0o ->
cardinal p <=c m ->
y ^c m = (x ^c m) *c (y ^c (cardinal p)).
Proof.
move=> on op mnz cpm.
have cm := (proj32 cpm).
have ca: cardinalp (x ^c m) by rewrite /cpow; fprops.
pose hyp p:= cardinal p <=c m ->
\aleph (n +o p) ^c m = x ^c m *c \aleph (n +o p) ^c (cardinal p).
case:(least_ordinal6 hyp op); first by apply.
set q :=least_ordinal _ _; move=> [oq pb] [] => pa.
have xnz: x <> \0c by apply: aleph_nz.
move: (pa); rewrite - {1} (card_card cm) => pa'.
case: (ordinal_trichot oq) => h.
rewrite h cardinal_set0 (osum0r on) cpowx0 cprod1r //.
move:h=> [r or qv].
rewrite qv - osum2_succ //.
have rq1: inc r q by rewrite qv; fprops.
have cq:= (cleT (sub_smaller (ordinal_transitive oq rq1)) pa).
move: (pb _ rq1 cq).
set y1 := \aleph (n +o r); set y2 := \aleph (osucc (n +o r)).
have onr: ordinalp (n +o r) by fprops.
move: (infinite_power2 onr mnz); rewrite -/y1 -/y2 => r1 r2.
have osnr: ordinalp (osucc (n +o r)) by fprops.
have cy1m: cardinalp (y1 ^c m) by rewrite /cpow; fprops.
have icy2: infinite_c y2 by apply: CIS_aleph.
have icy1: infinite_c y1 by apply: CIS_aleph.
have icx: infinite_c x by apply: CIS_aleph.
have y1nz: y1 <> \0c by apply: aleph_nz.
have y2nz: y2 <> \0c by apply: aleph_nz.
move: (icy1) (icy2) (icx) => [cy1 _ ] [cy2 _] [cx _].
have xx: x <=c x by fprops.
have y1y1: y1 <=c y1 by fprops.
have y2y2: y2 <=c y2 by fprops.
have le1: x ^c m <=c y1 ^c m.
have xy1: x <=c y1.
by apply: aleph_le_lec; apply (osum_Mle0 on or).
by apply: cpow_Mleeq.
have le0: y1 <=c y2.
by apply: aleph_le_lec; exact (proj1 (oltS (OS_sum2 on or))).
have le2: y1 ^c m <=c y2 ^c m by apply: cpow_Mleeq.
have paa: x <=c x ^c m by apply: cpow_Mle1 => //.
have lexx: y2 ^c (osucc r) <=c y2 ^c m.
by rewrite - qv - cpowcr - (cpowcr _ m);exact (cpow_Meqle y2nz pa').
have icxm:= (ge_infinite_infinite icx paa).
have icy1m:= (ge_infinite_infinite icxm le1).
have icy2m:= (ge_infinite_infinite icy1m le2).
have y1mnz: y1 ^c m <> \0c by apply:(cpow_nz y1nz).
have xmnz: x ^c m <> \0c by apply: (cpow_nz xnz).
have saux2: y2 ^c cardinal (osucc r) = y2 ^c (osucc r)
by apply: cpow_pr; fprops.
case: (cleT_ee cy1m cy2) => r3.
move: (cprod_inf r3 icy2 y1mnz).
rewrite cprodC; move=> h; rewrite h in r1.
rewrite r1; rewrite r1 in lexx.
rewrite saux2 (cleA lexx (cpow_Mle1 cy2 (@osucc_nz r))).
have r6: x ^c m <=c y2 by rewrite -r1; apply:cleT le1 le2.
by rewrite cprodC (cprod_inf r6 icy2 xmnz).
move: (cprod_inf r3 icy1m y2nz) => r4.
rewrite r4 in r1.
have saux: y1 ^c cardinal r = y1 ^c r by apply: cpow_pr; fprops.
have r6: y2 ^c (osucc r) <> \0c by apply: (cpow_nz y2nz).
case: (equal_or_not (x ^c m) (y1 ^c m)) => r7.
rewrite r7 -r1.
by rewrite saux2 (cprod_inf lexx icy2m r6).
have r8: x ^c m h.
have it: infinite_c (y1 ^c r)
by apply: (ge_infinite_infinite icxm h).
move: (cprod_inf h it xmnz); rewrite cprodC => xx1.
by rewrite r2 - xx1 saux.
have nzyr: y1 ^c r <> \0c by apply: (cpow_nz y1nz).
by move:(cprod_inf h icxm nzyr) r2; rewrite saux => -> ww; case: r7.
have crr1:cardinal r <=c cardinal (osucc r).
apply: sub_smaller; rewrite /osucc; fprops.
move: (cpow_Mlele y1nz le0 crr1); rewrite saux saux2.
rewrite -r9 -r1 => le3; rewrite (cleA lexx le3) cprodC.
by rewrite (cprod_inf (cleT le1 le2) icy2m xmnz).
have onq:=(OS_sum2 on oq).
apply cleA; last first.
move: (CIS_pow (CIS_aleph onq) mnz) => r1.
have r0: x <=c \aleph (n +o q).
by apply: aleph_le_lec; apply osum_Mle0.
have r2: x ^c m <=c \aleph (n +o q) ^c m.
apply: (cpow_Mleeq _ r0 (aleph_nz on)).
apply: (cprod_inf4 r2 _ r1).
apply: cpow_Meqle => //; apply: (aleph_nz onq).
set E := (fun_image q (fun z => \aleph (n +o z))).
set f := Lg q (fun z : Set => \aleph (n +o z)).
have r2: E = range f by rewrite Lg_range.
have r1 : \aleph (n +o q) = \osup E.
move: (normal_ofs_compose aleph_normal (osum_normal on)) => [xa xb].
move: (xb _ h) => /= ->; congr (union _); set_extens; aw.
have fgf: fgraph f by rewrite /f; fprops.
have r3: forall i, inc i (domain f) -> \2c <=c Vg f i.
rewrite /f; bw; move=> i idf; bw; apply: infinite_ge2.
apply: CIS_aleph; apply: (OS_sum2 on (ordinal_hi oq idf)).
have r4: \aleph (n +o q) = csum f.
rewrite r1 r2 - csum_of_small_b4 //.
move=> a ad; exact: (proj32 (r3 _ ad)).
rewrite -r2 -r1; apply: CIS_aleph => //.
rewrite - r2 -r1 /f; bw.
have r5: q <=o n +o q by apply: osum_M0le.
apply:cleT (aleph_le_lec r5).
move: (ocle1 (aleph_pr6 oq)).
rewrite (card_card (CS_aleph oq)) //.
have r5: \aleph (n +o q) <=c cprod f.
rewrite r4; apply: compare_sum_prod2 => //.
move=> i idf; move: (r3 _ idf) => [_ c _]; fprops.
move: (cpow_Mleeq m r5 (aleph_nz onq)).
rewrite cpow_prod {1} /f; bw.
rewrite /cprodb.
have ->: (Lg q (fun i : Set => Vg f i ^c m)) =
Lg q (fun t => x ^c m *c \aleph (n +o t) ^c (cardinal t)).
apply: Lg_exten; move=> t tq.
have tq1: t : x ^c (m *c q) = x ^c m.
have icm:= (ge_infinite_infinite icq pa).
move: (cprod_inf pa icm (infinite_nz icq)).
by rewrite cprod2cr => ->.
set f2:= \aleph (n +o q) ^c (cardinal q).
set ff:= (fun i : Set => \aleph (n +o i) ^c (cardinal i)).
move => r6.
have: cprod (Lg q ff) <=c f2 ^c (cardinal q).
rewrite cpowcr - cpow_pr2/cst_graph.
apply: cprod_increasing; bw.
move=> t tq; rewrite {1} (LVg_E ff tq) {1} (LVg_E _ tq).
have [tq1 _]: t : f2 ^c (cardinal q) = f2.
by rewrite /f2 - cpow_pow; congr cpow; apply: csquare_inf.
move=> r7; apply: (cleT r6); apply: cprod_Mlele => //; fprops.
Qed.
Lemma infinite_power5' n p m (x:=\aleph n) (y:= \aleph (n +o p)):
ordinalp n -> natp p -> m <> \0o ->
cardinal p <=c m ->
y ^c m = (x ^c m) *c y.
Proof.
move => pa pN pd pe.
have pb:= (ordinal_hi OS_omega pN).
have pb': natp (cardinal p) by rewrite (card_nat pN).
case: (equal_or_not p \0c) => pz.
have ix:= CIS_aleph pa.
have le1: x <=c x ^c m by apply:(cpow_Mle1 (proj1 ix) pd).
have ipo:= (ge_infinite_infinite ix le1).
by rewrite /y pz (osum0r pa) -/x (cprod_inf le1 ipo (infinite_nz ix)).
have iy:= CIS_aleph (OS_sum2 pa pb).
have pnz:cardinal p <> \0c by apply:card_nonempty0.
by rewrite (infinite_power5 pa pb pd pe) -/x -/y (cpow_inf iy pb' pnz).
Qed.
Lemma infinite_power5'' n p m (x:=\aleph n) (y:= \aleph (n +o p)):
ordinalp n -> natp p -> infinite_c m ->
y ^c m = (x ^c m) *c y.
Proof.
move => pa pb pc.
move:(Nat_hi pb); rewrite - (card_nat pb) => pd.
exact:(infinite_power5' pa pb (infinite_nz pc) (finite_le_infinite pd pc)).
Qed.
Lemma infinite_power6 p m (y:= \aleph p):
ordinalp p -> m <> \0o ->
cardinal p <=c m ->
(infinite_c m \/ p <> \0o) ->
y ^c m = (\2c ^c m) *c (y ^c (cardinal p)).
Proof.
move=> op mz cpm dc.
have cm := proj32 cpm.
move: (infinite_power5 OS0 op mz cpm).
rewrite (osum0l op) -/y aleph0E; move => ->.
have pa:= CIS_omega.
have aux:=(infinite_ge2 pa).
case: (finite_dichot cm) => fm; last first.
move/infinite_c_P2:(fm) => fm'.
by rewrite (infinite_power1_a aux fm' fm).
case: dc => pz; first by case: (infinite_dichot1 fm pz).
have mb: natp m by apply /NatP.
have mpb: natp (cardinal p) by apply (NS_le_nat cpm mb).
rewrite (cpow_inf pa mb mz).
have cpz: cardinal p <> \0o by move=> h; move: (card_nonempty h).
have iy:= (CIS_aleph op).
have le1: omega0 <=c \aleph p.
by rewrite - aleph0E; apply: aleph_le_lec; by apply: ozero_least.
have le2: \2c ^c m <=c \aleph p.
apply: cleT le1.
apply: finite_le_infinite => //;apply /NatP; apply: NS_pow; fprops.
move: (cpow_inf iy mpb cpz).
have -> : \aleph p ^c cardinal p = \aleph p ^c p by apply: cpow_pr; fprops.
move ->.
rewrite cprodC; rewrite (cprod_inf le1 iy omega_nz).
rewrite cprodC; rewrite (cprod_inf le2 iy) //.
apply: cpow2_nz.
Qed.
Lemma infinite_power6_0 p m (y:= \aleph p):
ordinalp p -> infinite_c m -> cardinal p <=c m ->
y ^c m = (\2c ^c m) *c (y ^c (cardinal p)).
Proof.
move=> op icm cp.
have aux: (infinite_c m \/ p <> \0o) by left.
by rewrite (infinite_power6 op (infinite_nz icm) cp aux).
Qed.
Lemma infinite_power6_ct p m (y:= \aleph p):
ordinalp p -> infinite_c m -> cardinal p <=c omega0 ->
y ^c m = (\2c ^c m) *c (y ^c aleph0).
Proof.
move => ha hb hc.
move /infinite_c_P2: (hb) => hb'; move: (cleT hc hb') => hd.
rewrite (infinite_power6_0 ha hb hd).
case: (finite_dichot (proj31 hc)) => fp.
case: (equal_or_not p \0c) => epz.
move: (infinite_powerset hb) => he.
rewrite /y epz cardinal_set0 cpowx0 /aleph0 aleph0E (cprod1r (proj1 he)).
rewrite(infinite_power1_b CIS_omega) - cpow_sum2 csum_inf //.
have nn: natp (cardinal p) by apply/NatP.
have cpz: cardinal p <> \0o by move=> h; move: (card_nonempty h).
rewrite (cpow_inf (CIS_aleph ha) nn cpz).
have pN: natp p by apply/NatP; exact :(ordinal_finite1 ha fp).
rewrite (infinite_power3 pN omega_nz) cprodA - cpow_sum2 csum_inf //.
by move/infinite_c_P2: fp => fp; rewrite - (cleA fp hc).
Qed.
Lemma infinite_power5_ex:
\aleph (omega1 +o omega0) ^c (\aleph \2o) =
(\2c ^c (\aleph \2o)) *c ((\aleph omega1) ^c aleph1)
*c (\aleph (omega1 +o omega0) ^c aleph0).
Proof.
have ha: ordinalp omega1 by exact: OS_aleph OS1.
have hb: ordinalp omega0 by exact OS_omega.
have hc:= (CIS_aleph OS2).
have hd:= (infinite_nz hc).
move: (aleph_le_lec (proj1 olt_02)).
rewrite aleph0E /aleph0 -{1 4} (card_card CS_omega) => he.
have hi:= (card_card(CS_aleph OS1)).
move: (aleph_le_lec (proj1 olt_12)); rewrite - hi => hf.
by rewrite (infinite_power5 ha hb hd he) (infinite_power6_0 ha hc hf) hi.
Qed.
Lemma infinite_power6_1 a: a
(\aleph a) ^c aleph1 =
(\aleph a) ^c aleph0 *c \2c ^c aleph1.
Proof.
move => ao.
have oa:= proj31_1 ao.
have coo: cardinalp (\aleph \1o) by apply: CS_aleph; fprops.
move: ao => /(ocle2P coo oa) ao.
rewrite /aleph0 - aleph0E.
move: (aleph_nz oa) => xnz.
apply: cleA.
rewrite (infinite_power6_0 oa (CIS_aleph OS1) (proj1 ao)) cprodC.
apply: cprod_Mlele; last by apply: cleR; fprops.
by apply: cpow_Meqle => //;apply: (aleph_pr10a OS0); rewrite osucc_zero.
have ioa:= (CIS_aleph oa).
apply: cprod_inf4.
- apply: cpow_Meqle => //; apply: aleph_le_lec; apply: ozero_least; fprops.
- apply: cpow_Mleeq; [ apply: finite_le_infinite | ]; fprops.
- apply: CIS_pow => //; apply: aleph_nz; fprops.
Qed.
Lemma infinite_power6_2 a: a
(\aleph a) ^c aleph2 =
(\aleph a) ^c aleph1 *c \2c ^c aleph2.
Proof.
move => ao.
have oa:= proj31_1 ao.
have coo: cardinalp aleph2 by apply: CS_aleph; fprops.
move: ao => /(ocle2P coo oa) ao.
have xnz:= (aleph_nz oa).
apply: cleA.
rewrite (infinite_power6_0 oa (CIS_aleph OS2) (proj1 ao)) cprodC.
apply: cprod_Mlele; last by apply: cleR; fprops.
by apply: cpow_Meqle => //;apply: (aleph_pr10a OS1); rewrite osucc_one.
move: (CIS_aleph oa) => ioa.
apply: cprod_inf4.
- apply: cpow_Meqle => //;apply: aleph_le_lec;apply: oge1; fprops.
- apply: cpow_Mleeq; [ apply: finite_le_infinite |];fprops.
- apply: CIS_pow => //; apply: aleph_nz; fprops.
Qed.
Lemma infinite_power6_3:
(\aleph omega0) ^c aleph1 =
(\aleph omega0) ^c aleph0 *c \2c ^c aleph1.
Proof.
apply: infinite_power6_1.
rewrite - aleph0E; apply: aleph_lt_lto; apply: olt_01.
Qed.
Lemma infinite_power6_4 a b:
infinite_o a -> a ordinalp b ->
(\aleph a) ^c (\aleph b) =
(\aleph a) ^c aleph0 *c \2c ^c (\aleph b).
Proof.
move => ioa a1 ob.
have oa:= proj31_1 a1.
have iob:= (CIS_aleph ob).
move: (a1) => /(ocle2P (CS_aleph OS1) oa).
rewrite - osucc_zero => ca; move: (aleph_pr10a OS0 ca) => ca1.
have ca2: cardinal a <=c \aleph b.
by apply: (cleT ca1); apply aleph_le_lec; apply: ozero_least.
rewrite (infinite_power6_0 oa iob ca2) cprodC.
suff: cardinal a = aleph0 by move ->.
rewrite /aleph0 - aleph0E; apply: cleA => //; rewrite aleph0E.
by move/(omega_P1 oa): ioa => /sub_smaller; rewrite (card_card CS_omega).
Qed.
Lemma infinite_power6_5 a b c :
ordinalp a -> ordinalp b ->
\aleph (\omega a) = c ^c (\aleph b) ->
b oa ob.
have la:=(aleph_limit oa).
have aux: infinite_c (\aleph (\aleph a)).
by apply: CIS_aleph; apply: OS_aleph.
have ->: c ^c \omega b =(cardinal c) ^c \omega b by apply:cpow_pr; fprops.
set C := cardinal c.
case: (equal_or_not C \1c) => eq1.
rewrite eq1 cpow1x =>h; move: aux; rewrite h; move: finite_1.
move => pa pb; case: (infinite_dichot1 pa pb).
case: (equal_or_not C \0c) => eq0.
rewrite eq0 cpow0x =>h. move: aux; rewrite h; move: finite_0.
move => pa pb; case: (infinite_dichot1 pa pb).
by case: (aleph_nz ob).
move: (cge2 (CS_cardinal c) eq0 eq1) => c2 h.
move: (power_cofinality5 c2 (CIS_aleph ob)).
rewrite - (f_equal cofinality h).
rewrite regular_initial_limit1 //.
move: (CIS_aleph oa) => ia.
move: (cofinality_small ia) => l1 l2.
exact: (aleph_ltc_lt ob oa (clt_leT l2 l1)).
Qed.
Lemma infinite_power6_6 n : ordinalp n ->
\2c ^c (\aleph omega0) = \aleph (\omega n) -> omega0 on h3; symmetry in h3.
exact (infinite_power6_5 on OS_omega h3).
Qed.
Lemma infinite_power6_5a a b : infinite_c b ->
\aleph omega1 = a ^c b -> b = aleph0.
Proof.
move => /ord_index_pr1; set n := ord_index b;move => [on <-] eq.
by move:(infinite_power6_5 OS1 on eq) => /olt1 ->; rewrite aleph0E.
Qed.
Definition gimel_fct x := x ^c (\cf x).
Lemma gimel_prop1 x: regular_cardinal x ->
\2c ^c x = gimel_fct x.
Proof.
by move=> /regular_cardinalP[ic xc]; rewrite /gimel_fct xc infinite_power1_b.
Qed.
Lemma gimel_prop2 x: infinite_c x ->
gimel_fct x <=c \2c ^c x.
Proof.
move=> ic; rewrite /gimel_fct - (infinite_power1_b ic).
move: (cofinality_small ic) => cg.
apply: cpow_Mlele => //; [ by apply: infinite_nz | apply: (cleR (proj1 ic))].
Qed.
Lemma infinite_power6_7a: \2c ^c aleph1 = aleph2 ->
\aleph omega0 ^c aleph1 = \aleph omega0 ^c aleph0.
Proof.
move => pa; move: infinite_power6_3; rewrite pa.
have pc: aleph2 <=c \aleph omega0 ^c aleph0.
have l1: aleph2 <=c \aleph omega0.
apply: aleph_le_lec; apply: ole_2omega.
have co:= proj32 l1.
apply: (cleT l1); apply: cpow_Mle1 => //; last by apply: omega_nz.
have i2:=(CIS_aleph OS2).
have i3:= (ge_infinite_infinite i2 pc).
by rewrite (cprod_inf pc i3 (infinite_nz i2)).
Qed.
Lemma infinite_power6_7b:
\2c ^c aleph1 = aleph2 ->
(\aleph omega0) ^c aleph0 <> \aleph omega1.
Proof.
move => pa pb.
move: (infinite_power6_7a pa); rewrite pb => aux; symmetry in aux.
rewrite - (aleph0E) in pb.
move: (infinite_power6_5 OS1 OS1 aux); by move => [].
Qed.
Lemma infinite_power6_7c:
\2c ^c aleph1 = aleph2 ->
\aleph omega1
\aleph omega1 ^c aleph1 = (\aleph omega0) ^c aleph0.
Proof.
set x1 := \aleph omega1.
set x2 := \aleph omega0 ^c aleph0.
move => pa [pb _].
have pc: \aleph omega0 <> \0c by apply: (aleph_nz OS_omega).
have x1nz: x1 <> \0c by apply: aleph_nz ; apply: OS_aleph; fprops.
have pd: aleph0 <=c aleph1.
rewrite /aleph0 - aleph0E;apply: aleph_le_lec; apply: (ozero_least OS1).
have pe: \aleph omega0 <=c x1.
by apply: aleph_le_lec; apply: (ocle).
have pf: x2 <=c x1 ^c aleph0 by apply: cpow_Mleeq.
symmetry;apply: cleA.
apply: (cleT pf); apply: cpow_Meqle => //; apply: aleph_nz.
have: x1 ^c \aleph \1o <=c x2 ^c \aleph \1o by apply: cpow_Mleeq.
move: (infinite_power6_7a pa); rewrite -/x2 ; move => <-.
rewrite - cpow_pow csquare_inf //;apply: CIS_aleph; fprops.
Qed.
Lemma infinite_power6_7d:
\aleph omega0
(\aleph omega0) ^c omega0 = \2c ^c omega0.
Proof.
move=> [h _ ].
move: (CIS_aleph OS_omega) => io.
apply: cleA; last first.
apply cpow_Mleeq;[ by apply: infinite_ge2 | fprops].
move: (cpow_Mleeq omega0 h (infinite_nz io)).
rewrite - cpow_pow csquare_inf //; apply: CIS_omega.
Qed.
Lemma infinite_power6_7e:
\aleph omega1 <=c \2c ^c omega0 ->
(gimel_fct (\aleph omega0) = \2c ^c aleph0
/\ gimel_fct (\aleph omega1) = \2c ^c aleph1).
Proof.
set o1 := \aleph \1o.
move => h; rewrite /gimel_fct.
have h1: \aleph omega0 <=c \aleph o1.
rewrite - aleph0E; apply: aleph_le_lec; apply: aleph_le_leo.
apply: ozero_least; fprops.
move: (cleT h1 h) => h2.
move: (regular_initial_limit1 (aleph_limit OS0)); rewrite aleph0E.
move: (regular_initial_limit1 (aleph_limit OS1)); rewrite -/o1.
move => -> ->.
have pa:= (CIS_aleph OS_omega).
rewrite (proj2 regular_omega).
move: (regular_cardinal_aleph1) => [pb].
rewrite (cofinality_card pb) -/o1; move => ->.
have cn2:=card2_nz.
split.
apply: cleA.
move: (cpow_Mleeq omega0 h2 (infinite_nz pa)).
rewrite - cpow_pow csquare_inf //; apply: CIS_omega.
apply: cpow_Mleeq => //; apply: finite_le_infinite => //; fprops.
move: (CIS_aleph (proj1 (proj1 pb))); rewrite -/o1 => io1.
have aux: (omega0 *c o1) = o1.
rewrite cprodC; apply: cprod_inf => //.
rewrite - aleph0E; apply: aleph_le_lec; apply: ozero_least; fprops.
apply: omega_nz.
apply: cleA.
move: (cpow_Mleeq o1 h (infinite_nz io1)).
by rewrite - cpow_pow aux.
apply: cpow_Mleeq => //; apply: finite_le_infinite => //; fprops.
Qed.
Lemma infinite_power6_7f:
\aleph omega0 [pa <-].
by rewrite (cofinality_card pa)(regular_initial_limit1 la).
Qed.
Lemma ord_sup_aleph x: limit_ordinal x ->
\csup (range (Lg x \aleph)) = \aleph x.
Proof.
move => lx.
have fgf: fgraph (Lg x \aleph) by fprops.
move: aleph_normal => [_ h]; rewrite (h _ lx).
congr (union _ ); set_extens t.
move /(range_gP fgf) ; bw;move => [z zb]; bw => ->.
apply /funI_P; ex_tac.
move => /funI_P [z za zb]; apply /(range_gP fgf) ; bw.
ex_tac; bw; ue.
Qed.
Lemma infinite_increasing_power1 X b:
ofg_Mle_leo X -> domain X = \omega b -> ordinalp b ->
limit_ordinal (\osup (range X)) ->
cprod (Lg (domain X) (fun z => \aleph (Vg X z))) =
\aleph (\osup (range X)) ^c \aleph b.
Proof.
move => px dx ob la.
set Y := Lg _ _.
have p1: fgraph Y by rewrite /Y; fprops.
have p2: infinite_c (domain Y) by rewrite /Y; bw; rewrite dx; apply CIS_aleph.
move: (increasing_sup_limit3 px la) => pb.
move: px => [fgx pa xi].
have p3: (forall a : Set, inc a (domain Y) -> \0c a adx; bw; apply: aleph_nz1;apply: pa.
have p4: forall u v, inc u (domain Y) -> inc v (domain Y) -> u <=o v ->
Vg Y u <=c Vg Y v.
rewrite /Y; bw => u v ud vd uv; bw; apply: aleph_le_lec.
apply: (xi _ _ ud vd uv).
rewrite (infinite_increasing_power p1 p2 p3 p4).
by rewrite /Y; bw; rewrite pb dx.
Qed.
Lemma infinite_increasing_power2 X b:
ofg_Mlt_lto X -> domain X = \omega b -> ordinalp b ->
cprod (Lg (domain X) (fun z => \aleph (Vg X z))) =
\aleph (\osup (range X)) ^c \aleph b.
Proof.
move=> p1 p3 p4.
have lb: limit_ordinal (domain X) by rewrite p3; apply: aleph_limit.
move: (increasing_sup_limit2 p1 lb) => la.
move: ( ofg_Mlt_lto_p3 p1 lb) => p2.
by apply: infinite_increasing_power1.
Qed.
Lemma ord_sup_aleph_sum x: ordinalp x ->
\csup (range (Lg omega0 (fun z=> \aleph (x +o z)))) =
\aleph (x +o omega0).
Proof.
move => ox.
move: (normal_ofs_compose aleph_normal (osum_normal ox)) => [_ xb].
by move: (xb _ omega_limit) => /= ->; rewrite Lg_range.
Qed.
Lemma cprod_inf_eq x y i:
fgraph x -> fgraph y -> (domain x = domain y) ->
inc i (domain x) -> (Vg x i) <> \0c -> Vg y i <> \0c ->
(exists j, [/\ inc j (domain x), j <> i, infinite_c (Vg x j),
Vg x i <=c Vg x j & Vg y i <=c Vg x j]) ->
(forall j, inc j (domain x) -> j = i \/ Vg x j = Vg y j) ->
cprod x = cprod y.
Proof.
move => pa pb pc pd pe pf [j [qa qb qc qd qe]] ph.
set x' := Lg (domain x) (fun z => Yo (z = i) (Vg x j) (Vg x z)).
set y' := Lg (domain y) (fun z => Yo (z = i) (Vg y j) (Vg y z)).
have svj: Vg x j = Vg y j by case: (ph _ qa) => // aux; by case: qb.
have sp: x' = y'.
rewrite /x' /y' -pc; apply: Lg_exten => k kdx; bw; Ytac xeq; Ytac0 => //.
case: (ph _ kdx) => // aux.
suff: forall z, fgraph z -> inc i (domain z) -> Vg z i <> \0c ->
inc j (domain z) -> j <> i -> infinite_c (Vg z j) -> Vg z i <=c Vg z j ->
cprod z = cprod (Lg (domain z)(fun t => Yo (t = i)(Vg z j) (Vg z t))).
move => aux.
rewrite (aux x pa pd pe qa qb qc qd) -/ x'.
rewrite pc in pd qa; rewrite svj in qc qe.
by rewrite (aux y pb pd pf qa qb qc qe) -/ y' sp.
move => z fgz idz jdz znz jni iv jv.
set z1 := (Lg (domain z) (fun t => Yo (t = i) (Vg z j) (Vg z t))).
move: (setC1_K idz); set j1 := (domain z) -s1 i => pA.
symmetry in pA.
have aux1: ~ inc i j1 by move /setC_P => [_] /set1_P; case.
rewrite (induction_prod1 pA aux1).
have fgz1: fgraph z1 by rewrite /z1; fprops.
have pN: domain z1 = j1 +s1 i by rewrite /z1; bw.
rewrite (induction_prod1 pN aux1).
have fg2: fgraph (restr z j1) by fprops.
have fg3: fgraph (restr z1 j1) by fprops.
have pC: sub j1 (domain z) by move => t /setC1_P [].
have pD: sub j1 (domain z1) by rewrite /z1; bw.
have jj: inc j j1 by apply /setC1_P; split => //.
have dr1: (domain (restr z j1)) = j1 by bw.
have dr2: (domain (restr z1 j1)) = j1 by bw.
have jdz1: inc j (domain (restr z j1)) by ue.
move: (setC1_K jdz1); set j2 := _ -s1 j => pE.
symmetry in pE.
have aux2: ~ inc j j2 by move /setC1_P=> [_].
rewrite (induction_prod1 pE aux2).
rewrite dr1 -dr2 in pE.
rewrite (induction_prod1 pE aux2) - cprodA - cprodA.
have sc: sub j2 j1 by move => t /setC1_P []; rewrite dr1.
move: (sub_trans sc pC) => sd.
rewrite (double_restr _ sc) (double_restr _ sc).
rewrite /z1; bw; Ytac0; Ytac0; apply:f_equal2.
apply:f_equal; apply: fgraph_exten; fprops; bw.
move=> k kj2.
have k2: inc k (domain z) by apply: sd.
by bw;Ytac ki; [ move: (sc _ kj2); rewrite ki |].
by rewrite (cprod_inf jv iv jdz) (csquare_inf iv).
Qed.
Lemma infinite_prod_pA:
cprodb Nat csucc = cprodb Nat (fun z => (csucc (csucc z))).
Proof.
set j := Nat -s1 \0c.
set f := (Lg Nat csucc).
have fgf: fgraph f by rewrite /f; fprops.
have sj:sub j (domain f) by rewrite /f; bw;apply sub_setC.
have sj1: sub (singleton \0c) Nat by move=> t /set1_P ->; apply:NS0.
have f1: (forall i, inc i ((domain f) -s j) -> (Vg f i) = \1c).
rewrite /f/j; bw => i /setC_P [iN] /setC_P nv; bw.
rewrite - succ_zero; ex_middle aux; case: nv;split => //.
by dneg i0; move /set1_P: i0 => ->.
rewrite /cprodb (cprod_one_unit sj f1).
have ->: cprodb j (Vg f) = cprodb j csucc.
by rewrite /f;apply: cprodb_exten => i ii; bw; move/setC1_P: ii => [].
apply:cprod_Cn2; split => //.
+ move => t tN; apply /setC_P;split; first by apply:NS_succ.
move /set1_P; apply: succ_nz.
+ move => u v uN vN;apply: succ_injective1; fprops.
+ move => y /setC1_P [yn ynz].
by move: (cpred_pr yn ynz) => [pa pb]; exists (cpred y).
Qed.
Lemma infinite_prod_pB: cprodb Nat csucc = \2c ^c omega0.
Proof.
move:CIS_omega => io.
have : cprodb Nat csucc <=c cprod (cst_graph omega0 omega0).
rewrite /cst_graph; apply: cprod_increasing; bw; fprops.
move=> x xN; bw; apply: finite_le_infinite => //.
by apply /NatP; apply: NS_succ.
rewrite cpow_pr2 (infinite_power1_b io) => le1.
apply: cleA => //.
rewrite - cpow_pr2.
rewrite infinite_prod_pA.
rewrite /cst_graph;apply: cprod_increasing; bw; fprops.
move=> x xN; bw.
have sxb: natp (csucc x) by fprops.
have cs: cardinalp (csucc \0c) by apply: CS_succ.
have cs0: cardinalp (\0c) by fprops.
rewrite - succ_one - succ_zero; apply /(cleSSP cs); fprops.
move: (CS_nat xN) => h.
apply /(cleSSP CS0 h); apply: (czero_least h).
Qed.
Lemma cprod_An1 a b f: ordinalp a -> ordinalp b ->
cprodb (a +o b) f =
cprodb a f *c cprodb b (fun z => f (a +o z)).
Proof.
move => oa ob.
rewrite {1} /cprodb; set g := Lg (a +o b) f.
have fgg: fgraph g by rewrite /g; fprops.
have sab:= proj33 (osum_Mle0 oa ob).
move: (is_partition_with_complement sab).
have -> : a +o b = domain g by rewrite /g; bw.
move=> pfa.
rewrite (cprod_An pfa).
rewrite /partition_with_complement; bw; symmetry; apply: cprod2_pr.
set ff := fun l: Set => _.
have ->: cprodb a f = ff C0.
by rewrite /ff /g; bw; apply: cprodb_exten => s sf /=; bw;apply: sab.
suff: (cprodb b (fun z => f (a +o z))) = ff C1
by move => ->; apply doubleton_fam_canon.
rewrite /ff /g;bw.
have -> : cprodb ((a +o b) -s a)(Vg (Lg (a +o b) f)) = cprodb ((a +o b) -s a) f.
apply: cprodb_exten => i /setC_P[ii _]; bw.
symmetry;apply:cprod_Cn2; split.
+ move => t tb; apply/setC_P; rewrite (osum_rec_def oa ob);split.
apply /setU2_P; right; apply/funI_P; ex_tac.
by move=> /(oltP oa) h1; move:(oltNge h1(osum_Mle0 oa (ordinal_hi ob tb))).
+ move => u v uo vo su.
move: (ordinal_hi ob uo) (ordinal_hi ob vo) => ou ov.
exact (osum2_simpl ou ov oa su).
+ by rewrite (osum_rec_def oa ob); move => y /setC_P [/setU2_P] [] // /funI_P.
Qed.
Lemma infinite_prod_pB1: union (range (Lg Nat csucc)) = omega0.
Proof.
rewrite Lg_range; set_extens t.
move => /setU_P [z tz /funI_P [u u1 uv]].
rewrite uv in tz; exact:(NS_inc_nat (NS_succ u1) tz).
move => tu; apply/setU_P; exists (osucc t); fprops.
rewrite - (succ_of_Nat tu); apply /funI_P; ex_tac.
Qed.
Lemma infinite_prod_pB2: (*alt proof *)
cprodb Nat csucc = \2c ^c omega0.
Proof.
set x := (Lg Nat csucc).
have fgf: fgraph x by rewrite / x; fprops.
have icy: infinite_c (domain x) by rewrite /x; bw; apply: CIS_omega.
have pa: cardinal_pos_fam x.
move;rewrite /x; bw; move=> a adx; rewrite /x; bw;apply: succ_positive.
have pb: fg_Mle_lec x.
move;rewrite /x; bw; move => a b aN bN [_ _ ab]; bw.
move:(CS_nat aN) (CS_nat bN) => ca cb.
apply /(cleSSP ca cb); split => //.
rewrite /cprodb (infinite_increasing_power fgf icy pa pb).
rewrite /x infinite_prod_pB1; bw.
rewrite infinite_power1_b //;exact CIS_omega.
Qed.
Lemma infinite_prod_pC:
cprodb Nat \aleph = (\aleph omega0) ^c omega0.
Proof.
set x := (Lg Nat \aleph).
have fgf: fgraph x by rewrite / x; fprops.
have icy: infinite_c (domain x) by rewrite /x; bw; apply: CIS_omega.
have pa: cardinal_pos_fam x.
move;rewrite /x; bw; move=> a adx; rewrite /x; bw; apply: aleph_nz1.
exact (ordinal_hi OS_omega adx).
have pb: fg_Mle_lec x.
move;rewrite /x; bw; move => a b aB bB ab; bw;exact (aleph_le_lec ab).
rewrite /cprodb (infinite_increasing_power fgf icy pa pb).
rewrite /x (ord_sup_aleph omega_limit); bw.
Qed.
Lemma infinite_prod_pD (o2 := omega0 +o omega0):
cprodb o2 \aleph = (\aleph o2) ^c omega0.
Proof.
set oo := (\aleph o2).
move: OS_omega => ioo.
apply: cleA.
have -> : oo ^c omega0 = oo ^c (omega0 +o omega0).
by rewrite - cpowcr cardinal_omega2 cpowcr.
have oo2: ordinalp o2 by apply: OS_sum2.
rewrite - cpow_pr2 /cst_graph; apply: cprod_increasing; bw; fprops.
by move=> x xB;bw; apply: aleph_le_lec; apply/(oleP oo2); apply:setU1_r.
set p1:= cprod (Lg omega0 (fun z => (\aleph (omega0 +o z)))).
set x := (Lg omega0 (fun z : Set => \aleph (omega0 +o z))).
have fgf: fgraph x by rewrite / x; fprops.
have icy: infinite_c (domain x) by rewrite /x; bw; apply: CIS_omega.
have pa: cardinal_pos_fam x.
move;rewrite /x; bw; move=> a adx; rewrite /x; bw; apply: aleph_nz1.
by apply: OS_sum2 => //; apply(ordinal_hi ioo adx).
have pb: fg_Mle_lec x.
move;rewrite /x; bw; move => a b aB bB ab; bw.
exact (aleph_le_lec (osum_Meqle ab ioo)).
move: (infinite_increasing_power fgf icy pa pb).
have ->: union (range x) = oo by apply: (ord_sup_aleph_sum ioo).
rewrite {2} /x; bw; move => <-.
move: (cprod_An1 \aleph ioo ioo) => ->.
have fg1: fgraph (Lg omega0 \aleph) by fprops.
rewrite cprodC; apply: cprod_M1le; rewrite /cprod;fprops.
apply /cprod_nzP; hnf;bw => i id; bw; apply:(aleph_nz(ordinal_hi ioo id)).
Qed.
Lemma infinite_prod_pE (o2 := omega1 +o omega0):
cprodb o2 \aleph = (\aleph o2) ^c aleph1.
Proof.
set o1 := \aleph \1o.
have ico:= CIS_omega.
have ioo:= OS_omega.
have oo1: ordinalp o1 by apply: OS_aleph; apply: OS1.
move: (CIS_aleph OS1) => io1.
move /infinite_c_P2: (io1) => io2.
have px: cprod (Lg o1 \aleph) = (\aleph o1 ^c o1) ^c omega0.
rewrite - cpow_pow (cprod_inf io2 io1 omega_nz) //.
set x := (Lg o1 \aleph).
have qa: (fgraph x) by rewrite /x; fprops.
have qb: (infinite_c (domain x)) by rewrite /x; bw.
have qc: cardinal_pos_fam x.
move; rewrite /x; bw => a ao; bw; apply: (aleph_nz1 (ordinal_hi oo1 ao)).
have qd: fg_Mle_lec x.
move; rewrite /x; bw; move => a b ax bx ab; bw.
exact (aleph_le_lec ab).
move: (infinite_increasing_power qa qb qc qd).
rewrite /x; rewrite (ord_sup_aleph (aleph_limit OS1)); bw.
have pa: cprod (Lg omega0 (fun z => (\aleph (o1 +o z)))) =
(\aleph o2) ^c omega0.
set x := (Lg omega0 (fun z => (\aleph (o1 +o z)))).
have qa: (fgraph x) by rewrite /x; fprops.
have qb: (infinite_c (domain x)) by rewrite /x; bw.
have qc: cardinal_pos_fam x.
move; rewrite /x; bw => a ao; bw; apply: aleph_nz1.
by apply: OS_sum2 => //; apply (ordinal_hi ioo ao).
have qd: fg_Mle_lec x.
move;rewrite /x; bw; move => a b ax bx ab; bw.
exact (aleph_le_lec (osum_Meqle ab oo1)).
move: (infinite_increasing_power qa qb qc qd).
by rewrite /x; move => ->; bw; rewrite (ord_sup_aleph_sum oo1).
have <- : cprod
(Lg omega0 (fun z => (\aleph (o1 +o z) ^c o1))) = \aleph o2 ^c o1.
move: pa; set f:= Lg omega0 _.
have pb: fgraph f by rewrite /f; fprops.
move: (cpow_prod o1 f); rewrite /cprodb.
have -> : (Lg (domain f) (fun i => Vg f i ^c o1)) =
(Lg omega0 (fun z => \aleph (o1 +o z) ^c o1)).
rewrite /f; bw; apply: Lg_exten => t te; bw.
move => <- ->.
rewrite - cpow_pow cprodC (cprod_inf io2 io1 omega_nz) //.
suff -> //: cprodb o2 \omega = (cprodb (o1 +o omega0) \omega).
suff: cprodb omega0 (fun z => \aleph (o1 +o z) ^c o1) =
cprodb omega0 (fun z => \aleph o1 ^c o1 *c \aleph (o1 +o z)).
rewrite -/(cprodb omega0 _); move => ->.
rewrite - prod_of_prods (cprod_An1 \aleph oo1 ioo) /cprodb cpow_pr2 px //.
rewrite /cprodb;set l1:= Lg _ _; set l2 := Lg _ _.
have la: fgraph l1 by rewrite /l1; fprops.
have lb: fgraph l2 by rewrite /l2; fprops.
have lc: (domain l1 = domain l2) by rewrite /l1 /l2; bw.
have ld: inc \0o (domain l1) by rewrite /l1; bw; apply /NatP; fprops.
have oz: inc \0c omega0 by apply:NS0.
have aux1: \aleph o1 ^c o1 <> \0c.
apply: infinite_nz; apply: CIS_pow2; apply: CIS_aleph; fprops.
have le: (Vg l1 \0c) <> \0c by rewrite /l1; bw; rewrite (osum0r oo1).
have lf: (Vg l2 \0c) <> \0c.
rewrite /l2; bw.
by rewrite (osum0r oo1); apply: cprod2_nz => //; apply: aleph_nz.
have lg: (exists j, [/\ inc j (domain l1), j <> \0c, infinite_c (Vg l1 j),
Vg l1 \0o <=c Vg l1 j & Vg l2 \0o <=c Vg l1 j]).
have oo: inc \1o omega0 by apply:NS1.
have d1: domain l1 = omega0 by rewrite /l1; bw.
have i1d: inc \1o (domain l1) by ue.
have le1: \aleph (o1 +o \0o) <=c \aleph (o1 +o \1o).
apply: aleph_le_lec;apply: osum_Meqle; try apply: ozero_least; fprops.
exists \1o; split => //.
- fprops.
- rewrite /l1; bw; apply: CIS_pow2; apply: CIS_aleph; fprops.
- rewrite /l1; bw; apply: cpow_Mleeq => //.
apply: aleph_nz; apply: OS_sum2; fprops.
rewrite /l1/l2; bw.
rewrite (osum0r oo1).
set w := \aleph (o1 +o \1o) ^c o1.
have sa: \aleph o1 <> \0c by apply: aleph_nz; fprops.
have sb: \aleph o1 ^c o1 <=c w.
apply: cpow_Mleeq => //; apply: aleph_le_lec.
apply: osum_Mle0; fprops.
have sc: \aleph o1 <=c \aleph o1 ^c o1.
have co1: cardinalp (\aleph o1) by apply CS_aleph.
apply: cpow_Mle1 => //;apply: aleph_nz => //; fprops.
move: (ge_infinite_infinite (CIS_aleph oo1) sc) => i2.
exact: (cleT (cprod_inf1 sc i2) sb).
have lh: (forall j, inc j (domain l1) -> j = \0o \/ Vg l1 j = Vg l2 j).
rewrite /l1 /l2; bw; move => j jb.
case: (equal_or_not j \0o) => jnz;[by left | right; bw].
move: (card_nat jb) => pd.
have pb: \aleph \1o <> \0o by apply: aleph_nz; fprops.
have pc: cardinal j <=c \aleph \1o.
rewrite pd; apply: (cleT _ io2).
by apply: finite_le_infinite => //; apply /NatP.
have pe: infinite_c (\aleph (o1 +o j)).
apply: CIS_aleph; apply: OS_sum2 => //;apply: (ordinal_hi ioo jb).
move: (infinite_power5 oo1 (ordinal_hi ioo jb) pb pc).
have ->: \omega (o1 +o j) ^c cardinal j = \omega (o1 +o j) ^c j.
apply: cpow_pr; fprops.
by rewrite - /omega1 -/o1 (cpow_inf pe jb jnz).
by rewrite (cprod_inf_eq la lb lc ld le lf lg lh).
Qed.
Lemma infinite_prod3 X c (Y:= Lg (domain X) (fun z => \aleph (Vg X z)))
(b:= omega0 ^o c):
\0o ofg_Mlt_lto X -> domain X = b ->
(cprod Y) = (\csup (range Y)) ^c (cardinal b).
Proof.
move => cp ax db.
have oc:= proj32_1 cp.
have lb: limit_ordinal b by apply: indecomp_limit2.
move: (lb); rewrite -db => lb1.
move: (increasing_sup_limit4 ax lb1) (aleph_sum_pr6 ax lb1); rewrite -/Y.
set a := \osup (range X); move=> [la sra sav] pa.
move: ax => [gx ofx si]; rewrite sav.
apply: cleA; first by apply : infinite_increasing_power_bound1 => //.
have pb: \omega a <=c cprod Y.
rewrite pa;apply:compare_sum_prod1 => //; rewrite /Y; fprops.
by bw; move=> i idx; bw; apply:infinite_ge2; apply: CIS_aleph;apply: ofx.
move: (cpow_Mleeq (cardinal b) pb (aleph_nz (proj31 la))).
rewrite db;move => h; apply: (cleT h); clear pa pb h.
have dY: domain Y = b by rewrite /Y; bw.
set f := Lg (coarse b) (fun z => Vg Y (P z)).
have df: domain f = (coarse b) by rewrite /f; bw.
have fgf: fgraph f by rewrite /f; fprops.
have fgY: fgraph Y by rewrite /Y; fprops.
have ->: cprod Y ^c cardinal b = cprod f.
set g := Lg b (fun z => (singleton z) \times b).
have pa: partition_w_fam g (domain f).
split => //.
rewrite /g; fprops.
hnf;rewrite /g; bw;move => i j id jd; bw.
case: (equal_or_not i j) => ij; [ by left | right ].
apply: disjoint_pr => u /setX_P [_ p1 _] /setX_P [_ p2 _].
by case: ij; move: p1 p2 => /set1_P <- /set1_P <-.
rewrite df /coarse /g; set_extens t.
move /setUb_P; bw; move => [y yb]; bw; move => /setX_P [p1] /set1_P.
move => p2 p3; apply /setX_P;split => //; ue.
move => /setX_P [p1 p2 p3]; apply /setUb_P; bw; exists (P t); bw.
apply /setX_P;split;fprops.
rewrite (cprod_An pa) (cpow_prod _ Y) dY /g; bw; congr cprod.
apply: Lg_exten; move => x xb.
set s:= ((singleton x) \times b).
have xx: cardinal s = cardinal b.
symmetry; apply /card_eqP; apply: Eq_rindexed.
rewrite - (cpow_pr3 _ xx); congr cprod.
have sa: sub s (coarse b).
move=> t /setX_P [p1 /set1_P p2 p3]; apply /setX_P;split => //; ue.
have sb: sub s (domain f) by ue.
have qa: s = domain (restr f s) by bw.
rewrite /cst_graph; apply: fgraph_exten; [fprops | fprops | bw | bw].
move => v vd; bw; rewrite /f; bw; last by apply: sa.
by move: vd => /setX_P [_ /set1_P -> _].
set g := Lg b (fun z => Zo (coarse b) (fun t => (P t) +#o (Q t) =z)).
have pg: partition_w_fam g (domain f).
split => //; rewrite /g /coarse/mutually_disjoint; bw.
- fprops.
- move => i j ib jb; case: (equal_or_not i j) => ij; [ by left | right ].
bw;apply: disjoint_pr => u /Zo_hi p1 /Zo_hi p2; case: ij.
by rewrite - p1 - p2.
- rewrite df /coarse;set_extens t.
by move /setUb_P; bw; move => [y yb]; bw; move => /Zo_P [].
move: lb => [ob _ _] tb.
move: (tb) => /setX_P [pt /(oltP ob) p1 /(oltP ob) p2].
have pa: inc (natural_sum (P t) (Q t)) b.
by apply /(oltP ob); apply:natural_small.
by apply /setUb_P; bw; ex_tac; bw;apply: Zo_i.
rewrite (cprod_An pg).
apply: cprod_increasing; [ rewrite dY /g; bw | bw].
rewrite /g; bw => x xb; bw.
move: (natural_finite_cover oc xb).
rewrite - /b /coarse; set E:= Zo _ _; move => [pa pb].
have dr: domain (restr f E) = E.
rewrite restr_d //; rewrite /E df; apply: Zo_S.
have xd: inc x (domain X) by ue.
have le1: forall i, inc i E -> Vg f i <=c Vg Y x.
rewrite /f; move => i => /Zo_P [qa qb]; bw.
move: qa => /setX_P [_ ipb iqb].
have op:= (ordinal_hi (proj31 lb) ipb).
have oq := (ordinal_hi (proj31 lb) iqb).
move: (natural_M0le op oq); rewrite qb.
case: (equal_or_not (P i) x) => eq1.
rewrite eq1 => _; apply: cleR; rewrite /Y; bw; apply CIS_aleph.
by apply: ofx.
have pd: inc (P i) (domain X) by ue.
move => eq2; move: (proj1 (si _ _ pd xd (conj eq2 eq1))) => le2.
by rewrite /Y; bw; apply: aleph_le_lec.
have ix: infinite_c (Vg Y x).
by rewrite /Y; bw; apply: CIS_aleph; apply: ofx.
rewrite - (cpow_inf ix pa pb) - (cpow_pr3 _ (refl_equal (cardinal E))).
apply: cprod_increasing; rewrite /cst_graph ? dr; bw.
by move => t tE; bw; apply: le1.
Qed.
Lemma infinite_prod3_bis X m (Y:= Lg (domain X) (fun z => \aleph (Vg X z))):
infinite_c m -> ofg_Mlt_lto X -> domain X = m ->
(cprod Y) = (\csup (range Y)) ^c m.
Proof.
move => im pa pb.
move: (cardinal_indecomposable im) => idx.
move: (indecomp_prop3 idx) => [y oy xv].
case: (ozero_dichot oy) => ynz.
by move: im; rewrite xv ynz opowx0 => /(infinite_dichot1 finite_1).
rewrite xv in pb.
by rewrite (infinite_prod3 ynz pa pb) -xv (card_card (proj1 im)).
Qed.
Lemma infinite_prod4 X a m
(Y:= Lg (domain X) (fun z => \aleph (Vg X z) ^c m)):
limit_ordinal a -> \cf a <=c m -> domain X = \cf a ->
ofg_Mlt_lto X -> (a = \osup (range X)) ->
(cprod Y) = \aleph a ^c m.
Proof.
move => oa ca cdx ofx av.
have lc:=(cofinality_limit3 oa).
have cc:=(CS_cofinality (proj31 oa)).
have icc: infinite_c (\cf a) by split => //; apply: OIS_limit.
have im:= ge_infinite_infinite icc ca.
rewrite - cdx in lc.
move: (infinite_prod3_bis icc ofx cdx).
move: (increasing_sup_limit4 ofx lc); rewrite -av; move => [pa _ ->] => pd.
move: (f_equal (fun z => z ^c m) pd).
rewrite - cpow_pow cpow_prod cprodC (cprod_inf ca im (infinite_nz icc)).
move => <-; bw; rewrite /Y cdx; apply: cprodb_exten => x xd; bw.
Qed.
Lemma infinite_prod44 X a b
(Y:= Lg (domain X) (fun z => \aleph (Vg X z) ^c \aleph b)):
limit_ordinal a -> \cf a <=o b -> domain X = \omega (\cf a) ->
ofg_Mlt_lto X -> a = \osup (range X) ->
cprod Y = (\aleph a) ^c (\aleph b).
Proof.
move => oa ca cdx ofx av.
have oc:=(OS_cofinality (proj31 oa)).
have icc:=(CIS_aleph oc).
have lc:= (infinite_card_limit2 icc).
move: (infinite_prod3_bis icc ofx cdx).
rewrite - cdx in lc.
move:(increasing_sup_limit4 ofx lc); rewrite - av; move => [pa _ ->] => pd.
move: (f_equal (fun z => z ^c \aleph b) pd).
rewrite - cpow_pow cpow_prod cprodC.
rewrite (cprod_inf (aleph_le_lec ca) (CIS_aleph (proj32 ca))(infinite_nz icc)).
move => <-; bw; rewrite /Y cdx; apply: cprodb_exten => x xd; bw.
Qed.
Lemma infinite_prod_pF:
cprodb omega1 \aleph = (\aleph omega1) ^c aleph1.
Proof.
have ic: (infinite_c omega1) by apply CIS_aleph; fprops.
have oo:=(proj1 (proj1 ic)).
set (X := Lg omega1 id).
have sX: domain X = omega1 by rewrite /X; bw.
have ha: ofg_Mlt_lto X.
have fhx: fgraph (Lg omega1 id) by fprops.
rewrite /X;split => //;hnf;bw; [ move=> t to; bw | move => u v uo vo uv; bw].
exact:(ordinal_hi oo to).
have sr: \osup (range X) = omega1.
rewrite /X identity_r.
by move :(limit_nonsucc (infinite_card_limit2 ic)).
have lo:limit_ordinal (domain X). by rewrite sX; exact:(aleph_limit OS1).
move: (infinite_prod3_bis ic ha sX).
move: (increasing_sup_limit4 ha lo) => [_ _ ->]. rewrite sr => <-.
rewrite /X; bw; apply: cprodb_exten => x xa; bw.
Qed.
Lemma infinite_prod_pG b: \1o <=o b ->
cprodb omega1 (fun z => (\aleph z) ^c (\aleph b))
= (\aleph omega1) ^c (\aleph b).
Proof.
move => b1.
have cp1: aleph1 <=c \aleph b by apply:aleph_le_lec b1.
have ie := CIS_aleph (proj32 b1).
move: (f_equal (fun z => z ^c \aleph b) infinite_prod_pF).
rewrite cpow_prod - cpow_pow cprodC (cprod_inf cp1 ie (aleph_nz OS1)) => <-.
bw;apply: cprodb_exten => x xe; bw.
Qed.
Lemma infinite_prod_pH b: ordinalp b ->
cprodb omega0 (fun z => (\aleph z) ^c (\aleph b))
= (\aleph omega0) ^c (\aleph b).
Proof.
move => ob.
have ie := CIS_aleph ob.
move/infinite_c_P2 : (ie) => iea.
move: (f_equal (fun z => z ^c \aleph b) infinite_prod_pC).
rewrite cpow_prod - cpow_pow cprodC (cprod_inf iea ie omega_nz) => <-.
by bw; apply: cprodb_exten => x xd; bw.
Qed.
Lemma infinite_prod5 a:
(limit_ordinal a) ->
cprodb a \aleph = (\aleph a) ^c (cardinal a).
Proof.
move => la.
pose p j := limit_ordinal j ->
cprodb j \omega = \omega j ^c cardinal j.
apply: (least_ordinal2 (p:=p)) (proj31 la) la => y oy etc ly.
move: (cantor_of_limit ly) => [c [n [oc on nz yv cp]]].
have np := (ord_ne0_pos on nz).
have op:= (OS_pow OS_omega on).
case: (equal_or_not c \0o) => cz.
move: yv; rewrite cz (osum0l op) => yv.
set X := (Lg y id).
have dx: domain X = omega0 ^o n by rewrite -yv /X; bw.
have osx: ofg_Mlt_lto X.
rewrite /X /ofg_Mlt_lto /ordinal_fam; bw;split;fprops.
hnf; bw;move => x xy; bw; exact (ordinal_hi oy xy).
hnf; bw;move => u v ux vx uv; bw.
move: (infinite_prod3 np osx dx).
have ->: (Lg (domain X) (fun z => \omega (Vg X z))) = (Lg y \omega).
rewrite /X; bw; apply: Lg_exten => t te; bw.
by move => h; rewrite /cprodb h -yv ord_sup_aleph.
case: cp => [ cnz // |[lc le1 sv]].
have cy: c eq1.
rewrite {1} yv (cprod_An1 \aleph oc op) eq1.
set X := Lg (omega0 ^o n) (fun z => (c +o z)).
have dx: domain X = omega0 ^o n by rewrite /X; bw.
have xx: ofg_Mlt_lto X.
split; rewrite /X; fprops.
hnf;bw; move => x xv; bw; exact:(OS_sum2 oc (ordinal_hi op xv)).
hnf; bw; move => u v ud vd; bw => lt1.
by apply: osum_Meqlt.
move: (infinite_prod3 np xx dx); rewrite /cprodb.
set L1:= Lg _ _; set L2 := Lg _ _.
have ->: L1 = L2 by rewrite /L1 /L2 /X; bw; apply: Lg_exten => x xd; bw.
have l1: limit_ordinal (omega0 ^o n) by apply:indecomp_limit2.
have ->: union (range L2) = \omega y.
move: (normal_ofs_compose aleph_normal (osum_normal oc)) => [_ xb].
by move: (xb _ l1); rewrite -/L2 /= yv; move => ->; rewrite /L2 Lg_range.
move => ->;clear L1 L2.
have cnz: cardinal y <> \0c.
by apply:card_nonempty1; move: ly => [_ ok _]; exists \0c.
have le2: cardinal (omega0 ^o n) <=c cardinal y.
by apply ocle1; rewrite yv; apply: osum_M0le.
by move: (infinite_power5 oc op cnz le2); rewrite -yv => ->.
Qed.
Lemma infinite_prod6 a:
ordinalp a -> a <> \0o ->
cprodb (osucc a) \aleph = (\aleph a) ^c (cardinal a).
Proof.
move => oa anz.
pose p j := j <> \0o ->
cprodb (osucc j) \omega = \omega j ^c cardinal j.
apply: (least_ordinal2 (p:= p)) oa anz => y oy lyp ynz.
have ->: cprodb (osucc y) \aleph =
(cprodb y \omega) *c (\aleph y).
rewrite - (osucc_pr oy) (cprod_An1 \aleph oy OS1); congr (_ *c _).
rewrite /cprodb;set f := Lg _ _.
have fg: fgraph f by rewrite /f; fprops.
have df: domain f = singleton \0o by rewrite /f; bw.
have f0: Vg f \0o = \omega y.
rewrite /f; bw; [by rewrite (osum0r oy) | by apply /set1_P ].
by rewrite (cprod_trivial1 df) card_card // f0; apply: CS_aleph.
have cny: cardinal y <> \0c.
case: (emptyset_dichot y) => ey; first by contradiction.
by apply card_nonempty1.
case: (ordinal_trichot oy) => h; first contradiction; last first.
have onz: \omega y <> \0c by apply: aleph_nz.
have p1: \omega y <=c \omega y ^c cardinal y.
apply: (cpow_Mle1 (CS_aleph oy) cny).
move: (ge_infinite_infinite (CIS_aleph oy) p1) => p2.
by rewrite (infinite_prod5 h); apply: (cprod_inf).
move: h => [z oz zv].
case: (equal_or_not z \0o) => znz.
rewrite zv znz osucc_zero /cprodb.
set f := Lg _ _.
have fg: fgraph f by rewrite /f; fprops.
have df: domain f = singleton \0o by rewrite /f; bw.
have f0: Vg f \0o = \omega \0o.
by rewrite /f; bw; apply /set1_P.
have cv: cardinalp (Vg f \0o) by rewrite f0; apply: CS_aleph; fprops.
rewrite (cprod_trivial1 df) f0 (card_card CS1) cprod2cl cprodC.
have p1: \omega \0o <=c \omega \1o.
by apply: aleph_le_lec; apply: (ozero_least OS1).
by rewrite (cprod_inf p1 (CIS_aleph OS1) (aleph_nz OS0)) (cpowx1 (proj32 p1)).
have lt1: z zi.
hnf in zi; have <- //: cardinal z = cardinal (osucc z).
by apply /card_eqP.
have fz:finite_o z by split.
rewrite - (succ_of_finite fz).
have zN: natp z by apply /NatP.
rewrite (card_nat zN) (card_card (CS_succ z)).
rewrite (cpow_succ _ zN).
symmetry.
have onz: \omega z <> \0c by apply: aleph_nz.
have p1: \omega z <=c \omega z ^c z.
apply: (cpow_Mle1 (CS_aleph oz) znz).
move: (ge_infinite_infinite (CIS_aleph oz) p1) => p2.
apply: (cprod_inf) => //.
Qed.
Lemma infinite_power7c x y:
cardinalp x -> cardinalp y ->
cardinal (unionb (Lg x (functions y)))
<=c (csum (Lg (cardinals_lt x) (fun z => z ^c y))) *c x.
Proof.
move => cx cy.
set g := Lg _ _.
have fg: fgraph g by rewrite /g; fprops.
apply: (cleT (csum_pr1 _)).
set f := (Lg x (fun z => cardinal z ^c y)).
have fgf: fgraph f by rewrite /f; fprops.
set h := Lg (cardinals_lt x) (fun i => Zo x (fun t => (cardinal t) = i)).
have fgh: fgraph h by rewrite /h; fprops.
have dh: domain h = (cardinals_lt x) by rewrite /h; bw.
have mh: mutually_disjoint h.
by apply mutually_disjoint_prop2 => i j z id jd /Zo_hi => <- /Zo_hi <-.
move: (proj1 cx) => ox.
have ph: partition_w_fam h (domain f).
split => //; rewrite /f; bw; set_extens t.
move /setUb_P => [z za];rewrite /h; bw ; [by move => /Zo_P [] | ue].
move => tx; apply /setUb_P.
have ot:= (ordinal_hi ox tx).
have ts: inc (cardinal t) (cardinals_lt x).
by apply /(cardinals_ltP cx); apply /(ocle2P cx ot); apply/oltP.
exists (cardinal t); [by rewrite dh | by rewrite /h;bw; apply: Zo_i].
rewrite /csumb;set u := csum _.
move: (csum_An ph).
have -> : u = csum f.
rewrite /u /f; apply: f_equal; rewrite /g; bw; apply: Lg_exten=> t tx.
by bw; rewrite cpow_pr1 (card_card cy).
move ->.
rewrite -dh.
have fgfxx: fgraph (Lg (domain h) (cpow^~ y)) by fprops.
rewrite cprodC (cprod2Dn); bw.
apply: csum_increasing; bw.
move=> z zd; bw.
have pc: sub (Vg h z) (domain f).
move: ph => [_ _ un]; rewrite -un.
move=> t th; apply /setUb_P; exists z => //; ue.
have pd: sub (Vg h z) x by move: pc; rewrite /f; bw.
have pb: domain (restr f (Vg h z)) = Vg h z by rewrite restr_d //.
rewrite /csumb.
have ->: (Lg (Vg h z) (Vg f)) = Lg (Vg h z) (fun t => z ^c y).
apply: Lg_exten; fprops; bw.
rewrite /f => t td; move: (pd _ td) => tx; bw.
move: td; rewrite /h; bw; [ move /Zo_P; move => [_ -> //] | ue].
rewrite csum_of_same cprodC - cprod2cl.
apply cprod_Mlele.
by move: (sub_smaller pd); rewrite (card_card cx).
apply: cleR; rewrite /cpow;fprops.
Qed.
Lemma infinite_power7d x (y := cardinal (cardinals_lt x)):
cardinalp x -> x <> \0c ->
(y <=c x /\ y <> \0c).
Proof.
move=> cx xnz; split.
have pf: sub (cardinals_lt x) x.
move => t /Zo_P [_ ok]; move: (oclt ok).
by move =>/ oltP0 [_ _].
by move: (sub_smaller pf); rewrite (card_card cx).
apply: card_nonempty1; exists \0c.
by apply /(cardinals_ltP cx); split; [apply: czero_least | apply:nesym ].
Qed.
Lemma infinite_power7 x y:
infinite_c x -> y y <> \0c ->
x ^c y = (csumb (cardinals_lt x) (fun z => z ^c y)) *c x.
Proof.
move=> pa pb pc.
have cy:= proj31_1 pb.
have cx:= proj1 pa.
have le1:= (infinite_power7b pa pb).
have le2:= (infinite_power7c cx cy).
apply: (cleA (cleT le1 le2)).
have xnz: x <> \0c by apply: infinite_nz.
have pd: x <=c x ^c y.
have y1: \1c <=c y by apply: cge1.
apply: cpow_Mle1; fprops.
have ip:=(ge_infinite_infinite pa pd).
apply: (cprod_inf4 _ pd ip).
set f := (Lg (cardinals_lt x) (cpow^~ y)).
have fl: (forall i, inc i (domain f) -> Vg f i <=c ( x ^c y)).
rewrite /f; bw; move=> i id; bw.
case: (equal_or_not i \0c) => iz.
rewrite iz (cpow0x pc);apply: (czero_least (proj32 pd)).
move: id => /(cardinals_ltP cx) [le _].
by apply: cpow_Mleeq.
move: (infinite_power7d cx xnz) => [pe1 pf].
have fgf: fgraph f by rewrite /f; fprops.
move: (csum_of_small_b1 (conj fgf fl)); rewrite {2}/f; bw.
rewrite - cprod2cr cprod_inf//; exact: (cleT pe1 pd).
Qed.
Lemma infinite_power7e a y:
limit_ordinal a -> y <> \0c ->
\aleph a <=c \osup (fun_image a (fun z => (\aleph z) ^c y)).
Proof.
move=> ln ynz.
move: aleph_normal => [qa qb]; rewrite (qb _ ln).
set T2:= fun_image _ _.
set T := fun_image _ _.
have csr: cardinal_set T.
move=> t /funI_P [z zn ->]; rewrite /cpow; fprops.
apply:card_ub_sup; first by apply: (CS_sup csr).
move => // i /funI_P [z zn ->].
have sr1: inc ((\aleph z) ^c y) T by apply /funI_P; ex_tac.
apply: cleT (card_sup_ub csr sr1).
have oz:= (ordinal_hi (proj31 ln) zn).
by apply: cpow_Mle1; fprops; apply: CS_aleph.
Qed.
Lemma infinite_power7f a y:
limit_ordinal a -> y
(\aleph a) ^c y = \osup (fun_image a (fun z => (\aleph z) ^c y)).
Proof.
move => p1 p2.
have on:= (proj31 p1).
case: (equal_or_not y \0c) => yz.
rewrite yz cpowx0; set T := fun_image _ _.
suff: T = singleton \1c by move => ->; rewrite setU_1.
apply set1_pr.
by move: p1 => [q1 q2 q3]; apply /funI_P; exists \0o => //; rewrite cpowx0.
by move=> t /funI_P [z zn ->]; rewrite cpowx0.
move: (CIS_aleph on); set x:= \aleph a => icx.
rewrite - (regular_initial_limit1 p1) in p2.
have aux:= (infinite_power7 icx p2 yz).
set T := fun_image _ _.
set s := union T.
have s3: s <=c x ^c y.
apply: card_ub_sup; first by fprops.
move => i /funI_P [z zn ->].
have [zn1 _]: z aux.
have cff: cardinal_fam f by rewrite /f; hnf; bw; move=> i ad; bw; fprops.
have cx:= proj1 icx.
have cdf1: cardinal (domain f) <=c x.
rewrite /f; bw; exact (proj1 (infinite_power7d cx (infinite_nz icx))).
have fgf: fgraph f by rewrite /f; fprops.
have osr: ordinal_set (range f).
move=> t /(range_gP fgf); rewrite /f; bw; move=> [z zv -> ].
bw;apply: OS_cardinal; fprops.
have sr: s = \osup (range f).
rewrite /s /T /f; apply: ord_sup_1cofinal => //; split.
move=> t /funI_P [z zn ->]; apply /(range_gP fgf).
have os: inc (\aleph z) (cardinals_lt x).
by apply /(cardinals_ltP cx) /aleph_lt_ltc /oltP.
rewrite /f; bw; exists (\aleph z); bw.
move=> i /(range_gP fgf); rewrite /f; bw; move=> [u us]; bw => ->.
move: us => /(cardinals_ltP cx) us.
have cu:= proj31_1 us.
case: (finite_dichot cu) => fc.
exists (omega0 ^c y) => //.
apply /funI_P; exists \0o; [exact (proj32 p1) | by rewrite aleph0E ].
apply: ocle.
case: (equal_or_not u \0c) => uz.
rewrite uz (cpow0x yz); apply: czero_least; rewrite /cpow;fprops.
apply: cpow_Mleeq=> //;apply: finite_le_infinite => //.
exact: (CIS_omega).
move:(ord_index_pr1 fc) => [om uv].
exists (u ^c y).
apply /funI_P; exists (ord_index u); rewrite ? uv => //.
apply /(oltP on); apply: aleph_ltc_lt => //; ue.
exact: (ocle(cleR (CS_pow u y))).
move: (infinite_power7e p1 yz).
rewrite -/x -/T -/s => xs.
have pc: (infinite_c s) by apply: (ge_infinite_infinite icx xs).
have pd:= cleT cdf1 xs.
rewrite sr in pc pd xs.
move: (csum_of_small_b4 fgf cff pc pd);rewrite aux sr /csumb -/f => ->.
by apply: cprod_inf => //;apply: infinite_nz.
Qed.
Lemma infinite_power7f1 a y:
limit_ordinal a -> y y <> \0c ->
(\aleph a) ^c y = csumb a (fun z => (\aleph z) ^c y).
Proof.
move => pa pb pc.
have on:= (proj31 pa).
move: (infinite_power7f pa pb); rewrite - Lg_range=> eq0.
move: (ocle1 (aleph_pr6 on)); rewrite (card_card (CS_aleph on)) => le2.
rewrite eq0;symmetry; apply: csum_of_small_b4.
- fprops.
- by hnf; bw; move=> i an; bw; fprops.
- by rewrite - eq0; apply: CIS_pow => //; apply: CIS_aleph.
- by rewrite - eq0 Lg_domain; exact: (cleT le2 (cpow_Mle1 (proj32 le2) pc)).
Qed.
Lemma infinite_prod_pI:
csumb omega1 (fun z => \aleph z ^c aleph0) = \aleph omega1 ^c aleph0.
Proof.
have la: limit_ordinal omega1 by apply: aleph_limit; fprops.
have ic: infinite_c omega1 by apply: CIS_aleph; fprops.
have cf: omega0 ->.
rewrite - aleph0E; apply: aleph_lt_ltc; apply: olt_01.
rewrite (infinite_power7f1 la cf) //; first by apply: omega_nz.
Qed.
Lemma infinite_power8 n (x:= \aleph n) (z:= \cf x) y:
ordinalp n -> z <=c y ->
x ^c y = ( \osup (fun_image (cardinals_lt x) (fun t => t ^c y))) ^c z.
Proof.
move=> ln cy.
set T := fun_image _ _.
have cst: cardinal_set T.
move=> t /funI_P [zs _ ->]; rewrite /cpow; fprops. clear cst.
have icx: infinite_c x by apply: CIS_aleph.
have cxy: cardinalp (x ^c y) by rewrite /cpow; fprops.
have H:= (cofinality_card icx).
move: (cofinality_infinite icx); rewrite H -/z => icz.
have icy:= (ge_infinite_infinite icz cy).
have sx: \osup T <=c x ^c y.
apply: card_ub_sup => //.
move=> a /funI_P [u up ->].
case: (equal_or_not u \0c) => uz.
rewrite uz cpow0x; [by apply czero_least | by apply: infinite_nz].
apply: cpow_Mleeq => //.
by move: up => /(cardinals_ltP (proj1 icx)) [].
apply: cleA; last first.
have znz: z <> \0c by apply: infinite_nz.
case: (equal_or_not (\osup T) \0c) => snz.
by rewrite snz cpow0x => //; apply czero_least.
have : (\osup T) ^c z <=c (x ^c y) ^c z by apply: cpow_Mleeq => //.
rewrite - cpow_pow (cprod_inf cy) //.
move: (cofinality_c_pr3 icx) => [f [[[pc1 pc2 pd pe] pf] pc]].
have qa: x <=c cprod f.
rewrite -pf; apply: compare_sum_prod1 => //.
have : x ^c y <=c (cprod f) ^c y.
by apply: cpow_Mleeq => //;apply: infinite_nz.
rewrite (cpow_prod _ f) /cprodb.
set p := cprod _ => le1.
have cst: cardinal_set T by move=> t /funI_P [tt _ ->]; fprops.
have: p <=c cprod (cst_graph (domain f) (\osup T)).
apply: cprod_increasing; bw.
bw => t tdf; bw.
apply: card_sup_ub => //; apply /funI_P; exists (Vg f t) => //.
by apply /(cardinals_ltP (proj1 icx)); apply: pd.
by rewrite cpow_pr2 pe H; apply:cleT.
Qed.
Lemma infinite_power9 x y: infinite_c x -> infinite_c y ->
[/\ (x <=c y -> x ^c y = \2c ^c y),
(forall z, z x <=c z ^c y -> x ^c y = z ^c y) &
((forall z, z z ^c y
( ( y x ^c y = x)
/\ (\cf x <=c y -> x ^c y = x ^c (\cf x))))].
Proof.
move => icx icy.
have ynz:=(infinite_nz icy).
have xnz:= (infinite_nz icx).
split.
by move => h; apply: infinite_power1_a => //; apply: infinite_ge2.
move=> z le1 le2; apply: cleA.
rewrite - {2} (csquare_inf icy) cpow_pow.
by apply: cpow_Mleeq.
have znz: z <> \0c.
move=> bad; case: xnz; move: le2; rewrite bad cpow0x // => b1.
apply (cle0 b1).
apply: cpow_Mleeq => //; exact (proj1 le1).
move => h.
have x2: \2c //; apply /NatP; fprops.
have yx:= (cle_ltT (proj1 (cantor (proj1 icy))) (h _ x2)).
have [on xv]:= (ord_index_pr1 icx).
case: (ordinal_trichot on) => nz.
move: yx; have ->: x = omega0 by rewrite -xv nz aleph0E.
by move: icy => /infinite_c_P2 icy /(cleNgt icy).
move:nz=> [m om nv].
move: (regular_initial_successor om) => /regular_cardinalP [_ ww].
move: yx h; rewrite -xv nv ww => yo h;split; last by move=> /(cltNge yo).
have le2 := (h _ (aleph_pr10c om)).
move => _.
move: (infinite_power2 om ynz).
have pa: (infinite_c (\aleph (osucc m))) by apply: CIS_aleph; ue.
have pb:=(cpow_nz (b := y) (aleph_nz om)).
by rewrite cprodC (cprod_inf (proj1 le2) pa pb).
split.
rewrite -xv (regular_initial_limit1 nz) => yc.
move: (infinite_power7e nz ynz).
rewrite (infinite_power7f nz yc).
set T := fun_image _ _; move=> le1.
apply: cleA => //.
apply: (card_ub_sup (proj31 le1)).
move => a /funI_P [z zn ->]; rewrite - xv in h.
have aux : \aleph z /oltP [].
apply: (proj1 (h _ aux)).
rewrite -xv; move=> cf1.
have oxne: \aleph (ord_index x) <> \0c by ue.
apply: cleA; last by apply: cpow_Meqle.
rewrite {1} (infinite_power8 on cf1); set T2:= fun_image _ _.
case: (equal_or_not (union T2) \0c) => unz.
rewrite unz cpow0x.
apply: czero_least;rewrite /cpow; fprops.
apply: infinite_nz; apply:cofinality_infinite_cardinal; ue.
apply: cpow_Mleeq => //.
apply: card_ub_sup; first by rewrite xv; exact (proj1 icx).
move=> a; rewrite /T2 xv => /funI_P [z zi ->].
move: zi => /(cardinals_ltP (proj1 icx)) zi.
exact: (proj1 (h _ zi)).
Qed.
Lemma infinite_power7g x y: infinite_c x -> x <=c y ->
x ^c y = (csumb (cardinals_lt x) (fun z => z ^c y)) *c x.
Proof.
move => icx xy.
have [cx cy _]:= xy.
have icy: infinite_c y by apply: (ge_infinite_infinite icx xy).
have ynz: y <> \0c by apply: infinite_nz.
have x2: \2c <=c x by apply: infinite_ge2.
rewrite (infinite_power1_a (infinite_ge2 icx) xy icy) /csumb.
have pa:= cleT xy (proj1 (cantor cy)).
move: (infinite_power7d (proj1 icx) (infinite_nz icx)) => [pb pc].
set f := Lg _ _.
have cf: fgraph f by rewrite /f; fprops.
have pd: infinite_c (\2c ^c y) by apply: (ge_infinite_infinite icx pa).
have fl: forall i, inc i (domain f) -> Vg f i <=c \2c ^c y.
rewrite /f; bw; move=> i idf; bw.
move: idf => /(cardinals_ltP cx) idf.
have p1:= (proj1 (clt_leT idf xy)).
case: (equal_or_not i \0c) => iz.
rewrite iz (cpow0x ynz); apply: czero_least; rewrite /cpow; fprops.
case: (equal_or_not i \1c) => io.
rewrite io (cpow1x); apply: finite_le_infinite => //.
apply /NatP; fprops.
have i2: \2c <=c i.
have ci := (proj31 p1).
case: (finite_dichot ci) => iB.
move: iB;rewrite /NatP => iB.
rewrite - succ_one; apply/(cleSltP NS1); split; fprops.
apply: cge1 => //.
apply: (infinite_ge2 iB).
rewrite (infinite_power1_a i2 p1 icy).
apply: cleR; rewrite /cpow; fprops.
move: (csum_of_small_b1 (conj cf fl)); rewrite {2} /f; bw.
have -> : (\2c ^c y) *c cardinals_lt x
= (\2c ^c y) *c cardinal (cardinals_lt x).
by symmetry;apply cprod2cr.
move => le2.
have le3:= (cleT le2 (cprod_inf1 (cleT pb pa) pd)).
apply:cleA; last by apply: cprod_inf4.
have xnz: x <> \0c by apply: infinite_nz.
have pe: csum f <=c csum f *c x.
apply: cprod_M1le => //; rewrite /csum; fprops.
apply: (cleT _ pe).
have d2: inc \2c (cardinals_lt x).
apply/(cardinals_ltP cx).
apply: finite_lt_infinite => //; rewrite /NatP; fprops.
have ->: \2c ^c y = Vg f \2c by rewrite /f; bw.
apply csum_increasing6; rewrite /f;hnf;bw => t ta; bw; fprops.
Qed.
Lemma infinite_power7h x y:
regular_cardinal x -> \0c
x ^c y = (csumb (cardinals_lt x) (fun z => z ^c y)) *c x.
Proof.
move=> /regular_cardinalP [ic cfx] [[_ cy _] nzy].
case: (cleT_el (proj1 ic) cy) => xy; last first.
rewrite - cfx in xy; exact: (infinite_power7 ic xy (nesym nzy)).
by apply: infinite_power7g.
Qed.
Lemma infinite_power6w y: infinite_c y ->
( (exists2 x, y h; split.
exists (\2c ^c y); first by apply: (cantor (proj1 h)).
rewrite - cpow_pow csquare_inf //.
move: (ord_index_pr1 h)=> [on yv].
move: (cnextE on); rewrite yv; set z:= cnext y => zv.
have yz: y z.
move=> eq; rewrite {2} zv in eq.
move: (aleph_inj oz osn eq).
move: (aleph_limit osn); rewrite - zv; move => [la lb lc] zs.
have nz: inc (ord_index y) z by rewrite zs /osucc; fprops.
move: (lc _ nz); rewrite - zs => bad; exact (ordinal_irreflexive oz bad).
have tp:= (normal_ofs_fix aleph_normal oz).
have cft:= (cofinality_least_fp_normal aleph_normal zp tp).
move: tp =>[]; set t := the_least_fixedpoint_ge _ _ => tp1 tp2 tp3.
have cz: cardinalp z by rewrite zv; apply: CS_aleph.
have ct: cardinalp t by rewrite -tp2; apply: (CS_aleph (proj32 tp1)).
have yt: y //.
apply: (clt_leT (power_cofinality (infinite_ge2 ict))).
apply: cpow_Mlele.
by apply: infinite_nz.
move: ict => [cat _]; fprops.
by rewrite (cofinality_card ict) cft; apply /infinite_c_P2.
Qed.
Definition cpow_less x y :=
\csup (fun_image (cardinals_lt y) (fun t => x ^c t)).
Notation "x ^ x ^c t)).
Proof. move => t /funI_P [z _ ->]; fprops. Qed.
Lemma cpow_less_alt x y :
infinite_c y -> \2c <=c x ->
x ^ x ^c t).
Proof.
move=> icy xy.
rewrite /cpow_less; set E := (cardinals_lt y).
set f := (Lg E [eta cpow x]).
have cf: cardinal_fam f by rewrite/f;hnf;bw => t te; bw; fprops.
set s:= (union (range f)).
have <-: s = union (fun_image E (cpow x)) by rewrite /s Lg_range.
have cy:=(proj1 icy).
move: (infinite_power7d cy (infinite_nz icy)); rewrite -/E; move => [pw _].
suff aux: y <=c s.
symmetry; apply: csum_of_small_b4; fprops.
- apply: (ge_infinite_infinite icy aux).
- move: (cleT pw aux); bw.
have fgf: fgraph f by rewrite /f; fprops.
have csr: cardinal_set (range f).
move => t /(range_gP fgf); rewrite /f;bw;move => [z ze ->]; bw; fprops.
case: (cleT_el cy (CS_sup csr)) => //; rewrite -/s => sy.
move: (cantor (CS_sup csr)); rewrite -/s => /cltNge; case.
have sE: inc s E by apply /(cardinals_ltP cy).
apply: (cleT (cpow_Mleeq s xy card2_nz)).
apply: card_sup_ub => //; apply /(range_gP fgf).
rewrite /f; bw; exists s; bw; split => //.
Qed.
Lemma cpow_less_pr1 x y: \0c cardinalp y -> x ^ [[_ cx _] xnz] cy; apply:card_ub_sup; fprops.
move => t /funI_P [z zy ->]; apply: cpow_Mlele => //.
- by apply:nesym.
- by apply:cleR.
- by move: zy => /cardinals_ltP [].
Qed.
Lemma cpow_less_pr2 x y z: z x ^c z <=c (x ^ lt1; apply: card_sup_ub; first by apply: cpow_less_pr0.
apply /funI_P;exists z => //; apply /(cardinals_ltP (proj32_1 lt1)) => //.
Qed.
Lemma cpow_less_pr3 x y: \0c natp y ->
x ^ [[_ cx _] xnz] yN.
apply: cleA; last by apply: cpow_less_pr2; apply: cltS.
apply: card_ub_sup.
- fprops.
- move => i /funI_P [z zi ->]; apply: cpow_Mlele; fprops.
have cs: cardinalp (csucc y) by apply: CS_succ.
by move: zi => /(cardinals_ltP cs) /(cltSleP yN).
Qed.
Lemma cpow_less_pr4 x y: \0c infinite_c y ->
x ^ [[_ cx _] xnz] yi.
have cy := proj1 yi.
apply: cleA; last by (apply: cpow_less_pr2; apply:(cnext_pr2 cy)).
apply: card_ub_sup.
- fprops.
- move => i /funI_P [z /Zo_hi zi ->]; apply: cpow_Meqle;fprops.
apply: cnext_pr4 => //.
Qed.
Lemma CS_cpow_less x y: cardinalp (x ^
(x <=c \2c ^ icx; move: (proj1 icx) => cx.
have x2:= (infinite_ge2 icx).
split.
move: (@cpow_less_pr0 \2c x) => aux.
case: (cleT_el cx (CS_cpow_less \2c x)) => // pa.
set u := \2c ^ //; apply /funI_P;exists u => //.
apply /cardinals_ltP => //.
case: (cleNgt le (cantor (proj31_1 pa))).
split.
apply: card_sup_image; move=> t tx; apply: (cpow_Mleeq _ x2);fprops.
apply: cpow_less_pr1 => //; split; first by apply: czero_least.
exact: (nesym (infinite_nz icx)).
Qed.
Lemma cpow_less_pr5a x y: cardinalp x -> \2c <=c y -> x <=c x ^ cx y2.
move: (cpow_less_pr2 x (clt_leT (clt_12) y2)).
by rewrite cpowx1.
Qed.
Lemma cpow_less_pr5b x y: infinite_c x -> \2c <=c y -> infinite_c (x ^ cx y2; apply: (ge_infinite_infinite cx (cpow_less_pr5a (proj1 cx) y2)).
Qed.
Lemma cpow_less_pr5c x: \2c <=c x -> finite_c x -> x ^ x2 xf.
have co:= CS_omega.
have aux:= (@cpow_less_pr0 x omega0).
have oic:= CIS_omega.
have xb: natp x by apply /NatP.
have le1: x ^ // i /funI_P [z zx ->].
move: zx => /(cardinals_ltP co) zx.
apply: finite_le_infinite => //; apply /NatP; apply NS_pow; fprops.
by move: (oclt zx) =>/oltP0 [_ _].
ex_middle neq1.
set t := x ^ x ^ icx; move: (proj1 icx) => cx.
apply: cleA (cpow_less_pr5a cx (infinite_ge2 CIS_omega)).
apply: card_ub_sup => // i /funI_P [z za ->]; move: za.
move /(cardinals_ltP CS_omega) => za.
move: (oclt za) => /oltP0; move=> [_ _ xn].
by apply: cpow_inf1.
Qed.
Lemma cpow_less_pr5f (x := omega0): x ^ \2c <=c z ->
z ^c x = (z ^ icx t2.
move: (cofinality_c_pr3 icx) => [f [ [[pa1 pa2 pb pc] pd] _]].
apply: cleA.
rewrite - (cofinality_card icx) -{1} pd (cpow_sum _ f).
rewrite - pc - cpow_pr2 /cst_graph; bw.
apply: cprod_increasing; fprops; bw => t td; bw.
by apply: cpow_less_pr2; apply: pb.
have tp:=(clt_leT clt_02 t2).
have h:= (cpow_less_pr1 tp (proj1 icx)).
have cnz:= (infinite_nz (cofinality_infinite_cardinal icx)).
case: (equal_or_not (z ^ aux.
rewrite aux cpow0x //; by apply: czero_least; fprops.
move: (cpow_Mleeq (\cf x) h aux).
by rewrite - cpow_pow (cprod_inf (cofinality_small icx) icx cnz).
Qed.
Lemma cpow_less_pr6a x: infinite_c x ->
\2c ^c x = (\2c ^ icx; apply: cpow_less_pr6 => //; fprops.
Qed.
Lemma cpow_less_pr7a x: infinite_c x ->
csumb (cardinals_le x) (fun t => x ^c t) = \2c ^c x.
Proof.
move => icx; move: (icx) => [cx _].
set f := (Lg (cardinals_le x) [eta cpow x]).
set a := cardinals_lt x.
have h1P:= (cardinals_ltP cx).
have h2P:= (cardinals_leP cx).
have fgf: fgraph f by rewrite /f; fprops.
have pa: (a +s1 x) = (domain f).
rewrite /f /a; bw; set_extens t.
case/setU1_P => ha;apply /h2P; [by move/h1P: ha => []| rewrite ha; fprops].
move /h2P=> aux; apply /setU1_P; case:(equal_or_not t x) => tx; [by right |].
by left ; apply /h1P; split.
have pb: sub (a +s1 x) (domain f) by rewrite pa; fprops.
have pc: ~(inc x a) by move /h1P => [_].
move: (induction_sum0 f pc).
rewrite pa (restr_to_domain fgf (@sub_refl f)) /csumb; move => ->.
have pd : inc x (cardinals_le x) by apply/ h2P; fprops.
have ->: (restr f a) = Lg a (cpow x).
apply: Lg_exten => t tx; rewrite /f; bw.
move: pa; rewrite /f; bw;move => <-; fprops.
rewrite -/(csumb _ _) - (cpow_less_alt icx (infinite_ge2 icx)).
move: (cpow_less_compare icx) => [_ [_ pe]].
rewrite /f; bw; rewrite -(infinite_power1_b icx).
rewrite csumC (csum_inf pe) //; apply: CIS_pow => //.
by apply: infinite_nz.
Qed.
Lemma cpow_less_pr7b x (y := cnext x) : infinite_c x ->
csumb (cardinals_lt y) (fun t => y ^c t) = \2c ^c x.
Proof.
move => icx; move: (icx) => [cx _].
have pa:=(cnext_pr2 cx).
have iy:= (ge_infinite_infinite icx (proj1 pa)).
have y2:= (infinite_ge2 iy).
have qa:= (clt_leT clt_02 y2).
rewrite - (cpow_less_alt iy y2).
by rewrite (cpow_less_pr4 qa icx) infinite_power1 //; apply: cnext_pr3.
Qed.
Lemma cpow_less_pr8 x:
infinite_c x -> (forall y, y \2c ^c y
[/\ \2c ^c x = gimel_fct x,
x \2c ^c x = x ^c omega0)].
Proof.
move => icx h.
have cx := proj1 icx.
have pa: \2c ^c x = gimel_fct x.
rewrite (cpow_less_pr6a icx).
have le1 : (\2c ^i /funI_P [z] /(cardinals_ltP cx) pa.
move => ->; apply: (proj1 (h _ pa)).
by rewrite (cleA le1 (proj1 (cpow_less_compare icx))).
split; first by exact.
by rewrite -pa; apply: power_cofinality2.
by rewrite pa /gimel_fct => ->.
Qed.
Lemma cpow_less_pr9 x (y := cnext x):
infinite_c x -> ( y ^ icx; move: (icx) => [cx _].
have sp:= (cle_ltT(czero_least cx) (cnext_pr2 cx)).
rewrite (cpow_less_pr4 clt_02 icx) (cpow_less_pr4 sp icx).
by rewrite (infinite_power1_c icx).
Qed.
Definition cpow_less_ecb x :=
(exists2 a, a b \2c ^c a = \2c ^c b).
Lemma cpow_less_pr10 x: singular_cardinal x -> (cpow_less_ecb x)
-> \2c ^c x = \2c ^ [icx sx] [a ax ha].
have H:=(cofinality_card icx).
have cg:= (cofinality_small icx).
have [c [ac cf cx]]: exists c, [/\ a <=c c, \cf x <=c c& c h; first by exists (\cf x).
by exists a.
have p2: (\2c ^ i /funI_P [z zi ->].
move: zi => /(cardinals_ltP (proj1 icx)) zx.
case: (cleT_ee (proj31_1 zx) (proj31_1 cx)) => zc.
apply: cpow_Mlele ; fprops.
rewrite - (ha _ (cleT ac zc) zx); apply: cpow_Mlele ; fprops.
move: (cpow_less_pr6a icx).
move: (cofinality_infinite icx); rewrite H => coi.
have cnz := (infinite_nz coi).
rewrite p2 - cpow_pow cprod_inf//; apply (ge_infinite_infinite coi cf).
Qed.
Lemma gimel_prop n (x:= \aleph n): ordinalp n ->
[/\ (n = \0c -> \2c ^c x = gimel_fct x),
(osuccp n) -> \2c ^c x = gimel_fct x,
(limit_ordinal n -> cpow_less_ecb x ->
\2c ^c x = \2c ^ not (cpow_less_ecb x) ->
\2c ^c x = gimel_fct (\2c ^ on.
have res1: n = \0c -> \2c ^c x = gimel_fct x.
move => h; apply: gimel_prop1.
by rewrite /x h aleph0E; apply: regular_cardinal_omega.
have res2: osuccp n -> \2c ^c x = gimel_fct x.
move => [m om nm].
move: (regular_initial_successor om); rewrite -nm;apply: gimel_prop1.
move: (CIS_aleph on); rewrite -/x => icx.
move: (cofinality_infinite_cardinal icx)(gimel_prop2 icx)(icx) => coi g2 [cx _].
have pa: limit_ordinal n -> infinite_c (\2c ^ ln.
have h:= (cpow_less_pr2 \2c (aleph_lt_ltc (limit_pos ln))).
have ip2o:= (infinite_powerset (CIS_aleph OS0)).
exact (ge_infinite_infinite ip2o h).
split => //.
move=> ln cs; move: (infinite_powerset icx) => ip2x.
case: (equal_or_not x (\cf x)) => xcx.
have rx: regular_cardinal x by apply /regular_cardinalP.
rewrite - (gimel_prop1 rx) cprodC; symmetry; apply cprod_inf => //.
apply: (cpow_less_pr1 clt_02 cx).
exact (infinite_nz (pa ln)).
have si: singular_cardinal x by split => //; apply:nesym.
rewrite - (cpow_less_pr10 si cs).
symmetry; apply cprod_inf => //.
apply: infinite_nz; apply: CIS_pow2 => //.
move => ln nl.
have paln:= (pa ln).
rewrite /gimel_fct (cpow_less_pr6a icx).
suff aux: \cf (\2c ^ [pb _]; apply: OS_cardinal.
move: (cofinality_rw ox) (cofinality_rw oy) => [qa qb qc] [qd qe qf].
have x1: forall t, t \2c ^c t t tx; split; first by apply: cpow_less_pr2.
move => ub; case: nl; exists t => //.
move => b b1 b2.
move: (cpow_M2le b1) (cpow_less_pr2 \2c b2); rewrite - ub.
apply:cleA.
have x2: forall t, t exists2 u, t <=o \2c ^c u & u t tl.
have ot:= proj31_1 tl.
move /(ocle2P (proj1 paln) ot): tl => tl.
case: (oleT_el OS_omega ot) => cto; last first.
exists omega0.
exact (oleT (proj1 cto) (proj1 (oclt (cantor CS_omega)))).
rewrite - aleph0E; apply: aleph_lt_ltc.
by move: ln => [_ ok _]; apply /oltP.
have ict:= (infinite_set_pr3 cto).
move: (cnext_pr1 (proj1 ict)) => []; set st := cnext (cardinal t).
move=> sa sc sb; move: (sb _ tl) => sd.
set sst:= Yo (cardinalp t) t st.
have pc: t <=o sst.
rewrite /sst; Ytac ct; first by apply: oleR.
case: (oleT_ee ot (proj1 sa)) => // xx.
by move: (ocle1 xx); rewrite -/st (card_card sa) =>/(cltNge sc).
have sdd : sst bad ].
case: (p_or_not_p (exists2 u, u H.
by move: H => [u ua ub]; move: (x1 _ ua) => [_ xbad].
have bad2: forall w, w \2c ^c w <=c (cardinal t).
move=> w wc;apply: (cnext_pr4 (proj1 ict)); rewrite -/st bad; split.
exact: (cpow_less_pr2 \2c wc).
by move => eq; case: H; exists w.
have bad3: \2c ^ i /funI_P [z zs ->]; apply: bad2; apply /(cardinals_ltP cx).
case: (cltNge sc (cleT sd bad3)).
suff: (exists2 u, sst <=c \2c ^c u & u [u /ocle p1 p2]; exists u => //; exact: (oleT pc p1).
ex_middle bad; case: (cltNge sdd).
have cs:= (proj31_1 sdd).
apply:card_ub_sup; first exact cs.
move =>i /funI_P [z /(cardinals_ltP cx) zx ->].
have c2: cardinalp (\2c ^c z) by fprops.
by case: (cleT_ee cs c2) => // le4; case: bad; exists z.
apply: oleA.
move: (qb) => [f [[ff sf tf] cf]].
set g := Lf (fun z => \2c ^c (Vf f z)) (\cf x) (\2c ^ \2c ^c (Vf f z)) (\cf x) (\2c ^ t ts /=; rewrite - cpowcr.
set zz := cardinal _.
have zzx: zz //;rewrite -tf; fprops.
move: (cpow_less_pr2 \2c zzx) => [a1 a2 a3].
case: (ordinal_sub (OS_cardinal a1) (OS_cardinal a2) a3) => // eq1.
by move: (proj2 (x1 _ zzx)); rewrite eq1.
have fg: function g by apply: lf_function.
apply: (qf _ qa); exists g.
split; [ by hnf; rewrite /g; split => //; aw | move => t tp].
have tl: t [u u1 u2].
have ui: inc u x by move: (oclt u2) => /oltP0 [_ _].
move: (cf _ ui) => [z zx le2]; exists z => //.
rewrite /g; aw.
have le3:= (ocle1 le2).
move: (cpow_M2le le3); rewrite cpowcr cpowcr.
move => le4; exact: (oleT u1 (ocle le4)).
move: (qe) => [f [[ff sf tf] cf]].
pose g t := choose (fun u => (Vf f t (Vf f t t /(Vf_target ff); rewrite tf => xx.
have [sa _ sc]:= (infinite_card_limit2 paln).
move/(oltP sa): (sc _ xx) => /x2 [u /oleSltP aux ux].
by apply choose_pr; exists u.
set G:= Lf g (cofinality (\2c ^ t; rewrite - sf => stf; move: (gp _ stf) => [_].
by move /oclt =>/(oltP0) [_ _].
apply: qc => //; exists G; split.
by rewrite /G; hnf; aw;split => //; apply: lf_function.
move=> t tx; ex_middle bad.
have pb: forall z, inc z (cofinality (\2c ^ Vf G z z zsf; move: (zsf); rewrite - sf => zt.
have ow: ordinalp (Vf G z).
rewrite /G; aw;exact: (OS_cardinal (proj31_1 (proj2 (gp _ zt)))).
case: (oleT_el (ordinal_hi ox tx) ow) => // yy; case: bad; ex_tac.
have pc: forall z, inc z (cofinality (\2c ^ Vf f z z zc;move: (zc); rewrite - sf => /gp [lt1 _].
move: (pb _ zc); rewrite /G; aw; move => [] /ocle1 /cpow_M2le.
rewrite cpowcr cpowcr => /ocle x6 _; apply:(olt_leT lt1 x6).
have bad2: inc (\2c ^c t) (\2c ^ : (\2c ^c t = \2c ^c (cardinal t)) by apply: cpow_pr; fprops.
have ot:= (ordinal_hi ox tx).
by apply: x1 ; apply /(ocle2P cx ot); apply /oltP.
by move => x3; move: (oclt x3); move/(oltP oy).
by move: (cf _ bad2) => [z zc le]; move: (oleNgt le (pc _ zc)).
Qed.
Lemma gimel_prop3 x: infinite_c x ->
[/\ (regular_cardinal x -> \2c ^c x = gimel_fct x),
(singular_cardinal x -> cpow_less_ecb x -> \2c ^c x = \2c ^ not (cpow_less_ecb x) ->
\2c ^c x = gimel_fct (\2c ^ icx.
move: (ord_index_pr1 icx); set n := (ord_index x); move => [pa pb].
have qa: singular_cardinal x -> limit_ordinal n.
by rewrite - pb; apply: singular_limit.
move: (gimel_prop pa) => [pc pd pe pf].
rewrite pb in pe pf.
split; first by apply: gimel_prop1.
by move => qb qc; rewrite cpow_less_pr10.
by move => qb qc; exact (pf (qa qb) qc).
Qed.
Definition cpow_less_ec_prop x y a:=
a b x ^c a = x ^c b.
Lemma cpow_less_ec_pr0 x y:
infinite_c y -> \2c <=c x -> infinite_c (x ^ icy x2.
have pa: forall n, natp n -> n <=c x ^ n nN; apply (cleT (proj1 (cantor (CS_nat nN)))).
move: nN => /NatP nN.
apply: cleT _ (cpow_less_pr2 x (finite_lt_infinite nN icy)).
by apply: cpow_Mleeq => //; apply: card2_nz.
apply: (ge_infinite_infinite CIS_omega).
by rewrite omega_limit0; apply: (card_ub_sup (proj32 (pa _ NS2))).
Qed.
Lemma cpow_less_ec_pr1 x y:
cardinalp y -> exists a, cpow_less_ec_prop x (cnext y) a.
Proof.
move=> cy.
exists y; split; first by move: (cnext_pr1 cy) => [_ pb _].
move => b yb /(cnext_pr4 cy) bs; by rewrite (cleA bs yb).
Qed.
Lemma card_ge2_nz x: \2c <=c x -> x <> \0c.
Proof.
move => x2.
exact: (nesym (proj2 (clt_leT clt_02 x2))).
Qed.
Lemma cpow_less_ec_pr2 x y a:
cpow_less_ec_prop x y a -> \2c <=c x ->
forall b, a<=c b -> b x ^[ay h] x2 b le1 le2.
have xnz := (card_ge2_nz x2).
apply: cleA; last by apply: cpow_less_pr2.
have cy:= proj32_1 le2.
apply: card_ub_sup; first fprops.
move => i /funI_P [z /(cardinals_ltP cy) lt1 ->].
case: (cleT_ee (proj31 le1) (proj31_1 lt1)) => az.
rewrite - (h _ az lt1) (h _ le1 le2).
apply: (cleR); fprops.
exact (cpow_Meqle xnz (cleT az le1)).
Qed.
Lemma cpow_less_ec_pr3 x y a:
cpow_less_ec_prop x y a -> \2c <=c x -> singular_cardinal y ->
(x ^ h x2 [icy sy]; move: (h) => [ay h0].
have h1:= (cpow_less_ec_pr2 h x2).
have ca:= (proj31_1 ay).
rewrite (h1 _ (cleR ca) ay).
split; first by exact.
have cg:= (cofinality_small icy).
have [c [ac cf cx]]: exists c, [/\ a <=c c, \cf y <=c c &c cp; last by exists a; split;fprops.
exists (\cf y); split => //; split; fprops.
have coi:=(cofinality_infinite_cardinal icy).
have cnz:=(infinite_nz coi).
have icc:= (ge_infinite_infinite coi cf).
rewrite (cpow_less_pr6 icy x2) (h1 _ ac cx) - cpow_pow.
by rewrite (cprod_inf cf icc cnz) (h0 _ ac cx).
Qed.
Lemma cpow_less_ec_pr4 x y:
infinite_c y -> \2c <=c x ->
(exists a, cpow_less_ec_prop x y a) ->
y <=c \cf (x ^ icy x2 [a ha].
have hb:= (cpow_less_ec_pr2 ha x2).
move: (ord_index_pr1 icy); set i := ord_index y; move=> [oi yv].
have xnz: \0c li.
have yo: y = omega0 by rewrite -yv li aleph0E.
move: ha => [ay h1].
rewrite (hb _ (cleR (proj31_1 ay)) ay).
move: (oclt ay); rewrite yo => /olt_omegaP aN.
have sN:= (NS_succ aN).
have sy: (csucc a) //; first by apply /NatP.
apply: CIS_omega.
have eq1:= (h1 _ (cleS aN) sy).
case: (finite_dichot (proj32 x2)) => icx.
have xN: natp x by apply /NatP.
have x1:=(clt_leT (clt_12) x2).
by move: (cpow_Meqlt xN sN (cltS aN) x1) => [_ bad]; case: bad.
have pa:= (cofinality_infinite_cardinal (CIS_pow icx (@succ_nz a))).
by rewrite eq1;apply /infinite_c_P2.
move: li => [j oj jv].
have ->: y = cnext (\aleph j) by rewrite -yv jv cnextE.
have ipy:= (CIS_aleph oj).
rewrite (cpow_less_pr4 xnz ipy).
by move: (power_cofinality5 x2 ipy)(cnext_pr1 (proj1 ipy)) => s [_ _]; apply.
rewrite -yv.
rewrite {1} (proj2 (aleph_normal) _ li).
move: (ha) => [ay _]; move: (ay) => [[ca _] _ _].
have aa:= cleR ca.
have [c [ic ac cy]]: exists c, [/\ infinite_c c, a <=c c & c fa; exists omega0; split => //; first by apply: finite_le_infinite.
rewrite - aleph0E -yv; apply: aleph_lt_ltc.
by move: li => [ori zi _]; apply/oltP.
rewrite yv (hb _ ac cy).
apply: card_ub_sup.
apply: CS_cofinality; exact: (proj1 (CS_pow x c)).
move => t /funI_P [z zi ->].
have zi1: z /oltP [].
move: (aleph_lt_ltc zi1); rewrite yv => lt.
move: (ic) => [cc _].
case: (cleT_el cc (proj31_1 lt)) => le1.
rewrite - (hb _ ac cy) (hb _ (cleT ac le1) lt).
apply: (proj1 (power_cofinality5 x2 (CIS_aleph (proj31_1 zi1)))).
exact:(cleT (proj1 le1) (proj1 (power_cofinality5 x2 ic))).
Qed.
Lemma cpow_less_ec_pr5 x y:
infinite_c y -> \2c <=c x ->
~ (exists a, cpow_less_ec_prop x y a) ->
exists X, let Y := Lg (domain X) (fun z => x ^c (Vg X z)) in
[/\ domain X = \cf y,
(forall i, inc i (domain X) -> Vg X i Vg Y i omega0 -> card_nz_fam X) &
\csup (range Y) = x ^ icy x2 ha.
move: (ord_index_pr1 icy); set c := ord_index y; move => [oc yv].
case: (equal_or_not c \0c)=> cz.
have yo: y = omega0 by rewrite -yv cz aleph0E.
have oic:=CIS_omega.
case: (finite_dichot (proj32 x2)) => fcx; last first.
case: ha; rewrite yo;exists \1c; split; first by apply /clt_omegaP; fprops.
move => b b1 bo.
have bnz: b <> \0c by move/cge1P:b1 => [_ /nesym].
by rewrite(cpowx1 (proj1 fcx)) (cpow_inf fcx) //;apply /clt_omegaP.
exists (Lg y id); simpl; rewrite yo; split => //.
- bw.
- by rewrite (proj2 (regular_omega)).
- by hnf;bw;move => a ay; bw; apply/clt_omegaP.
- bw => i ib; bw; rewrite (cpow_less_pr5c x2 fcx); apply/clt_omegaP; fprops.
- bw; rewrite /cpow_less Lg_range; congr union.
set_extens t;move /funI_P => [z zo ->]; apply/funI_P.
exists z; bw;by apply/(cardinals_ltP CS_omega); apply/clt_omegaP.
move /(cardinals_ltP CS_omega): zo => /clt_omegaP zb; exists z => //; bw.
case: (ordinal_trichot oc) => // lc.
move: lc => [d od dv]; case: ha; exists (\aleph d).
have ipy := (CIS_aleph od).
move: (cnext_pr1 (proj1 ipy)) => [pb pc pd].
move: (cnextE od); rewrite -dv yv => <-; split => //.
by move => b l1 /(cnext_pr4 (proj1 ipy)) pe; rewrite (cleA l1 pe).
have xnz:= (card_ge2_nz x2).
have pa: forall a, a exists b, [/\ a a ay; ex_middle bad; case: ha; exists a; split => //.
move => b ab lby; ex_middle ne.
case: bad; exists b; split => //; split => //; first by dneg eq0; rewrite eq0.
exact: (cpow_Meqle xnz ab).
have cfy:= (regular_initial_limit1 lc).
move: (cofinality_pr4 (proj31 lc)); rewrite - cfy yv; move=> [f fa qe].
move: fa; set cy := \cf y; move => [[[ff sf tf]] cff [_ nf nf1]].
set X := Lg cy (fun z => \aleph (Vf f z)).
have fap: forall z, inc z cy -> inc (Vf f z) c.
by move => z zx; rewrite -tf; Wtac.
have faq: forall z, inc z cy -> ordinalp (Vf f z).
move=> z zx; exact: (ordinal_hi oc (fap _ zx)).
have pb: cardinal_fam X.
by rewrite /X;hnf;bw; move => a ay; bw;apply: CS_aleph; apply: faq.
have pc: fg_Mlt_ltc X.
hnf; rewrite /X; bw;move => a b ac bc ab; bw;apply: aleph_lt_ltc.
by apply: nf.
have pb': fgraph X by rewrite /X; fprops.
have pd: cardinal_set (range X).
by move => t /(range_gP pb') [z zd ->]; apply: pb.
have pe: \osup (range X) = y.
set S := \osup (range X); move: (proj1 icy) => ccy.
case: (cleT_el ccy (CS_sup pd)) => pr1.
apply:cleA => //; apply: card_ub_sup=> // i /(range_gP pb').
rewrite /X; bw; move => [z zy ->]; bw; move /(oltP oc): (fap _ zy) => [].
by rewrite - yv => /aleph_le_lec.
have [ra rb rc]: limit_ordinal cy.
apply: infinite_card_limit2.
by rewrite /cy - yv cfy; apply: cofinality_infinite_limit.
have: infinite_c S.
have: inc (\aleph (Vf f \0c)) (range X).
apply /(range_gP pb'); rewrite /X; bw; ex_tac; bw.
move /(card_sup_ub pd); apply: ge_infinite_infinite; apply: CIS_aleph.
by apply: faq.
move/ord_index_pr1 => []; set s := ord_index S => os sv.
move: pr1; rewrite - /S - sv - yv; move /(aleph_ltc_lt os oc).
move: lc => [_ c0 cl]; move => /(oltP oc) /cl /cff [z zc h].
have: inc (\aleph (Vf f z)) (range X).
apply /(range_gP pb'); rewrite /X; bw; ex_tac; bw.
move/(card_sup_ub pd); rewrite -/S - sv; move /(aleph_lec_le(proj32 h) os).
by move /oltSleP => /(oleNgt h).
have pi : card_nz_fam X.
by rewrite /X; hnf; bw; move => i idx; bw; apply: aleph_nz; apply: faq.
have ph: (forall i, inc i (domain X) -> Vg X i i ic;bw; rewrite -yv.
apply: aleph_lt_ltc; move: (fap _ ic).
by move /(oltP oc).
set Y := (Lg (domain X) (fun z => x ^c (Vg X z))).
have pf: forall i, inc i (domain X) -> Vg Y i i idx; rewrite /Y; bw.
move: (ph _ idx) => /pa [b [ba /(cpow_less_pr2 x) bb bc]].
exact:(clt_leT bc bb).
have pg: union (range Y) = x ^ t/ (range_gP rb); rewrite /Y; bw; move => [u ud ->]; bw; fprops.
have rc: cardinalp (x ^ re.
rewrite /Y; bw.
apply: cleA.
apply: card_ub_sup => // i /(range_gP rb).
by move=> [z]; rewrite {1}/ Y; bw => /pf [] h _ ->.
apply: card_ub_sup => // i /funI_P [z].
move /(cardinals_ltP (proj1 icy)) => rf ->.
have [t tr xt]: exists2 t, inc t (range X) & z <=c t.
ex_middle bad; case:(cltNge rf).
have ccz := proj31_1 rf.
rewrite -pe; apply : card_ub_sup => //.
move => j jr; case: (cleT_ee (pd _ jr) (proj31_1 rf)) => //.
move => zj; case: bad; ex_tac.
apply: (cleT (cpow_Meqle xnz xt)).
have fgx:fgraph X by rewrite /X; fprops.
move: tr => /(range_gP fgx) [v va ->].
apply: card_sup_ub => //; apply /(range_gP rb); bw.
exists v; bw => //; rewrite /Y; bw.
exists X; split => //; rewrite /X; bw.
Qed.
Lemma cpow_less_ec_pr6 x y:
infinite_c y -> \2c <=c x ->
~ (exists a, cpow_less_ec_prop x y a) ->
\cf (x ^ pa pb pc.
symmetry.
move: (cpow_less_ec_pr5 pa pb pc) => [X [q1 q2 q3 q4 q5]].
have icz: infinite_c (x ^ x ^c Vg X z)) by fprops.
move: (icz) => [[oz _] _]; move: (icz) => [cz _].
apply: cleA; last first.
move: q5; set v := range _ => e1.
have h: sub v (x ^ t /(range_gP fgY); bw; move => [z /q3 h ->].
by move :(oclt h) => /(oltP oz).
move: (cofinality_pr8 oz h e1).
move: (range_smaller fgY); rewrite -/v q1; bw.
rewrite (card_card (CS_cofinality (proj1 (proj1 pa)))) => l1 l2.
exact: cleT l2 l1.
move: (cofinality_pr4 oz).
move => [f [[[ff sf tf] cff] fb] fc].
have xnz:= (card_ge2_nz pb).
have ra: forall a, a exists b, [/\ a a ay; ex_middle bad; case: pc; exists a; split => //.
move => b ab lby; ex_middle ne.
case: bad; exists b; split => //; split => //; first by dneg eq0; rewrite eq0.
exact (cpow_Meqle xnz ab).
have rb: forall i, inc i (source f) ->
exists t, inc t y /\ cardinal (Vf f i) <=c x ^c t.
move => i isf.
have /(oltP oz) la: inc (Vf f i) (x ^ lb.
move:pa => [cy _]; move: (cy) => [oy _].
move: (clt_sup (@cpow_less_pr0 x y) lb) => [v /funI_P[w]].
move /(cardinals_ltP cy)=> /oclt => rb -> rc.
by exists w; split => //; apply /(oltP oy).
pose g i := choose (fun t => inc t y /\ cardinal (Vf f i) <=c x ^c t).
have gp: forall i, inc i (source f) ->
inc (g i) y /\ cardinal (Vf f i) <=c x ^c (g i).
move => i /rb h; apply: (choose_pr h).
move: (fun_image_smaller (source f) g).
have oy:=(proj1 (proj1 pa)).
set G := fun_image (source f) g; rewrite sf (card_card (CS_cofinality oz)).
have sgy: sub G y by move => t /funI_P [z /gp [ h _] ->].
suff ugy: \osup G = y by apply: cleT; exact (cofinality_pr8 oy sgy ugy).
have osy: ordinal_set y by move => t/(ordinal_hi oy).
have ->: y = union y.
by move: (limit_nonsucc (infinite_card_limit2 pa)).
apply: (ord_sup_1cofinal) => //; split => // a /(oltP oy) lay.
have oa:= proj31_1 lay.
move /(ocle2P (proj1 pa) oa): lay => /ra [b [sa sb sc]].
have: inc (x ^c b) (x ^ [b' [b1 b2 b3]].
move: (clt_leT b3 (cpow_less_pr2 x b2)).
apply: oclt.
rewrite - sf in cff; move /cff => [c c1 /ocle1 c2].
exists (g c); first by apply/funI_P; ex_tac.
move/gp: c1 => [sd se].
move: (cleT c2 se); rewrite (card_card (CS_pow x b)) => sg.
case: (oleT_ee oa (ordinal_hi oy sd)) => //.
move /ocle1 => /(cpow_Meqle xnz); rewrite cpowcr => l3.
by move: (clt_leT sc (cleT sg l3)) => [].
Qed.
Lemma cpow_less_ec_pr7 x y z (p := (x ^ \2c <=c x ->
[/\ ( \1c <=c z -> z p = x ^ z p = x ^c y) &
(y <=c z -> p = x ^c z)].
Proof.
move => icy x2.
have ia:= (cpow_less_ec_pr0 icy x2).
have ca := proj1 ia.
have aux: forall z, infinite_c z -> \cf z <=c z.
move =>t icz;move: (icz) => [cz _]; move:(cz) => [oz _].
apply: ocle3 => //; first by apply: CS_cofinality.
by apply: cofinality_pr3.
have cfys := (aux _ icy).
case: (p_or_not_p (exists a, cpow_less_ec_prop x y a)).
move => [a ha]; split.
- move=> z1 z2.
have znz: z <> \0c by move/cge1P:z1 => [_ /nesym].
have hb:= (cpow_less_ec_pr2 ha x2).
have pb:= (clt_leT z2 cfys).
have cz := (proj31_1 z2).
rewrite /p.
case: (finite_dichot cz) => fz.
have zN: natp z by apply /NatP.
by rewrite (cpow_inf ia zN znz).
have [b [b1 b2 b3]]: exists b, [/\ a <=c b, z <=c b & b [ay _]; move: (ay) => [[ca1 _] _ _].
case: (cleT_ee ca1 cz) => le1.
by exists z; split => //; apply: cleR.
exists a; split;fprops.
have ib:=(ge_infinite_infinite fz b2).
by rewrite /p (hb _ b1 b3) - cpow_pow (cprod_inf b2 ib znz).
- move => pa pb.
have sy: singular_cardinal y.
by split => //; move: (cle_ltT pa pb) => [_].
move: (cpow_less_ec_pr3 ha x2 sy) => [pc pd].
rewrite /p pd - cpow_pow (cprod_inf (proj1 pb) icy) //.
move: (cofinality_infinite_cardinal icy) => i1.
exact: (infinite_nz (ge_infinite_infinite i1 pa)).
- move => yz.
move: (cpow_less_ec_pr2 ha x2) => hb.
move: ha => [ay _];move: (ay) => [[oa _] _ _].
case: (equal_or_not a \0c) => az.
have y1: \1c ab.
rewrite /p (hb _ ab y1) (cpowx1 (proj32 x2)) //.
rewrite /p (hb _ (cleR oa) ay) - cpow_pow (cprodC).
have iz:= (ge_infinite_infinite icy yz).
by rewrite (cprod_inf (cleT (proj1 ay) yz) iz az).
move => ha.
have hb:= (cpow_less_ec_pr6 icy x2 ha).
move: (cpow_less_ec_pr5 icy x2 ha) => [X].
set Y := Lg (domain X) (fun z0 : Set => x ^c Vg X z0).
move => [q1 q2 q3 q4 q5].
have fgY: fgraph Y by rewrite /Y; fprops.
have q6: cardinal_fam Y by rewrite /Y; hnf;bw;move => t td; bw; fprops.
have q10: csum Y = x ^ z p = x ^ z1 zcy.
rewrite -hb in zcy.
have znz: z <> \0c by move/cge1P:z1 => [_ /nesym].
rewrite /p (infinite_power7 ia zcy znz) /csumb.
set T := Lg _ _.
have pa: (forall i, inc i (domain T) -> Vg T i <=c x ^ i id; bw.
move: id => /(cardinals_ltP ca) => le2.
have csr: cardinal_set (range Y).
by move => t /(range_gP fgY) [w wi ->]; apply: q6.
move: le2; rewrite - {1} q5 => le2.
move: (clt_sup csr le2); move => [v ].
move /(range_gP fgY); rewrite /Y;bw; move => [w wdx ->]; bw => le3.
case: (equal_or_not i \0c) => iz.
rewrite iz (cpow0x znz); apply: (czero_least ca).
move: (cpow_Mleeq z le3 iz); rewrite - (cpow_pow) => pb.
apply (cleT pb); apply: (cpow_less_pr2).
move: (q2 _ wdx) => le1.
rewrite hb in zcy; move: (clt_leT zcy cfys) => le4.
by apply: cprod_inf5.
have ct: cardinal_fam T by rewrite /T; hnf;bw; move => a ad;bw; fprops.
have ct': fgraph T by rewrite /T; fprops.
have dt: domain T = cardinals_lt (x ^ [le2 tnz].
have snz: csum T <> \0c.
have zt: inc \1c (domain T).
rewrite /T; bw; apply /(cardinals_ltP ca).
apply: (finite_lt_infinite finite_1 ia).
move: (csum_increasing6 ct zt).
move: zt; rewrite {1}/T; bw => zt;rewrite {1} /T; bw.
by rewrite cpow1x; move/cge1P => [_ /nesym].
rewrite (cprod_inf le2 ia tnz) => le3.
by rewrite cprodC (cprod_inf le3 ia snz).
case: (equal_or_not y omega0) => yo.
split => //.
by move:regular_omega => [ra rb];rewrite yo rb => l1 /(cleNgt l1).
move => yz;rewrite /p yo.
have oic:= CIS_omega.
have o2:=(finite_le_infinite finite_2 oic).
rewrite yo in yz.
have icz: infinite_c z by apply: (ge_infinite_infinite oic yz).
case: (finite_dichot (proj32 x2)) => fx.
rewrite (cpow_less_pr5c x2 fx).
rewrite (infinite_power1_a o2 yz icz).
by rewrite (infinite_power1_a x2 (finite_le_infinite fx icz) icz).
by rewrite (cpow_less_pr5e fx).
have xnz:= (card_ge2_nz x2).
have pa: forall z, infinite_c z -> (x ^ (Vg X t) *c z))).
move => w wi; rewrite - q10.
have pb: (forall i, inc i (domain Y) -> \2c <=c Vg Y i).
rewrite /Y; bw => i idx; bw.
move: (q4 yo _ idx) => enz.
exact: (cleT x2 (cpow_Mle1 (proj32 x2) enz)).
have le1 := (compare_sum_prod1 pb).
have le0: csum Y <> \0c by rewrite q10; apply: infinite_nz.
apply: (cleT (cpow_Mleeq w le1 le0)).
rewrite (cpow_prod _ Y) cpow_sum /Y.
rewrite /cprodb.
rewrite Lg_domain Lg_domain; set f1 := Lg _ _; set f2 := Lg _ _.
have ->: f1 = f2 by apply: Lg_exten => t te; bw; rewrite - cpow_pow.
apply: cleR; rewrite /cprod; fprops.
move: (cofinality_infinite_cardinal icy) => cyi.
split => //.
move => p1 p2.
have icz: (infinite_c z) by apply: (ge_infinite_infinite cyi p1).
move: (pa _ icz); set f := Lg _ _ => pb.
have pc: csum f <=c y.
have df: domain f = \cf y by rewrite /f; bw; ue.
have cf0: fgraph f by rewrite /f; fprops.
have cf2: (forall i, inc i (domain f) -> Vg f i <=c y).
rewrite /f; bw => i idx; bw; rewrite cprodC.
apply: (cprod_inf4 (proj1 p2) (proj1 (q2 _ idx)) icy).
move: (csum_of_small_b1 (conj cf0 cf2)).
by rewrite df (cprod_inf cfys icy (infinite_nz cyi)).
apply:cleA; first by apply: (cleT pb (cpow_Meqle xnz pc)).
rewrite /p (cpow_less_pr6 icy x2);
apply: (cpow_Meqle (infinite_nz ia) p1).
move => p1.
have icz: (infinite_c z) by apply: (ge_infinite_infinite icy p1).
move: (pa _ icz); set f := Lg _ _ => p2.
have pb: x ^c csum f <=c x ^c z.
apply: (cpow_Meqle xnz).
have cf1: fgraph f by rewrite /f; fprops.
have cf2: (forall i, inc i (domain f) -> Vg f i <=c z).
rewrite /f; bw => i idx; bw; rewrite cprodC.
apply: cprod_inf1 => //.
exact (cleT (proj1 (q2 _ idx)) p1).
have df: domain f = \cf y by rewrite /f; bw; ue.
move: (csum_of_small_b1 (conj cf1 cf2))=> l3; apply:(cleT l3).
rewrite df; exact: (cprod_inf1 (cleT cfys p1) icz).
apply: (cleA (cleT p2 pb)).
exact: (cpow_Mleeq z (cpow_less_pr5a (proj32 x2) (infinite_ge2 icy)) xnz).
Qed.
(** inaccessible cardinals *)
Lemma inaccessible_pr2 x: inaccessible_w x ->
cardinal (Zo x regular_cardinal) = x.
Proof.
move=> ix; move: ix (inaccessible_pr1 ix) => [rx [n ln xv]] xx.
have cx: cardinalp x by apply: (proj1 (proj1 rx)).
rewrite - {2} (card_card cx).
apply: cleA; first by apply: sub_smaller; apply Zo_S.
set S := (Zo x regular_cardinal).
have ox:= proj1 cx.
have lx: limit_ordinal x.
suff : x = n by move => ->.
apply:aleph_inj => //; [ by move: ln => [] | by ue].
have oo:= OS_aleph ox.
have pa: forall i, inc i x -> inc (\aleph (osucc i)) S.
move=> i ix; apply: Zo_i.
rewrite xx; apply /(oltP oo); apply: aleph_lt_lto.
by apply/(oltP ox); move: lx => [_ _ ]; apply.
apply: regular_initial_successor; apply: (ordinal_hi ox ix).
set f := Lf (fun z => (\aleph (osucc z))) x S.
have inf: injection f.
apply: lf_injective => // u v ux vx sv.
have ou:= (ordinal_hi ox ux).
have ov :=(ordinal_hi ox vx).
apply: ord_succ_inj => //; apply: aleph_inj; fprops.
have ->: x = source f by rewrite /f; aw.
have ->: S = target f by rewrite /f; aw.
by apply: incr_fun_morph.
Qed.
Definition next_dominant x :=
the_least_fixedpoint_ge (cpow \2c) x.
Definition card_dominant x:=
infinite_c x /\ forall a b, a b a ^c b
x <> \0c -> (forall m, m \2c ^c m card_dominant x.
Proof.
move=> cx xnz h.
have ix: infinite_c x.
case: (finite_dichot cx) => // fx.
have xN: natp x by apply /NatP.
move: (cpred_pr xN xnz) => [pa pb].
have pc: (cpred x) h1.
case: (cleNgt h1 (cantor (proj32 h1))).
split => //.
move=> a b ax bx.
case: (equal_or_not b \0c) => bz.
rewrite bz cpowx0; apply: finite_lt_infinite => //.
rewrite /NatP; fprops.
case: (equal_or_not a \0c) => az.
rewrite az cpow0x // ; apply: finite_lt_infinite => //.
rewrite /NatP; fprops.
have [c [ca cb ccx]]: exists c, [/\ a <=c c, b <=c c & c fc.
apply: finite_lt_infinite => //.
by apply /NatP; apply NS_pow; apply /NatP.
by rewrite (infinite_power1_b fc); apply h.
Qed.
Lemma card_dominant_pr2: card_dominant omega0.
Proof.
have io: infinite_c omega0 by rewrite - aleph0E; apply: CIS_aleph; fprops.
split => //.
have lo: forall c, c natp c.
move=> c; split => h.
by apply /olt_omegaP; apply: oclt.
by apply: finite_lt_infinite => //; apply /NatP.
move=> a b /lo aN /lo bN; apply/lo; fprops.
Qed.
Lemma next_dominant_pr x (y:= next_dominant x): cardinalp x ->
[/\ card_dominant y , x x y <=c z)].
Proof.
move => cx; rewrite /y /next_dominant; clear y.
rewrite /the_least_fixedpoint_ge.
move: (induction_defined_pr (cpow \2c) x).
set f := induction_defined _ _; move=> [sf [ff sjf f0 fnz]].
have cs1: forall n, natp n -> cardinalp (Vf f n).
apply: Nat_induction; first ue.
move=> n nN _; rewrite (fnz _ nN) /cpow; fprops.
have cs: cardinal_set (target f).
by move => t /sjf; rewrite sf; move=> [u ub <-]; apply: cs1.
set y:= \osup (target f).
have ltxy: x //.
apply: card_dominant_pr1 => //; first by apply: (CS_sup cs).
move => yz; rewrite yz in ltxy; case: (clt0 ltxy).
move=> m my.
have [n pd pe]: exists2 n, inc n (target f) & m <=c n.
ex_middle bad.
have cm:= proj31_1 my.
have pd: forall t, (inc t (target f) -> t <=c m).
move=> t ti.
case: (cleT_ee (cs _ ti) cm) => // b1; case: bad;ex_tac.
case: (cltNge my (card_ub_sup cm pd)).
move: (sjf _ pd) => [u us uv].
have le1: \2c ^c m <=c \2c ^c n by apply: cpow_Meqle; fprops.
have le2: \2c ^c n z [iz dz] xz; apply card_ub_sup; first by exact (proj1 iz).
move => a /sjf; rewrite sf; move=> [n nB <-].
suff : Vf f n [].
move: n nB; apply: Nat_induction; first by ue.
move=> n nB le1; rewrite (fnz _ nB); apply: dz => //.
apply: finite_lt_infinite => //; rewrite /NatP; fprops.
Qed.
Lemma card_dominant_pr3 x (y := next_dominant x) :
cardinalp x -> \2c ^c y = y ^c omega0.
Proof.
move => cx; move: (next_dominant_pr cx); rewrite -/y.
move=> [[iy yp] _].
move: (iy) => [cy _ _].
have oy: omega0 <=c y by apply /infinite_c_P2.
have co:= CS_omega.
apply: cleA; last first.
rewrite -(infinite_power1_b iy).
apply:cpow_Mlele; fprops; by apply: infinite_nz.
move: (induction_defined_pr (cpow \2c) x) => /=.
set f := (induction_defined (cpow \2c) x).
move => [qa [rb qb2] qc qd].
have bv: y = \osup (target f) by done.
have ra: fgraph (Lg omega0 (Vf f)) by fprops.
have bv1: y = \osup (range (Lg omega0 (Vf f))).
rewrite bv; apply: f_equal; set_extens t.
move /qb2=> [u usf <-]; apply /(range_gP ra); bw.
rewrite qa in usf;exists u; bw.
move /(range_gP ra); bw; move => [u usf ]; bw; move => ->; Wtac; ue.
have rd0: forall u, natp u -> cardinalp (Vf f u).
apply: Nat_induction; first ue.
move=> n nN _; rewrite (qd _ nN) /cpow; fprops.
have rd: cardinal_fam (Lg omega0 (Vf f)) by hnf; bw => t tw; bw; fprops.
have bv2: y = csum (Lg omega0 (Vf f)).
by rewrite csum_of_small_b4 // - bv1 //; bw; rewrite (card_card co).
rewrite {1} bv2 cpow_sum; bw; rewrite - cpow_pr2.
have cs1: (cardinal_set (target f)).
by move => t /qb2 [u usf <-];apply: rd0; rewrite /natp - qa.
apply: cprod_increasing; bw => t tN; bw.
by rewrite -(qd _ tN); apply: (card_sup_ub cs1); Wtac;rewrite qa; apply:NS_succ.
Qed.
Definition least_non_trivial_dominant := next_dominant omega0.
Lemma card_dominant_pr4 (b:= least_non_trivial_dominant):
[/\ card_dominant b,
omega0 omega0 b <=c z),
(b ^c omega0 = omega0 ^c b)
& (b ^c omega0 = \2c ^c b) /\
(b ^c omega0 = (\2c ^c b) ^c b) ].
Proof.
have co:= CS_omega.
move: (next_dominant_pr co) (card_dominant_pr3 co).
rewrite (_: (next_dominant omega0) = b ) //.
move => [pa pb pc] pd; move: (pa) => [pf _].
have io: infinite_c omega0 by rewrite - aleph0E; apply: CIS_aleph; fprops.
have pe: omega0 ^c b = \2c ^c b.
apply: infinite_power1_a => //.
apply: finite_le_infinite;fprops.
apply: (proj1 pb).
by rewrite - cpow_pow (csquare_inf pf) pe pd.
Qed.
Lemma dominant_limit a: ordinalp a ->
~ (card_dominant (\aleph (osucc a))).
Proof.
move=> oa [cd1 cd2].
set x := \omega a.
rewrite - (cnextE oa) in cd2.
move: (CIS_aleph oa) => icx.
move: (cnext_pr2 (proj1 icx))(cnext_pr3 (proj1 icx)) => lt1 pa.
by move: (cd2 _ _ lt1 lt1); rewrite (infinite_power1_b icx) => /cltNge.
Qed.
Lemma card_dominant_pr5 x: card_dominant x ->
(\2c ^ [icx cdx].
suff pa: \2c ^ [cx _].
have aux:= (@cpow_less_pr0 \2c x).
apply: cleA.
apply:card_ub_sup => //i /funI_P [z zi ->].
have pa:=(finite_lt_infinite finite_2 icx).
move: zi => /(cardinals_ltP cx) pb.
exact (proj1 (cdx _ _ pa pb)).
by case: (cpow_less_compare icx).
Qed.
(* x is y-strong *)
Definition rel_strong_card x y:=
forall t, t t ^c y \aleph z ^c B))):
rel_strong_card A B -> B <> \0c -> ordinalp a ->
(s <=c A /\ (limit_ordinal a -> s = A)).
Proof.
move => sab bnz oa.
have cA:= (CS_aleph oa).
move: (CIS_aleph oa); rewrite -/A => iA.
have pa: s <=c A.
apply: card_ub_sup => // i /funI_P [z za ->].
have lt1: \omega z /oltP [].
exact: (proj1 (sab _ lt1)).
split => // la.
set g := (fun z => \omega z ^c B).
set f := (fun z => \omega z).
have pb: (forall x, inc x a -> f x <=c g x).
move => x xa; rewrite /f/g.
have ox:= ordinal_hi oa xa.
apply: (cpow_Mle1 (CS_aleph ox) bnz).
apply: cleA; first by exact.
apply: cleT (card_sup_image pb).
move: aleph_normal => [_ h]; move: (h _ la).
have ->: (fun_image a \omega) = (fun_image a f) by set_extens t; bw.
move => <-; apply: cleR; apply: (CS_aleph oa).
Qed.
Lemma card_dominant_pr8 a b (A := \aleph a) (B:= \aleph b) (X := A ^c B):
ordinalp a -> ordinalp b -> rel_strong_card A B ->
( (B X = A) /\ (\cf A <=c B -> X = gimel_fct A)).
Proof.
move => oa ob sab.
move: (CIS_aleph oa) (CIS_aleph ob) => ia ib.
move: (infinite_power9 ia ib) => [_ _ i9]; exact (i9 sab).
Qed.
Definition the_nondominant_least A B :=
select (fun z => [/\ z A <=c t ^c B -> z <=c t)]) A.
Lemma the_nondominant_least_pr1 A B (C:= the_nondominant_least A B):
~ (rel_strong_card A B) -> cardinalp A ->
[/\ C A <=c t ^c B -> C <=c t)].
Proof.
move => h cA.
rewrite /C/the_nondominant_least.
apply select_pr; last first.
move => x y p1 [p2 p3 p4] q1 [q2 q3 q4].
exact: (cleA (p4 _ q2 q3) (q4 _ p2 p3)).
pose p c := c u ua.
have cp: cardinalp (u ^c B) by fprops.
case: (cleT_el (proj32_1 ua) cp) => // h2.
case: h1; exists u; rewrite /p;split => //.
have oc: ordinalp c by move: cp => [[[[cx _] _] _] _].
move: (least_ordinal4 oc cp);set z := least_ordinal _ _.
move=> [_ [p1 p2] p3].
have iaa: inc z A.
by move: (oclt p1) => /oltP0 [_ _].
ex_tac;split => // => t ta le.
have pt: (p t) by split.
have ot: ordinalp t by move: pt => [[[[cx _] _] _] _].
move: (ocle1 (p3 _ ot pt)).
rewrite (card_card (proj31_1 p1)).
by rewrite (card_card (proj31_1 (proj1 pt))).
Qed.
Lemma the_nondominant_least_pr2 a b (A := \aleph a) (B:= \aleph b)
(c := (ord_index (the_nondominant_least A B))):
~ (rel_strong_card A B) -> ordinalp a -> ordinalp b ->
(A <=c \2c ^c B) \/
[/\ c A <=c \aleph t ^c B -> c <=o t)].
Proof.
move => h oa ob.
move: (the_nondominant_least_pr1 h (CS_aleph oa)).
set C := the_nondominant_least A B; move => [pa pb pc].
have cc:= proj31_1 pa.
case: (finite_dichot cc) => ifc.
left.
have bnz: B <> \0c by apply: aleph_nz.
have iB:= (CIS_aleph ob).
have cp:= (CS_pow \2c B).
case: (equal_or_not C \0c) => cnz.
move: pb; rewrite cnz (cpow0x bnz) => le2.
exact: (cleT le2 (czero_least cp)).
case: (equal_or_not C \1c) => cno.
move: pb; rewrite cno cpow1x => le2.
exact: (cleT le2 (cge1 cp (@cpow_nz _ B card2_nz))).
have c2:= (cge2 cc cnz cno).
have le1: C <=c B by apply: finite_le_infinite.
have <- //: C ^c B = \2c ^c B by apply: infinite_power1_a.
right.
move: (ord_index_pr1 ifc); rewrite {1 2}/C -/c; move => [oc ac].
have ltca: c //; rewrite ac.
rewrite ac; split => //.
move => t ta tb.
have lt1: \aleph t C A <=c C ^c B -> A ^c B = C ^c B.
Proof.
move => ib ca le1.
case: (equal_or_not C \0c) => cnz.
move: le1; rewrite cnz (cpow0x (infinite_nz ib)) => az.
case: (clt0 (clt_leT ca az)).
have anz: A <> \0c.
move=> h; rewrite h in ca; case: (clt0 ca).
move: (cpow_Mleeq B le1 anz).
rewrite - cpow_pow (csquare_inf ib) -/B => le4.
exact: (cleA le4 (cpow_Mleeq B (proj1 ca) cnz)).
Qed.
Lemma card_dominant_pr10 a b (A := \aleph a) (B:= \aleph b) (X := A ^c B)
(C := (the_nondominant_least A B)):
ordinalp a -> ordinalp b ->
\2c ^c B ~ (rel_strong_card A B) ->
[/\ rel_strong_card C B, singular_cardinal C,
\cf C <=c B, B oa ob lt2 nsr.
move: (CIS_aleph oa) (CIS_aleph ob) => ia ib.
move: (the_nondominant_least_pr1 nsr (proj1 ia)).
rewrite -/C; move => [pa pb pc].
move: (card_dominant_pr9 ib pa pb); rewrite -/A -/B -/C => eq1.
have na2b: ~(A <=c \2c ^c B).
move => bad.
move: (cpow_Mleeq B bad (aleph_nz oa)).
by rewrite - cpow_pow (csquare_inf ib) => /(cltNge lt2).
have cc:=(proj31_1 pa).
case: (cleT_el cc (proj1 ib)) => lBC.
case: na2b.
have cp := (CS_pow \2c B).
case: (equal_or_not C \0c) => cnz.
move: pb; rewrite cnz (cpow0x (aleph_nz ob)) => le2.
exact: (cleT le2 (czero_least cp)).
case: (equal_or_not C \1c) => cno.
move: pb; rewrite cno cpow1x => le2.
exact: (cleT le2 (cge1 cp (@cpow_nz _ B card2_nz))).
by rewrite - (infinite_power1_a (cge2 cc cnz cno) lBC ib).
have pd:rel_strong_card C B.
move => t tC.
case: (cleT_el cc (CS_pow t B)) => // cb.
move: (card_dominant_pr9 ib tC cb); rewrite -/B => le1.
rewrite le1 in pb.
case: (cltNge tC (pc _ (cle_ltT (proj1 tC) pa) pb)).
have ic: infinite_c C by apply: (ge_infinite_infinite ib (proj1 lBC)).
move: (ord_index_pr1 ic); set c:= (ord_index C); move => [oc qb].
rewrite -qb in pd.
move: (card_dominant_pr8 oc ob pd); rewrite qb -/B; move => [pe pf].
rewrite qb in pd.
case: (cleT_el (CS_cofinality (proj1 cc)) (proj1 ib)) => h.
move: (cle_ltT h lBC) => [_ ne].
by rewrite - (pf h) - eq1.
by move: pb; rewrite (pe h) => /(cltNge pa).
Qed.
Lemma card_dominant_pr11 A B (X := A ^c B):
infinite_c A -> infinite_c B ->
[\/ X = A, X = \2c ^c B |
exists C, [/\ infinite_c C, rel_strong_card C B,
\cf C <=c B , B ia ib.
move: (ord_index_pr1 ia); set a:= (ord_index A); move => [oa qa].
move: (ord_index_pr1 ib); set b:= (ord_index B); move => [ob qb].
case: (equal_or_not (\2c ^c B) (A ^c B)) => eq0; first by constructor 2.
have pa: \2c ^c B //; apply: (cpow_Mleeq B (infinite_ge2 ia) card2_nz).
case: (cleT_el (proj1 ia) (proj1 ib)) => cab.
constructor 2; exact :(infinite_power1_a (infinite_ge2 ia) cab ib).
case: (p_or_not_p (rel_strong_card A B)) => sr.
move: (card_dominant_pr8 oa ob); rewrite qa qb => h.
move: (h sr) => [h1 h2].
have cco:=(CS_cofinality (proj1 (proj1 ia))).
case: (cleT_el cco (proj1 ib)) => h3.
constructor 3; exists A;split;fprops.
by constructor 1 ; apply: h1.
move: (card_dominant_pr10 oa ob).
set C := the_nondominant_least _ _; rewrite qa qb.
move => xx; move: (xx pa sr); move => [q1 q2 q4 q5 q6].
constructor 3; exists C; split => //.
apply (ge_infinite_infinite ib (proj1 q5)).
Qed.
Definition inaccessible x :=
inaccessible_w x /\ (forall t, t \2c ^c t Vg f i card_dominant x.
Proof.
move => [[pa1 pa2] pb].
move: pa2 => [n [on _ _] xv].
move: (CIS_aleph on); rewrite - xv => icx.
apply: (card_dominant_pr1 (proj1 icx) (infinite_nz icx) pb).
Qed.
Lemma inaccessible_pr3 x: \2c
(forall f, cprod_of_small f x -> cprod f
card_dominant x.
Proof.
move => cx h.
have ccx := proj32_1 cx.
apply: card_dominant_pr1 => //.
move => p; rewrite p in cx; case: (clt0 cx).
move => m mx; rewrite - cpow_pr2; apply: h; hnf; bw; split => //.
hnf;bw => t te; bw; fprops.
move => t te; bw.
Qed.
Lemma inaccessible_pr4 x: \2c
(forall f, cprod_of_small f x -> cprod f
(x = omega0 \/ (exists2 n, limit_ordinal n & x = \aleph n)).
Proof.
move=> x2 h.
move: (inaccessible_pr3 x2 h) => [pa pb].
move: (ord_index_pr1 pa) => [on xv]; rewrite -xv.
case: (ordinal_trichot on) => ln; last by right; exists (ord_index x).
left; rewrite ln; apply: aleph0E.
move: ln => [m om mv].
move: (cnext_pr1 (CS_aleph om)).
rewrite (cnextE om) - mv xv; move => [pc pd pe].
move: (pb _ _ pd pd); rewrite (infinite_power1_b (CIS_aleph om)).
rewrite - {1} xv mv => /(aleph_pr10a om) => l2.
case: (cleNgt l2 (cantor (proj31_1 pd))).
Qed.
Lemma inaccessible_pr5 x: \2c
(forall f, cprod_of_small f x -> cprod f
(x = omega0 \/ inaccessible x).
Proof.
move=> h1 h2.
case: (inaccessible_pr4 h1 h2) => lx; first by left.
move: (inaccessible_pr3 h1 h2) => [pa pb].
right; split; last by move => t tx; apply: pb.
split => //; split => //.
have H:=(cofinality_card pa).
rewrite H;ex_middle cs.
have pe: \cf x //; exact (cofinality_small pa).
move: (cofinality_c_pr3 pa) =>[f [[qa qb] df sf etc]].
have cff: cardinal_fam f by move => t /qb /proj31_1.
have: cprod_of_small f x by split => //; rewrite df H.
move /h2 => l2.
by move: (compare_sum_prod1 etc); rewrite sf => /(cltNge l2).
Qed.
Lemma inaccessible_pr6 x: inaccessible x ->
(forall f, cprod_of_small f x -> cprod f [[[cx rx] pb] pc] f [pe pf pg].
set z := domain f in pg.
set f' := (Lg z (Vg f)).
have df' : domain f' = z by rewrite /f'; bw.
have pa: csum_of_small1 x f'.
by rewrite /f';split; fprops;hnf; bw => i idf; bw; apply: pf.
have cff: cardinal_fam f' by move => t /(proj2 pa) /proj31_1.
set su := csum f'.
have sux: su <=c x.
move: (csum_of_small_b2 pa); rewrite df' => qb.
exact: (cleT qb (cprod_inf1 (proj1 pg) cx)).
case: (equal_or_not su x) => sux1.
have: cofinality_c x <=o z.
move: (cofinality_c_rw (infinite_ge2 cx)) => [_ _ cfxp].
by apply: (cfxp _ (proj1 (proj31_1 pg))); exists f'.
by move: (oclt pg); rewrite rx => qa /(oltNge qa).
have dx:card_dominant x.
apply: card_dominant_pr1 => //; [ exact: (proj32 sux) | by apply infinite_nz].
apply: cle_ltT ((proj2 dx) _ _ (conj sux sux1) pg).
rewrite - cpow_pr2; apply cprod_increasing; rewrite /cst_graph; bw.
move => i idf; bw.
have udf': inc i (domain f') by ue.
move: (csum_increasing6 cff udf'); rewrite {1}/f'; bw.
Qed.
Lemma inaccessible_pr7 x y: inaccessible x ->
y <> \0c -> y x ^c y = x.
Proof.
move => [[[icx cfx] pb] pc] pd pe.
rewrite (cofinality_card icx) in cfx.
rewrite - cfx in pe.
move: (icx) => [cx _].
rewrite (infinite_power7 icx pe pd) /csumb.
set f := Lg _ _.
have cff: cardinal_fam f.
rewrite /f; hnf;bw; move => a adf; bw; fprops.
have snz: csum f <> \0c.
have zi: inc \1c (cardinals_lt x).
by apply /(cardinals_ltP cx); apply: infinite_gt1.
have zi1: inc \1c (domain f) by rewrite /f; bw.
move: (csum_increasing6 cff zi1); rewrite {1}/f; bw; rewrite cpow1x.
by move => qa qb; rewrite qb in qa; move: (cleNgt qa clt_01).
rewrite cprodC; apply: (cprod_inf) => //.
have dx:card_dominant x.
by apply: card_dominant_pr1 => //; apply infinite_nz.
rewrite cfx in pe.
have pf: csum_of_small1 x f.
rewrite /f;split; fprops; hnf; bw; move => i idf; bw.
by move: idf => /(cardinals_ltP cx) => idf;apply (proj2 dx).
move: (csum_of_small_b2 pf) => le1.
have df: cardinal (domain f) <=c x.
rewrite /f; bw.
by case: (infinite_power7d cx (infinite_nz icx)).
by move: (cprod_inf1 df icx);rewrite cprod2cr; apply: cleT.
Qed.
Lemma inaccessible_pr8 x: inaccessible x -> x = x ^ h; move: (h) => [[[pa1 pa2] pb] pc]; move: (proj1 pa1) => cx.
apply: cleA.
by move: (cpow_less_pr2 x (infinite_gt1 pa1)); rewrite (cpowx1 cx).
apply: card_ub_sup => // t /funI_P [z z1 ->].
move: z1 => /(cardinals_ltP cx) => z1.
case: (equal_or_not z \0c) => xnz.
rewrite xnz cpowx0; apply (proj1 (infinite_gt1 pa1)).
move: (inaccessible_pr7 h xnz z1) => ->.
apply: (cleR (proj32_1 z1)).
Qed.
Lemma inaccessible_dominant1 x:
card_dominant x ->
(x = omega0 \/ (exists2 n, limit_ordinal n & x = \aleph n)).
Proof.
move => [pa pb].
move: (ord_index_pr1 pa); set c := ord_index x; move => [pd pe].
case: (ordinal_trichot pd) => ln;last by right; exists c.
by left; rewrite -pe ln aleph0E.
move: ln => [m om mv].
set y:= \aleph m.
have yx: y le1.
by move: (cnext_pr3(CS_aleph om));rewrite (cnextE om) -mv pe => /(cltNge le1).
Qed.
Lemma inaccessible_dominant2 x
(p1 := forall z, \0c z x ^c z = x)
(p2:= forall z, \0c x ^c z = x *c \2c ^c z):
[/\ (infinite_c x -> p1 -> p2),
(card_dominant x -> (p1 <-> p2)),
(card_dominant x -> p1 -> (x = omega0 \/ inaccessible x)) &
(x = omega0 \/ inaccessible x -> (card_dominant x /\ p1))].
Proof.
have r1:infinite_c x -> p1 -> p2.
move=> icx hp1 z zp.
have x2:= (infinite_ge2 icx).
have xnz:=(infinite_nz icx).
have cz:= proj32_1 zp.
case: (cleT_ee (proj1 icx) (CS_pow \2c z)) => le1.
have icp:= (ge_infinite_infinite icx le1).
case: (finite_dichot cz) => icz.
have f1: finite_c (\2c ^c z).
by apply /NatP; apply NS_pow; fprops.
case: (infinite_dichot1 f1 icp).
rewrite (infinite_power1 x2 le1 icz).
by rewrite cprodC cprod_inf.
have pnz: \2c ^c z <> \0c by apply: cpow2_nz.
rewrite (hp1 _ zp (clt_leT (cantor cz) le1)).
rewrite cprod_inf //.
have r2: card_dominant x -> (p1 <-> p2).
move=> [icx cdx]; split; first by apply: r1.
move => hp2 z z0 zx.
have pnz: \2c ^c z <> \0c by apply: cpow2_nz.
move: (cdx _ _ (finite_lt_infinite finite_2 icx) zx) => [l1 _].
rewrite (hp2 _ z0) cprod_inf //.
have r3: card_dominant x -> p1 -> x = omega0 \/ inaccessible x.
move => pa pc; case: (inaccessible_dominant1 pa); first by left.
move => h; right.
move: pa => [pa pb].
split; last first.
by move => t tx; apply: pb => //; apply: (finite_lt_infinite finite_2 pa).
split; last by exact.
have h1:= (cofinality_c_small (infinite_ge2 pa)).
split => //; ex_middle eq1.
have pd: \0c [_].
split => //.
case => ix.
rewrite ix; split; first by apply: card_dominant_pr2.
move => z z0 zf.
have pa: infinite_c x by rewrite ix; apply: CIS_omega.
have pb: natp z by rewrite ix in zf; move:(oclt zf) => /oltP0 [_ _].
have pc: z <> \0c by move: z0 => [_] /nesym.
by rewrite cpow_inf.
split; first by apply: inaccessible_dominant.
by move => z [_ /nesym zc] zx;apply: inaccessible_pr7.
Qed.
Lemma inaccessible_dominant3 x: omega0
(inaccessible x <->
( (forall a b, a b a ^c b z x ^c z = x))).
Proof.
move => [h1 h2].
have ix: infinite_c x by apply /infinite_c_P2.
move: (inaccessible_dominant2 x) => [pa pb pc pd]; split.
move => h; move: (pd (or_intror h)) => [[_ pe] pf]; split => //.
move => [h3 h4].
by case: (pc (conj ix h3) h4) => // eq; move: h2; rewrite eq.
Qed.
Lemma cofinality_sum1 a: ordinalp a ->
\cf (\aleph(a +o omega0)) = omega0.
Proof.
move => oa.
rewrite (regular_initial_limit1 (osum_limit oa omega_limit)).
rewrite (cofinality_sum oa olt_0omega).
exact (proj2 regular_omega).
Qed.
Lemma cofinality_sum2 a: ordinalp a ->
singular_cardinal (\aleph(a +o omega0)).
Proof.
move => oa; move: (OS_sum2 oa OS_omega) => os.
split; first by apply: CIS_aleph.
rewrite (cofinality_sum1 oa) - {1} aleph0E => h.
symmetry in h; move: (aleph_inj os OS0 h) => /(osum2_zero oa OS_omega) [_].
by move: omega_nz.
Qed.
Lemma singular_non_collectivizing:
not (exists E, forall x, singular_cardinal x -> inc x E).
Proof.
move=> [E ep].
set F := Zo E singular_cardinal.
have ce: cardinal_set F by move => t /Zo_P [_ [[pa _] _]].
move: regular_initial_limit4 => h.
have ef: inc (\aleph omega0) F by apply: Zo_i => //; apply: ep.
move: (ge_infinite_infinite (CIS_aleph OS_omega) (card_sup_ub ce ef)) => ins.
move: (ord_index_pr1 ins) =>[]; set n := ord_index _ => on yv.
have h1:= (cofinality_sum2 on).
have xf: inc (\aleph (n +o omega0)) F by apply: Zo_i => //; apply: ep.
move: (card_sup_ub ce xf); rewrite -yv => h2.
move: (aleph_lec_le (OS_sum2 on OS_omega) on h2).
by move: (osum_Meqlt olt_0omega on); rewrite (osum0r on) => pa /(oltNge pa).
Qed.
Lemma genconthypothesis_alt b: ordinalp b ->
(forall a, ordinalp a -> \2c ^c (\aleph a) = \aleph (a +o b)) ->
b ob h.
have oo:= OS_omega.
case: (oleT_el oo ob) => // lob.
pose p x := b [oa pa al].
have ab: a <=o b by apply: al.
have a0: \0o nz; first by case: (proj2 a0).
move: nz => [m om mv].
have pm: p m.
move: OS1 pa; rewrite /p mv => o1.
rewrite - osucc_pr // - osumA // osum_1inf //.
by move: (al _ om pm); rewrite mv; move/(oltNge (oltS om)).
set k := \aleph (a +o a).
have oaa:=(OS_sum2 oa oa).
have sk: singular_cardinal k.
split; first by apply:CIS_aleph.
have laa:= (osum_limit oa nz).
have anz: a <> \0o by apply: limit_nz.
rewrite /k (regular_initial_limit1 laa) (cofinality_sum oa a0).
move=> bad; move: (cofinality_pr3 oa); rewrite bad.
move: (aleph_pr6 oaa) => le1 le2.
case: (oltNge paa (oleT le1 le2)).
set s1 := \aleph (a +o b).
have pc : forall c, c \2c ^c (\aleph (a +o c)) = s1.
move => c ca.
have oc:= proj31_1 ca.
have oac: ordinalp (a +o c) by apply: OS_sum2 => //.
rewrite (h _ oac) - (osumA oa oc ob).
have <- //: b = (c +o b).
ex_middle neq.
have p1: b <=o c +o b by apply osum_M0le.
case: (oltNge ca (al _ oc (conj p1 neq))).
have pd: forall c, a<=o c -> c \2c ^c (\aleph c) = s1.
move=> c ac caa; move: (odiff_pr ac) => [qa qb].
rewrite qb in caa; move: (osum_Meqltr qa oa oa caa) => da.
by move: (pc _ da); rewrite -qb.
have px: (cpow_less_ecb k).
exists (\aleph a); first by apply: (aleph_lt_ltc paa).
move=> c c1 c2.
move: (ge_infinite_infinite (CIS_aleph oa) c1) => ic.
move: (ord_index_pr1 ic) => [om mv].
rewrite (pd _ (oleR oa) paa).
rewrite -mv in c1 c2.
have p1:= (aleph_lec_le oa om c1).
have p2:= (aleph_ltc_lt om oaa c2).
by rewrite -mv (pd _ p1 p2).
move: (cpow_less_pr10 sk px); rewrite (h _ oaa).
set s2 := \aleph ((a +o a) +o b) => eq1.
have c12: s1 //.
suff: \2c ^ /(cltNge c12).
apply:card_ub_sup; first exact: (proj31_1 c12).
move => i /funI_P [z zv ->].
have ck: cardinalp k by move: sk => [[ok _] _].
move: zv => /(cardinals_ltP ck) zv.
have cz:=proj31_1 zv.
have is1: infinite_c s1 by apply: CIS_aleph; apply: OS_sum2.
case: (finite_dichot cz) => fz.
apply: finite_le_infinite => //.
by apply /NatP; apply: NS_pow; fprops; apply /NatP.
move: (ord_index_pr1 fz)=> [om zv1].
have lt1: (ord_index z) le1.
by rewrite (pd _ le1 lt1); apply: cleR; move: is1 => [].
by rewrite (h _ om); apply: aleph_le_lec; apply: osum_Mleeq.
Qed.
Section GenContHypothesis_Props.
Hypothesis gch: GenContHypothesis.
Lemma infinite_power10 x y (z := x ^c y): infinite_c x ->
[/\ (y = \0c -> z = \1c),
(y <> \0c -> y z = x),
(\cf x <=c y -> y <=c x -> z = cnext x)&
(x z = cnext y)].
Proof.
move=> ic; rewrite /z.
have x2:= (infinite_ge2 ic).
have cx:= proj1 ic.
have xx:=(cleR cx).
have xnz:= infinite_nz ic.
have r1: y = \0c -> x ^c y = \1c by move => ->; rewrite cpowx0.
have r2: x x ^c y = cnext y.
move=> [xy _].
have icy:(infinite_c y) by apply: (ge_infinite_infinite ic xy).
rewrite (gch icy); apply: (infinite_power1_a _ xy icy).
apply: finite_le_infinite => //; rewrite /NatP; fprops.
move: (cnext_pr1 cx) => [qa qb qc].
have r3: \cf x <=c y -> y <=c x -> x ^c y = cnext x.
move=> pa pb.
move: (power_cofinality x2); rewrite (cofinality_card ic) => pc.
have pd: x ^c (\cf x) <=c x ^c y by apply: cpow_Mlele.
have lt1:= (qc _ (clt_leT pc pd)).
apply: cleA lt1.
rewrite (gch ic) - (infinite_power1_b ic).
by apply: cpow_Mlele.
split => // ynz ycx.
have cy := (proj31_1 ycx).
have yl1:=(cge1 cy ynz).
apply: cleA; last by apply: cpow_Mle1.
rewrite (infinite_power7 ic ycx ynz) /csumb.
set f := Lg _ _.
have cf: cardinal_fam f by rewrite /f;hnf;bw => a ac; bw; fprops.
have fl: forall i, inc i (domain f) -> Vg f i <=c x.
rewrite /f; bw; move=> i id; bw.
case: (equal_or_not i \0c) => iz.
rewrite iz (cpow0x ynz); apply: czero_least; rewrite /cpow; fprops.
case: (equal_or_not i \1c) => io.
rewrite io (cpow1x); apply: finite_le_infinite => //; apply: finite_1.
move: id => /(cardinals_ltP cx) lt.
have ci:= proj31_1 lt.
case: (Nat_dichot cy) => yN.
case: (Nat_dichot ci) => iN.
by apply: (finite_le_infinite _ ic); apply /NatP;apply: NS_pow.
exact: (cleT (cpow_inf1 iN yN) (proj1 lt)).
have ra: forall t, infinite_c t -> t \2c ^c t <=c x.
move=> t it tx.
by rewrite - (gch it); move: (cnext_pr1 (proj1 it))=> [ _ _]; apply.
have ray: \2c ^c y <=c x.
by apply: ra => //; apply: (clt_leT ycx); apply: cofinality_small.
case: (Nat_dichot ci) => iN.
have b1:= NS1.
have iy: i <=c y by apply (Nat_le_infinite).
have i2: \2c <=c i.
rewrite - succ_one ; apply /(cleSltP b1).
by split; [apply: cge1 | apply:nesym].
rewrite (infinite_power1_a i2 iy yN) //.
have i2:= (finite_le_infinite finite_2 iN).
case: (cleT_ee ci cy) => cp1.
rewrite (infinite_power1_a i2 cp1 yN) //.
have le1: i ^c y <=c i ^c i by apply: cpow_Mlele => //; fprops.
apply: (cleT le1).
rewrite (infinite_power1_b iN); exact: (ra _ iN lt).
have df: domain f = (cardinals_lt x) by rewrite /f; bw.
move: (infinite_power7d cx xnz)=> [pe pf].
have fgf: fgraph f by rewrite /f; fprops.
move: (csum_of_small_b1 (conj fgf fl)).
rewrite {2} /f; bw; rewrite - (cprod2cr)(cprod_inf pe ic pf) => aux.
by apply cprod_inf4.
Qed.
Lemma infinite_power10_a x: infinite_c x ->
x ^c (\cf x) = cnext x.
Proof.
move => icx; move: (infinite_power10 (\cf x) icx) => [_ _ pa _].
have h:=(cofinality_small icx).
apply: pa => //;apply (cleR (proj31 h)).
Qed.
Lemma infinite_power10_b x y:
infinite_c x -> y y <> \0c ->
x ^c y = x.
Proof.
move=> icx yc ynz.
by move: (infinite_power10 y icx) => [_ pb _ _]; apply: pb.
Qed.
Lemma cpow_less_pr11a x y:
infinite_c y -> \2c <=c x -> finite_c x ->
x ^ icy x2 xf.
have cy := proj1 icy.
have cs:= (@cpow_less_pr0 y x).
have le1: x ^ // i /funI_P [z /(cardinals_ltP cy) zs ->].
have cz:=proj31_1 zs.
case: (finite_dichot cz) => fz.
apply: finite_le_infinite => //.
by apply /NatP; apply: NS_pow; fprops; apply /NatP.
rewrite (infinite_power1_a x2 (finite_le_infinite xf fz) fz).
rewrite - (gch fz).
by move: (cnext_pr1 cz) => [_ _ ]; apply.
ex_middle neq.
move: (cpow_less_pr2 x (conj le1 neq)); set t := (x ^ le2.
move: (cleT (cpow_Mleeq t x2 card2_nz) le2) => le3.
case: (cleNgt le3(cantor (proj32 le3))).
Qed.
Lemma cpow_less_pr11b x: infinite_c x -> \2c ^ icx; apply: cpow_less_pr11a;fprops. Qed.
Lemma cpow_less_pr12 x: regular_cardinal x ->
x ^ /regular_cardinalP [ix cx]; move: (ix) => [cax _].
have aux: x ^c \1c = x by rewrite cpowx1.
have x1:=(infinite_gt1 ix).
apply: cleA; last by rewrite - {1} aux; apply cpow_less_pr2.
apply: (card_ub_sup cax) => i.
move /funI_P => [z] /(cardinals_ltP cax) zx ->.
case: (equal_or_not z \0c) => zz.
by rewrite zz cpowx0; move: x1 => [].
rewrite (infinite_power10_b); fprops; ue.
Qed.
Lemma inaccessible_weak_strong x:
inaccessible_w x -> inaccessible x.
Proof.
move => h; split => // t th.
move: h => [[pa pb] [n [on _ ln xv]]].
case: (finite_dichot (proj31_1 th)) => it.
apply:(finite_lt_infinite) => //.
apply /NatP; apply: NS_pow; apply /NatP;fprops.
move: th; rewrite - (gch it).
move: (ord_index_pr1 it) => [om <-]; rewrite (cnextE om) xv => le1.
move: (aleph_ltc_lt om on le1) => mn.
apply: aleph_lt_ltc; apply /oltP0; split;fprops.
apply: ln; apply /oltP => //.
Qed.
Lemma inaccessible_pr8_gch x: \2c
([\/ (x = omega0),
(exists2 n, ordinalp n & x = \aleph (osucc n)) | inaccessible x]
<-> x = x ^ x2.
set p:= (exists2 n, ordinalp n & x = \aleph (osucc n)).
have cx:=proj32_1 x2.
have xnz : x <> \0c.
move => xz; rewrite xz in x2; case: (clt0 x2).
have xp:=(clt_ltT clt_02 x2).
have aux: p -> x = x ^ [n on xv].
rewrite {3} xv; move: (cpow_less_pr4 xp (CIS_aleph on)).
rewrite (cnextE on); move => ->.
have i1:=(CIS_aleph on).
by rewrite xv - (cnextE on) (gch i1) - cpow_pow (csquare_inf).
split.
case =>//; first by move ->; symmetry; apply: cpow_less_pr5f.
by apply: inaccessible_pr8.
move => h.
case: (finite_dichot cx) => fx.
have xN: natp x by apply /NatP.
move: (cpred_pr xN xnz)=> [ub uv].
move: (cpow_less_pr3 xp ub); rewrite -uv -h.
move: (cltS ub); rewrite -uv => pa.
have xp1: \1c [].
move: (ord_index_pr1 fx) => [om xv]; symmetry in xv.
case: (ordinal_trichot om) => ln.
by constructor 1; rewrite - aleph0E - ln.
move: ln => [n on nv]; constructor 2; exists n => //.
by rewrite -nv.
constructor 3;apply: inaccessible_weak_strong.
split; last by exists (ord_index x).
split => //; ex_middle cs.
have cs1:=(cofinality_c_small (proj1 x2)).
move: (cpow_less_pr2 x (conj cs1 cs)); rewrite -h => lt1.
case: (cleNgt lt1(power_cofinality (proj1 x2))).
Qed.
Lemma infinite_power7h_rev x: \0c
(forall y, \0c
x ^c y = (csumb (cardinals_lt x) (fun z => z ^c y)) *c x)
-> regular_cardinal x.
Proof.
move => xp h.
move: (xp) => [_ /nesym xnz].
have cx:=proj32_1 xp.
case: (equal_or_not x \1c) => x1.
move: (h _ (clt_02)); rewrite x1 cpow1x; rewrite x1 in xp.
have ->: (cardinals_lt \1c) = singleton \0c.
apply : set1_pr; first by apply /(cardinals_ltP CS1).
by move => t /(cardinals_ltP CS1) /clt1.
rewrite csum_trivial3 (cpow0x card2_nz) (card_card CS0) cprod0l.
by move => /card1_nz.
case: (equal_or_not x \2c) => x2.
move: (h _ (clt_02)); rewrite x2; rewrite x2 in xp.
rewrite /csumb;set f := Lg _ _.
have aux: (cardinals_lt \2c) = doubleton \0c \1c.
set_extens t.
move => aux; apply /set2_P; apply: clt2.
by apply /(cardinals_ltP CS2).
case /set2_P => ->; apply /(cardinals_ltP CS2);
[apply: clt_02 | apply: clt_12].
have df: doubleton_fam f \0c \1c.
have pa: inc \1c (cardinals_lt \2c) by rewrite aux; fprops.
have pb: inc \0c (cardinals_lt \2c) by rewrite aux; fprops.
exists \0c; exists \1c; rewrite /f; bw;split; fprops.
rewrite cpow0x; fprops.
rewrite cpow1x; fprops.
rewrite - (csum2_pr df) (csum0l CS1) (cprod1l CS2) cpowx2 two_times_two.
move: (cltS NS2) (cltS NS3).
rewrite / card_four / card_three => lt1 lt2 eq3.
by move: (clt_leT lt1 (proj1 lt2)); rewrite eq3; move => [].
case: (Nat_dichot cx) => fx.
move: (h _ (clt_01)); rewrite /csumb; set f := Lg _ _.
have i2d: inc \2c (domain f).
rewrite /f; bw; apply /(cardinals_ltP cx); split; last by apply:nesym.
by apply: cge2.
have xx: inc \2c (cardinals_lt x) by move: i2d; rewrite /f; bw.
have cf: cardinal_fam f.
rewrite /f; hnf; bw => a ai; bw; fprops.
move: (csum_increasing6 cf i2d); rewrite {1}/f; bw.
rewrite (cpowx1 CS2) (cpowx1 cx) => pa pb.
move: (cprod_Mlele pa (cleR cx)); rewrite -pb two_times_n => qb.
by move: (csum_Mlteq fx xp);rewrite (csum0l cx) => /(cleNgt qb).
have H:= (cofinality_card fx).
split => //.
move: (cofinality_infinite fx); rewrite H => coi.
move: (h _ (finite_lt_infinite finite_0 coi)).
rewrite /csumb; set f := Lg _ _.
rewrite (infinite_power10_a fx) => pa.
ex_middle cnx.
have pc:= (cofinality_small fx).
have pb: forall i, inc i (domain f) -> Vg f i <=c x.
rewrite /f;bw;move=> i idf; bw.
move: idf => /(cardinals_ltP cx) => idf.
case: (equal_or_not i \0c) => i0.
rewrite i0 cpow0x; [ exact (proj1 xp) | by apply: infinite_nz ].
case: (equal_or_not i \1c) => i1.
by rewrite i1 cpow1x; apply (proj1 (infinite_gt1 fx)).
have y2:= (cge2 (proj31_1 idf) i0 i1).
have aux: forall z, infinite_c z -> z \2c ^c z <=c x.
move => z iz zx; rewrite - (gch iz).
by move: (cnext_pr1 (proj1 iz)) => [_ _]; apply.
case: (cleT_ee (proj31_1 idf) (proj31 pc)) => le1.
by rewrite (infinite_power1_a y2 le1 coi); apply: aux.
have iy:= (ge_infinite_infinite coi le1).
move: (cpow_Meqle i0 le1); rewrite (infinite_power1_b iy) => ce.
apply: (cleT ce (aux _ iy idf)).
have cff: fgraph f by rewrite /f; fprops.
move: (csum_of_small_b1 (conj cff pb)).
rewrite {2} /f; bw.
move: (infinite_power7d cx xnz) => [ca _].
move: (cprod_Mlele (cleR cx) ca); rewrite cprod2cr => cb cc.
move: (cleT cc cb); rewrite (csquare_inf fx) => cd.
move: (cprod_Mlele cd (cleR cx)); rewrite (csquare_inf fx) - pa.
by move: (cnext_pr1 cx) => [_ aa _ ]=> /(cltNge aa).
Qed.
Lemma infinite_increasing_power5gch X
(Y:= Lg (domain X) (fun z => \aleph (Vg X z)))
(a := \osup (range X)):
ofg_Mlt_lto X -> limit_ordinal (domain X) ->
((cprod Y) = \aleph a ^c (cardinal (domain X)) /\
(cprod Y) = \aleph (osucc a)).
Proof.
move => pa pb.
move: (infinite_increasing_power5 pa pb).
move: (increasing_sup_limit4 pa pb);rewrite -/Y -/a; move => [pc pd pe].
have ia:=(CIS_aleph (proj31 pc)).
rewrite -/a -/Y.
rewrite - (cnextE (proj31 pc)) - (gch ia).
move: (cnext_pr1 (proj1 ia)) => [_].
set A := \omega a; set B := A ^c cardinal (domain X).
move=> _ qa [qb qc qd].
have qe:= (qa _ qb).
have bv := (cleA qc (cleT qd qe)).
by split => //; apply:cleA => //; rewrite bv.
Qed.
Lemma cpow_less_ec_pr8 x y ( z := x ^ infinite_c x ->
[/\ (y <=c \cf x -> z = x),
(\cf x y <=c cnext x -> z = cnext x) &
(cnext x z = y)].
Proof.
move => icy icx; rewrite /z.
have cy:= proj1 icy.
have cx:= proj1 icx.
have sp1:=(cnext_pr2 cx).
have sp1' := proj1 sp1.
split.
move => pa; move: (cpow_less_pr5a cx (infinite_ge2 icy)) => le1.
apply: cleA; last by exact.
apply: (card_ub_sup cx) => i /funI_P [t ta ->]; move: ta.
move/ (cardinals_ltP cy) => ty.
move: (clt_leT ty pa) => lt2.
case: (equal_or_not t \0c) => tnz.
rewrite tnz cpowx0; apply: (finite_le_infinite finite_1 icx).
rewrite (infinite_power10_b icx lt2 tnz); fprops.
move => p1 p2; apply: cleA; last first.
by move: (cpow_less_pr2 x p1); rewrite (infinite_power10_a icx).
apply: (card_ub_sup (proj32 p2)) => i /funI_P [t ta ->]; move: ta.
move /(cardinals_ltP cy) => ty.
move: (infinite_power10 t icx) => [pa pb pc pd].
case: (equal_or_not t \0c) => tz.
rewrite (pa tz); apply: cleT p2.
apply: (finite_le_infinite finite_1 icy).
case: (cleT_el (proj31_1 p1) (proj31_1 ty)) => ctc.
rewrite (pc ctc (cnext_pr4 cx (clt_leT ty p2))); exact:(cleR (proj32 p2)).
by rewrite (pb tz ctc).
move => qa.
apply: cleA.
apply: (card_ub_sup cy).
move => i /funI_P [t ta ->]; move: ta.
move /(cardinals_ltP cy) => ty.
move: (infinite_power10 t icx) => [pa pb pc pd].
case: (equal_or_not t \0c) => tz.
by rewrite (pa tz); apply: (finite_le_infinite finite_1 icy).
move: (cofinality_small icx) => p1.
case: (cleT_el (proj31 p1) (proj31_1 ty)) => ctc.
case: (cleT_el (proj31_1 ty) cx) => ctx.
rewrite (pc ctc ctx); apply: (proj1 qa).
rewrite (pd ctx); move: (cnext_pr1 (proj32_1 ctx)).
by move => [_ _]; apply.
by rewrite (pb tz ctc); apply: (cleT sp1' (proj1 qa)).
move: (ord_index_pr1 icy); set c := (ord_index y); move => [qb qc].
move: (ord_index_pr1 icx); set d := (ord_index x); move => [qd qe].
move: (qa); rewrite - {1} qe -qc (cnextE qd) => qa1.
move: (aleph_ltc_lt (OS_succ qd) qb qa1) => qa2.
case: (ordinal_trichot qb) => ln.
rewrite ln in qa2;case: (olt0 qa2).
move:ln => [e oe se].
move: (cnextE oe); rewrite - se => <-.
move: (CIS_aleph oe) => icz.
rewrite (cpow_less_pr4 (finite_lt_infinite finite_0 icx) icz).
move: (infinite_power10 ( \omega e) icx) => [ra rb rc rd].
have xe: x i /funI_P [w wi ->].
have wc: w le1.
apply: cleT (cpow_less_pr2 x le1).
apply: (cleT (proj1 (cantor (proj31_1 le1)))).
apply: (cpow_Mleeq (\omega w) (infinite_ge2 icx) card2_nz).
Qed.
End GenContHypothesis_Props.
Definition beth x :=
let p := fun z => \2c ^c z in
let osup := fun y f => \osup (fun_image y (fun z => (p (f z)))) in
let osupp:= fun f => Yo (domain f = \0o) omega0 (osup (domain f) (Vg f)) in
let f:= transdef_ord osupp in
f x.
Lemma beth_prop:
[/\ normal_ofs beth, beth \0o = omega0 &
(forall x, ordinalp x -> beth (osucc x) = \2c ^c (beth x)) ].
Proof.
apply: normal_ofs_existence.
- move => x ox.
move: (CS_pow \2c x) => cp.
case: (oleT_el (proj1 cp) ox) => //.
move /ocle1; rewrite (card_card cp) => /cleNgt; case.
by move: (cantor (CS_cardinal x)); rewrite cpowcr.
- move => x y /ocle1 /(cpow_Meqle card2_nz).
rewrite cpowcr cpowcr; apply: ocle.
- apply: OS_omega.
Qed.
Lemma beth0: beth \0o = omega0.
Proof. by move: (beth_prop) => [_ pa _]. Qed.
Lemma beth_succ x: ordinalp x ->
beth (osucc x) = \2c ^c (beth x).
Proof. move: (beth_prop) => [_ _ ]; apply. Qed.
Lemma beth_normal: normal_ofs beth.
Proof. by move: (beth_prop) => [pa _ _ ]. Qed.
Lemma CS_beth x: ordinalp x -> cardinalp (beth x).
Proof.
move: (beth_prop) => [pa pb pc] ox.
case: (least_ordinal6 (fun z => cardinalp (beth z)) ox) => //.
set y := least_ordinal _ _;move=> [pd pe]; case.
case: (ordinal_trichot pd).
- move ->; rewrite pb; apply: CS_omega.
- move => [z oz za]; rewrite za pc; fprops.
- by move /(proj2 pa) => ->; apply: CS_sup => t /funI_P [z zy ->]; apply: pe.
Qed.
Lemma beth_M x y: x beth x pa ineq.
exact: (oclt3 (CS_beth (proj31_1 ineq))(CS_beth (proj32_1 ineq)) (pa _ _ ineq)).
Qed.
Lemma beth_pr1 x: ordinalp x -> infinite_c (beth x).
Proof.
move => ox; case: (ozero_dichot ox).
move => ->; rewrite beth0; apply CIS_omega.
by move /beth_M; rewrite beth0; move => [/infinite_c_P2 le1 _].
Qed.
Lemma beth_gch: GenContHypothesis <-> beth =1o \aleph.
Proof.
split; last first.
move => h x icx.
move: (ord_index_pr1 icx) => [oy <-].
by rewrite (cnextE oy) - (h _ oy) - (beth_succ oy) (h _ (OS_succ oy)).
move =>h x ox.
case:(least_ordinal6 (fun z => beth z = \aleph z) ox) => //.
set y := least_ordinal _ _; move =>[pa pb];case.
case: (ordinal_trichot pa).
- by move => ->; rewrite aleph0E beth0.
- move=> [u ou u1].
rewrite u1 (beth_succ ou) - (cnextE ou) (h _ (CIS_aleph ou)).
rewrite pb // u1; fprops.
move=> lt.
rewrite (proj2 beth_normal _ lt) (proj2 aleph_normal _ lt).
by apply: ord_sup_2funI => s st; apply: pb.
Qed.
Lemma beth_fixed_point x:
ordinalp x -> beth x = x -> card_dominant x.
Proof.
move => ox bfx.
have icx: infinite_c x by rewrite -bfx; apply: beth_pr1.
have xnz:= (infinite_nz icx).
have cx := proj1 icx.
apply: card_dominant_pr1 => // m mx.
have cm:= proj31_1 mx.
move: (infinite_card_limit2 icx) => lx; move: (lx) =>[qa qb qc].
have [b pa pb]: exists2 b, m <=c beth b & b i <=c m.
move => t /funI_P [i ix ->].
have oi:= ordinal_hi qa ix.
case: (cleT_ee (CS_beth oi) cm) => // h; case: bad; exists i => //.
by apply /oltP.
have : union (fun_image x beth) <=c m.
by apply: card_ub_sup.
by rewrite - ((proj2 beth_normal) _ lx) bfx => /(cltNge mx).
apply: (cle_ltT (cpow_Meqle card2_nz pa)).
have ob:= proj31_1 pb.
rewrite -(beth_succ ob) - bfx; apply: beth_M.
by move: pb => /(oltP ox) hh; apply / (oltP ox);apply: qc.
Qed.
Lemma cofinality_least_fp_beth x y:
beth x <> x -> least_fixedpoint_ge beth x y ->
cofinality y = omega0.
Proof. apply: (cofinality_least_fp_normal beth_normal). Qed.
Lemma aleph_and_beth a: ordinalp a ->
exists b, [/\ ordinalp b, beth b <=c \aleph a & \aleph a oa; case: (normal_ofs_bounded (OS_aleph oa) (beth_normal)).
by rewrite beth0 => /(oleNgt (aleph_pr5 oa)).
move => [y [oy ha hb]].
have hc:=(CS_aleph oa).
have hd:= (ocle3 (proj1 (beth_pr1 oy)) hc ha).
have he:= (oclt3 hc (proj1 (beth_pr1 (OS_succ oy))) hb).
by exists y.
Qed.
Lemma beth_limit a: limit_ordinal a ->
exists2 b, limit_ordinal b & beth a = \aleph b.
Proof.
move => la.
have oa := proj31 la.
move/limit_ordinal_P:la => [ap al].
move: (ord_index_pr1 (beth_pr1 oa)); set b := ord_index _; move => [ob bv].
case: (ordinal_trichot ob) =>lb.
- by case:(proj2 (beth_M ap)); move: bv; rewrite lb aleph0E - beth0.
- move:lb => [c oc cv].
move:bv; rewrite cv => ea.
move: (aleph_and_beth oc) => [d [od ha hb]].
move: (cle_ltT ha (aleph_lt_ltc (oltS oc))); rewrite ea => la.
case: (oleT_ell oa od) => lb.
by case: (proj2 la); rewrite lb.
by case : (cltNge la (proj1(beth_M lb))).
case: (cltNge (beth_M (al _ (al _ lb)))).
move: (cleT (aleph_pr12f oc) (cpow_M2le (proj1 hb))).
by rewrite ea - (beth_succ (OS_succ od)).
- by exists b.
Qed.
Lemma beth_inaccessible a k : inaccessible k ->
a beth a [ina inb] sb.
have oa:= (proj31_1 sb).
move: sb.
case: (least_ordinal6 (fun a => a beth a //.
set y:= least_ordinal _ _; move => [oy pb]; case => lyk.
case: (ordinal_trichot oy).
- by move ->; rewrite beth0; move: (inaccessible_uncountable ina).
- move => [x ox yv].
have xy: inc x y by rewrite yv; fprops.
have lxk: x ly; rewrite (proj2 beth_normal _ ly).
have ck:= (proj1 (proj1(proj1 ina))).
move/(ocle2P ck (proj31_1 lyk)): (lyk) => cyk.
have ha:=(cle_ltT (fun_image_smaller y beth) cyk).
apply: (regular_sup (proj1 ina) ha) => i /funI_P [z zy ->].
have lzy: z beth k = k.
Proof.
move => ik.
move: beth_normal => [sa sb].
have infk:= (proj1 (proj1 (proj1 ik))).
have ck := (proj1 infk); have ok := (proj1 ck).
apply: cleA.
rewrite (sb _ (infinite_card_limit2 infk)); apply:card_ub_sup => //.
move => i /funI_P [z /(oltP ok) zk ->].
exact: (proj1(beth_inaccessible ik zk)).
move:(ocle1 (osi_gex sa ok)).
by rewrite (card_card ck) (card_card (CS_beth ok)).
Qed.
Lemma card_dominant_pr12 x: infinite_c x ->
(forall m, infinite_c m -> m \2c ^c m