Theorem tron

Description: The class of all ordinal numbers is transitive. (Contributed by NM, 4-May-2009)

	Ref	Expression
Assertion	tron	⊢ Tr On

Proof

Step	Hyp	Ref	Expression
1		dftr3	⊢ ( Tr On ↔ ∀ 𝑥 ∈ On 𝑥 ⊆ On )
2		vex	⊢ 𝑥 ∈ V
3	2	elon	⊢ ( 𝑥 ∈ On ↔ Ord 𝑥 )
4		ordelord	⊢ ( ( Ord 𝑥 ∧ 𝑦 ∈ 𝑥 ) → Ord 𝑦 )
5	3 4	sylanb	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → Ord 𝑦 )
6	5	ex	⊢ ( 𝑥 ∈ On → ( 𝑦 ∈ 𝑥 → Ord 𝑦 ) )
7		vex	⊢ 𝑦 ∈ V
8	7	elon	⊢ ( 𝑦 ∈ On ↔ Ord 𝑦 )
9	6 8	imbitrrdi	⊢ ( 𝑥 ∈ On → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ On ) )
10	9	ssrdv	⊢ ( 𝑥 ∈ On → 𝑥 ⊆ On )
11	1 10	mprgbir	⊢ Tr On