Theorem ordeleqon

Description: A way to express the ordinal property of a class in terms of the class of ordinal numbers. Corollary 7.14 of TakeutiZaring p. 38 and its converse. (Contributed by NM, 1-Jun-2003)

	Ref	Expression
Assertion	ordeleqon	⊢ ( Ord 𝐴 ↔ ( 𝐴 ∈ On ∨ 𝐴 = On ) )

Proof

Step	Hyp	Ref	Expression
1		onprc	⊢ ¬ On ∈ V
2		elex	⊢ ( On ∈ 𝐴 → On ∈ V )
3	1 2	mto	⊢ ¬ On ∈ 𝐴
4		ordon	⊢ Ord On
5		ordtri3or	⊢ ( ( Ord 𝐴 ∧ Ord On ) → ( 𝐴 ∈ On ∨ 𝐴 = On ∨ On ∈ 𝐴 ) )
6	4 5	mpan2	⊢ ( Ord 𝐴 → ( 𝐴 ∈ On ∨ 𝐴 = On ∨ On ∈ 𝐴 ) )
7		df-3or	⊢ ( ( 𝐴 ∈ On ∨ 𝐴 = On ∨ On ∈ 𝐴 ) ↔ ( ( 𝐴 ∈ On ∨ 𝐴 = On ) ∨ On ∈ 𝐴 ) )
8	6 7	sylib	⊢ ( Ord 𝐴 → ( ( 𝐴 ∈ On ∨ 𝐴 = On ) ∨ On ∈ 𝐴 ) )
9	8	ord	⊢ ( Ord 𝐴 → ( ¬ ( 𝐴 ∈ On ∨ 𝐴 = On ) → On ∈ 𝐴 ) )
10	3 9	mt3i	⊢ ( Ord 𝐴 → ( 𝐴 ∈ On ∨ 𝐴 = On ) )
11		eloni	⊢ ( 𝐴 ∈ On → Ord 𝐴 )
12		ordeq	⊢ ( 𝐴 = On → ( Ord 𝐴 ↔ Ord On ) )
13	4 12	mpbiri	⊢ ( 𝐴 = On → Ord 𝐴 )
14	11 13	jaoi	⊢ ( ( 𝐴 ∈ On ∨ 𝐴 = On ) → Ord 𝐴 )
15	10 14	impbii	⊢ ( Ord 𝐴 ↔ ( 𝐴 ∈ On ∨ 𝐴 = On ) )