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 A <-> ( A e. On \/ A = On ) )

Proof

Step Hyp Ref Expression
1 onprc 
 |-  -. On e. _V
2 elex 
 |-  ( On e. A -> On e. _V )
3 1 2 mto 
 |-  -. On e. A
4 ordon 
 |-  Ord On
5 ordtri3or 
 |-  ( ( Ord A /\ Ord On ) -> ( A e. On \/ A = On \/ On e. A ) )
6 4 5 mpan2 
 |-  ( Ord A -> ( A e. On \/ A = On \/ On e. A ) )
7 df-3or 
 |-  ( ( A e. On \/ A = On \/ On e. A ) <-> ( ( A e. On \/ A = On ) \/ On e. A ) )
8 6 7 sylib 
 |-  ( Ord A -> ( ( A e. On \/ A = On ) \/ On e. A ) )
9 8 ord 
 |-  ( Ord A -> ( -. ( A e. On \/ A = On ) -> On e. A ) )
10 3 9 mt3i 
 |-  ( Ord A -> ( A e. On \/ A = On ) )
11 eloni 
 |-  ( A e. On -> Ord A )
12 ordeq 
 |-  ( A = On -> ( Ord A <-> Ord On ) )
13 4 12 mpbiri 
 |-  ( A = On -> Ord A )
14 11 13 jaoi 
 |-  ( ( A e. On \/ A = On ) -> Ord A )
15 10 14 impbii 
 |-  ( Ord A <-> ( A e. On \/ A = On ) )