Proof 01. ⊢ set (least_univ onat) ∧ univ (least_univ onat), least_univ_is_univ onat_is_set. 02. ⊢ set (least_univ onat), conj_eliml 1. Univ_is_set. ⊢ set Univ, eq_subst_rev Univ_eq 2, P t ↔ set t.
Dependencies
The given proof depends on 11 axioms:
comp, efq, eq_refl, eq_subst, ext, infinity, lem, power, subset, union, universes.