proposition: Lemma universe_inaccessible_card1 b: b <o a -> cardinal(universe b) <c a.
proof: Proof. pose p b := b<o a -> cardinal (universe b) <c a. move: (ia) => [[ [ica _] _] _]. move => ba;ex_middle bad. apply:(least_ordinal2 (p:=p)) (proj31_1 ba) ba => y oy etc yb. move /(ocle2P (proj1 ica) oy) : (yb) => cya. rewrite /p (universe_rec oy). set yy := unionf _ _. have ->: yy = unionb (Lg y (fun z => \Po (universe z))). set_extens t. move /setUf_P => [s sa sb]; apply /setUb_P; aw; ex_tac; rewrite LgV//. move => /setUb_P; aw; move => [s sa]; rewrite LgV// => sb; apply /setUf_P; ex_tac. move: (csum_pr1 (Lg y (fun z => \Po (universe z)))). set s := csumb _ _; move => h; apply: (cle_ltT h); clear h. set f := Lg y (fun z => cardinal(\Po (universe z))). have pra: csum f = s. rewrite /s /f; aw;apply: csumb_exten; move => t ty /=; rewrite LgV//. have prb: domain f = y by rewrite /f;aw. have prc: cardinal_fam f by move => t; rewrite prb /f => ys; rewrite LgV//; fprops. have prd: fgraph f by rewrite /f; fprops. move /(infinite_regularP ica) : (proj1 (proj1 ia)) => h. apply: h; last by aw. split;fprops; hnf; aw => x xy; rewrite !LgV//; rewrite card_setP. move: (xy) => /(oltP oy) iy';rewrite - cpowcr. exact: ((proj2 ia) _ (etc _ iy' (ole_ltT (proj1 iy') yb))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)