Metamath Proof Explorer

Theorem ordfin

Description: A generalization of onfin to include the class of all ordinals. (Contributed by Scott Fenton, 19-Feb-2026)

Ref Expression
Assertion ordfin 
|- ( Ord A -> ( A e. Fin <-> A e. _om ) )

Proof

Step Hyp Ref Expression
1 ordeleqon 
 |-  ( Ord A <-> ( A e. On \/ A = On ) )
2 onfin 
 |-  ( A e. On -> ( A e. Fin <-> A e. _om ) )
3 onprc 
 |-  -. On e. _V
4 elex 
 |-  ( On e. Fin -> On e. _V )
5 3 4 mto 
 |-  -. On e. Fin
6 eleq1 
 |-  ( A = On -> ( A e. Fin <-> On e. Fin ) )
7 5 6 mtbiri 
 |-  ( A = On -> -. A e. Fin )
8 elex 
 |-  ( On e. _om -> On e. _V )
9 3 8 mto 
 |-  -. On e. _om
10 eleq1 
 |-  ( A = On -> ( A e. _om <-> On e. _om ) )
11 9 10 mtbiri 
 |-  ( A = On -> -. A e. _om )
12 7 11 2falsed 
 |-  ( A = On -> ( A e. Fin <-> A e. _om ) )
13 2 12 jaoi 
 |-  ( ( A e. On \/ A = On ) -> ( A e. Fin <-> A e. _om ) )
14 1 13 sylbi 
 |-  ( Ord A -> ( A e. Fin <-> A e. _om ) )