proposition: Lemma infinite_power7e a y: limit_ordinal a -> y <> \0c -> \aleph a <=c \osup (fun_image a (fun z => (\aleph z) ^c y)).
proof: Proof. move=> ln ynz. move: aleph_normal => [qa qb]; rewrite (qb _ ln). set T2:= fun_image _ _. set T := fun_image _ _. have csr: cardinal_set T by move=> t /funI_P [z zn ->]; fprops. apply:card_ub_sup; first by apply: (CS_sup csr). move => // i /funI_P [z zn ->]. have sr1: inc ((\aleph z) ^c y) T by apply /funI_P; ex_tac. apply: cleT (card_sup_ub csr sr1). have oz:= (Os_ordinal (proj31 ln) zn). exact:(cpow_Mle1 (CS_aleph oz) ynz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)