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