proposition: Lemma card_dominant_pr7 a (A := \aleph a) B (s := \osup (fun_image a (fun z=> \aleph z ^c B))): rel_strong_card A B -> B <> \0c -> ordinalp a -> (s <=c A /\ (limit_ordinal a -> s = A)).
proof: Proof. move => sab bnz oa. have cA:= (CS_aleph oa). move: (CIS_aleph oa); rewrite -/A => iA. have pa: s <=c A. apply: card_ub_sup => // i /funI_P [z za ->]. have lt1: \omega z <c A. by apply: aleph_lt_ltc; move: za => /oltP []. exact: (proj1 (sab _ lt1)). split => // la. set g := (fun z => \omega z ^c B). set f := (fun z => \omega z). have pb: (forall x, inc x a -> f x <=c g x). move => x xa; rewrite /f/g. have ox:= Os_ordinal oa xa. apply: (cpow_Mle1 (CS_aleph ox) bnz). apply: cleA; first by exact. apply: cleT (card_sup_image pb). move: aleph_normal => [_ h]; move: (h _ la). have ->: (fun_image a \omega) = (fun_image a f) by set_extens t; aw. move => <-; apply: cleR; apply: (CS_aleph oa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)