Metamath Proof Explorer

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 ⁡ A ↔ A ∈ On ∨ A = On

Proof

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