proposition: 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: 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; aw. 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;aw; set_extens t. move /setUb_P => [z za];rewrite /h LgV ; [by move => /Zo_P [] | ue]. move => tx; apply /setUb_P. have ot:= (Os_ordinal 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 LgV//; apply: Zo_i]. rewrite /csumb;set u := csum _. move: (csum_An ph). have -> : u = csum f. rewrite /u /f; apply: f_equal; rewrite /g; aw; apply: Lg_exten=> t tx. by rewrite LgV// cpow_pr1 (card_card cy). move ->. rewrite -dh. have fgfxx: fgraph (Lg (domain h) (cpow^~ y)) by fprops. rewrite cprodC (cprod2Dn); aw. apply: csum_increasing;aw; trivial. move=> z zd; rewrite LgV//. 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; aw. have pb: domain (restr f (Vg h z)) = Vg h z by aw. have ->: (csumb (Vg h z) (Vg f)) = csumb (Vg h z) (fun t => z ^c y). rewrite/f;apply: csumb_exten => t td; move: (pd _ td) => tx; rewrite LgV//. move: td; rewrite /h LgV; [ move /Zo_P; move => [_ -> //] | ue]. rewrite csum_of_same cprodC - cprod2cl LgV//. apply cprod_Mlele. by move: (sub_smaller pd); rewrite (card_card cx). apply: cleR; rewrite /cpow;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)