proposition: Lemma infinite_prod6 a: ordinalp a -> a <> \0o -> cprodb (osucc a) \aleph = (\aleph a) ^c (cardinal a).
proof: 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; aw. have f0: Vg f \0o = \omega y. rewrite /f LgV; [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_limA 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: (cle_inf_inf (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; aw. have f0: Vg f \0o = \omega \0o. by rewrite /f LgV//; 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: ole_01. by rewrite (cprod_inf p1 (CIS_aleph OS1) (aleph_nz OS0)) (cpowx1 (proj32 p1)). have lt1: z <o y by rewrite zv; apply: oltS. rewrite zv in cny. rewrite zv (lyp _ lt1 znz) (infinite_power2 oz cny); apply: f_equal2;last exact. case: (p_or_not_p (infinite_o 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: (cle_inf_inf (CIS_aleph oz) p1) => p2. apply: (cprod_inf) => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)