proposition: 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: 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:= (cle_inf_inf 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 cle0x | 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 cle0x. 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 cprodb (domain f) (fun i => \osup T). apply: cprod_increasing; aw; trivial => t tdf; rewrite !LgV//. apply: card_sup_ub => //; apply /funI_P; exists (Vg f t) => //. by apply /(cardinals_ltP (proj1 icx)); apply: pd. by rewrite cprod_of_same pe H; apply:cleT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)