proposition: Lemma universe_inaccessible_inc x: inc x (universe a) <-> (sub x (universe a) /\ cardinal x <c a).
proof: Proof. move: (ia) => [[ [ica _] _] _]. move:(infinite_card_limit2 ica) => loa. move:(proj31 loa) => oa. split. move => xua; split;first by apply: universe_trans. move: xua; rewrite (universe_limit loa) => /setUf_P [y ya yu]. move: (universe_trans (Os_ordinal oa ya) yu) => /sub_smaller. move /(oltP oa) : ya => /universe_inaccessible_card1. move => pa pb; apply: (cle_ltT pb pa). move => [xu cx]. set f := Lg x (fun z => cardinal (urank a z)). set s := csum f. have pra: csum f = s by []. have prb: domain f = x 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. have pre: forall i : Set, inc i (domain f) -> Vg f i <c a. move => i; rewrite prb /f => tx; rewrite LgV//. move: (xu _ tx); rewrite (universe_limit loa) => /setUf_P [y ya yb]. move: (urank_pr1 oa (xu _ tx)) => [pa1 pa2]. move: (urank_pr1 (Os_ordinal oa ya) yb) => [pb1 pb2]. apply /(ocle2P (proj1 ica) (proj31_1 pa1)). rewrite (urank_uniq pa2 pb2); apply: (ole_ltT (proj1 pb1)). by apply /(oltP oa). move /(infinite_regularP ica) : (proj1 (proj1 ia)) => h. have ww: cardinal (domain f) <c a by ue. move: (h _ (conj prd pre) ww) => lsa. move: (proj2 ia _ lsa); set s1 := \2c ^c s => lsb. move: (oclt lsb) => /universe_inc1; apply; apply /setP_P. move => i ix; move: (ix); rewrite - prb => ix'. move: (urank_pr1 oa (xu _ ix)) => [_ [hb /setP_P hc _]]. move: (csum_increasing6 (prc _ ix') ix'); rewrite pra /f LgV// => le2. move: (cle_ltT le2 (cantor (proj31_1 lsa))). by move /(ocle2P (CS_pow \2c s) hb) => /universe_inc1; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)