This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐴 ↔ ( 𝐴 ∈ 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 ) )