proposition: Lemma infinite_power7b x y: infinite_c x -> y <c \cf x -> x ^c y <=c cardinal (unionb (Lg x (functions y))).
proof: Proof. move=> icx yc. have cx:= proj1 icx. have ox:= OS_cardinal cx. have Ha f: (function_prop f y x) -> ordinal_set (Imf f). move => [ff sf tf] t /(Imf_P ff) [u usf ->]. by apply: (Os_ordinal ox); rewrite - tf;Wtac. have ha:(forall f, function_prop f y x -> inc (\osup (Imf f)) x). move => f fp; move: (fp) => [ff sf tf]. move:(Ha _ fp);set T := (Imf f) => osT. 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 => /(Imf_P 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 <o \osup T by apply /(oltP ou); ue. move: (olt_sup osT ls) => [z /(Imf_P ff) [u usf ->] [tw _]]. rewrite - sf; ex_tac. have oy:= (proj1 (proj31_1 yc)). case: (oleNgt ((proj33 (cofinality_rw ox)) _ 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) <o x. have qc:= (proj33 (infinite_card_limit2 icx)). 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 fpp t tsf. have osT := (Ha f fpp). apply /oleP; first by apply: OS_sup. apply: ord_sup_ub => //; apply /(Imf_P (proj31 fpp)); 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 /(Imf_P 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; aw; exists (sf1 f) => //; rewrite LgV//. set g := Lf R (functions y x) t1. suff ig: injection g by move: (inj_source_smaller 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.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)