proposition: Lemma card_universe_omega: cardinal (universe omega0) = aleph0.
proof: Proof. apply: cleA; last first. by move: (sub_smaller (ordinal_in_universe OS_omega)); rewrite cardinal_Nat. rewrite (universe_limit omega_limit). set f := (Lg omega0 universe). have ->: (unionf omega0 universe) = unionb f. rewrite /f /unionb; aw; apply:setUf_exten => h hi /=; rewrite LgV//. have ha: countable_set (domain f) by rewrite Lgd; apply: countable_Nat. have hb: allf f countable_set. rewrite /f;hnf; aw => i io; rewrite LgV//; apply:finite_is_countable. exact:(card_universe_fin io). by move: (countable_union ha hb) => /countableP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)