Proof
01. 1 ⊢ β ∈ On, hypo.
02. 2 ⊢ α ∈ β, hypo.
03. 1 ⊢ β ∈ Univ ∩ {α | transitive α ∧ ∀x. x ∈ α → transitive x},
eq_subst On_eq 1.
04. 1 ⊢ β ∈ Univ, intersection_eliml 3.
05. 1 ⊢ β ∈ {α | transitive α ∧ ∀x. x ∈ α → transitive x},
intersection_elimr 3.
06. 1 ⊢ transitive β ∧ ∀x. x ∈ β → transitive x, comp_elim 5.
07. 1 ⊢ transitive β, conj_eliml 6.
08. 1 ⊢ ∀x. x ∈ β → transitive x, conj_elimr 6.
09. 1, 2 ⊢ transitive α, uq_bounded_elim 8 2.
10. 10 ⊢ x ∈ α, hypo.
11. 1, 2 ⊢ α ⊆ β, transitive_elim 7 2.
12. 1, 2, 10 ⊢ x ∈ β, incl_elim 11 10.
13. 1, 2, 10 ⊢ transitive x, uq_bounded_elim 8 12.
14. 1, 2 ⊢ x ∈ α → transitive x, subj_intro 13.
15. 1, 2 ⊢ ∀x. x ∈ α → transitive x, uq_intro 14.
16. 1, 2 ⊢ transitive α ∧ ∀x. x ∈ α → transitive x, conj_intro 9 15.
17. 2 ⊢ set α, set_intro 2.
18. 1, 2 ⊢ α ∈ {α | transitive α ∧ ∀x. x ∈ α → transitive x},
comp_intro 17 16.
19. 1 ⊢ β ⊆ Univ, univ_trans Univ_is_univ 4.
20. 1, 2 ⊢ α ∈ Univ, incl_elim 19 2.
21. 1, 2 ⊢ α ∈ Univ ∩ {α | transitive α ∧ ∀x. x ∈ α → transitive x},
intersection_intro 20 18.
22. 1, 2 ⊢ α ∈ On, eq_subst_rev On_eq 21, P t ↔ α ∈ t.
23. 1 ⊢ α ∈ β → α ∈ On, subj_intro 22.
24. 1 ⊢ ∀α. α ∈ β → α ∈ On, uq_intro 23.
25. 1 ⊢ β ⊆ On, incl_intro 24.
On_is_transitive. ⊢ β ∈ On → β ⊆ On, subj_intro 25.
Dependencies
The given proof depends on 11 axioms:
comp, efq, eq_refl, eq_subst, ext, infinity, lem, power, subset, union, universes.