proposition: Lemma inaccessible_pr2 x: inaccessible_w x -> cardinal (Zo x regular_cardinal) = x.
proof: Proof. move=> ix; move: ix (inaccessible_pr1 ix) => [rx [n ln xv]] xx. have cx: cardinalp x by apply: (proj1 (proj1 rx)). rewrite - {2} (card_card cx). apply: cleA; first by apply: sub_smaller; apply Zo_S. set S := (Zo x regular_cardinal). have ox:= proj1 cx. have lx: limit_ordinal x. suff : x = n by move => ->. apply:aleph_inj => //; [ by move: ln => [] | by ue]. have oo:= OS_aleph ox. have pa: forall i, inc i x -> inc (\aleph (osucc i)) S. move=> i ix; apply: Zo_i. rewrite xx; apply /(oltP oo); apply: aleph_lt_lto. by apply/(oltP ox); move: lx => [_ _ ]; apply. apply: regular_initial_successor; apply: (Os_ordinal ox ix). set f := Lf (fun z => (\aleph (osucc z))) x S. have inf: injection f. apply: lf_injective => // u v ux vx sv. have ou:= (Os_ordinal ox ux). have ov :=(Os_ordinal ox vx). apply: osucc_inj => //; apply: aleph_inj; fprops. have ->: x = source f by rewrite /f; aw. have ->: S = target f by rewrite /f; aw. by apply: inj_source_smaller. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)