proposition: Lemma infinite_power7f a y: limit_ordinal a -> y <c \cf a -> (\aleph a) ^c y = \osup (fun_image a (fun z => (\aleph z) ^c y)).
proof: 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 <o a by apply /oltP. exact: cpow_Mleeq (aleph_le_lec zn1) (aleph_nz (proj31 zn1)). move: aux; set f := (Lg (cardinals_lt x) (cpow^~ y)) => aux. have cff: cardinal_fam f by rewrite /f; hnf; aw; move=> i ad; rewrite LgV//; fprops. have cx:= proj1 icx. have cdf1: cardinal (domain f) <=c x. rewrite /f Lgd; 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;aw; move=> [z zv -> ]. rewrite LgV//;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; aw; exists (\aleph z) => //; rewrite LgV//. move=> i /(range_gP fgf); rewrite /f; aw; move=> [u us]; rewrite LgV// => ->. move: us => /(cardinals_ltP cx) us. have cu:= proj31_1 us. case: (finite_or_infinite 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: cle0x; rewrite /cpow;fprops. apply: cpow_Mleeq=> //;apply: cle_fin_inf => //. 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: (cle_inf_inf 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.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)