Metamath Proof Explorer

Theorem infordmin

Description: _om is the smallest infinite ordinal. (Contributed by RP, 27-Sep-2023)

Ref Expression
Assertion infordmin 
|- A. x e. ( On \ Fin ) _om C_ x

Proof

Step Hyp Ref Expression
1 eldif 
 |-  ( x e. ( On \ Fin ) <-> ( x e. On /\ -. x e. Fin ) )
2 omelon 
 |-  _om e. On
3 ontri1 
 |-  ( ( _om e. On /\ x e. On ) -> ( _om C_ x <-> -. x e. _om ) )
4 3 bicomd 
 |-  ( ( _om e. On /\ x e. On ) -> ( -. x e. _om <-> _om C_ x ) )
5 4 con1bid 
 |-  ( ( _om e. On /\ x e. On ) -> ( -. _om C_ x <-> x e. _om ) )
6 nnfi 
 |-  ( x e. _om -> x e. Fin )
7 5 6 syl6bi 
 |-  ( ( _om e. On /\ x e. On ) -> ( -. _om C_ x -> x e. Fin ) )
8 2 7 mpan 
 |-  ( x e. On -> ( -. _om C_ x -> x e. Fin ) )
9 8 con1d 
 |-  ( x e. On -> ( -. x e. Fin -> _om C_ x ) )
10 9 imp 
 |-  ( ( x e. On /\ -. x e. Fin ) -> _om C_ x )
11 1 10 sylbi 
 |-  ( x e. ( On \ Fin ) -> _om C_ x )
12 11 rgen 
 |-  A. x e. ( On \ Fin ) _om C_ x