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

Metamath Proof Explorer

Theorem ominf

Description: The set of natural numbers is infinite. Corollary 6D(b) of Enderton p. 136. (Contributed by NM, 2-Jun-1998) Avoid ax-pow . (Revised by BTernaryTau, 2-Jan-2025)

Ref Expression
Assertion ominf 
|- -. _om e. Fin

Proof

Step Hyp Ref Expression
1 isfi 
 |-  ( _om e. Fin <-> E. x e. _om _om ~~ x )
2 nnord 
 |-  ( x e. _om -> Ord x )
3 ordom 
 |-  Ord _om
4 ordelssne 
 |-  ( ( Ord x /\ Ord _om ) -> ( x e. _om <-> ( x C_ _om /\ x =/= _om ) ) )
5 2 3 4 sylancl 
 |-  ( x e. _om -> ( x e. _om <-> ( x C_ _om /\ x =/= _om ) ) )
6 5 ibi 
 |-  ( x e. _om -> ( x C_ _om /\ x =/= _om ) )
7 df-pss 
 |-  ( x C. _om <-> ( x C_ _om /\ x =/= _om ) )
8 6 7 sylibr 
 |-  ( x e. _om -> x C. _om )
9 nnfi 
 |-  ( x e. _om -> x e. Fin )
10 ensymfib 
 |-  ( x e. Fin -> ( x ~~ _om <-> _om ~~ x ) )
11 9 10 syl 
 |-  ( x e. _om -> ( x ~~ _om <-> _om ~~ x ) )
12 11 biimpar 
 |-  ( ( x e. _om /\ _om ~~ x ) -> x ~~ _om )
13 pssinf 
 |-  ( ( x C. _om /\ x ~~ _om ) -> -. _om e. Fin )
14 8 12 13 syl2an2r 
 |-  ( ( x e. _om /\ _om ~~ x ) -> -. _om e. Fin )
15 14 rexlimiva 
 |-  ( E. x e. _om _om ~~ x -> -. _om e. Fin )
16 1 15 sylbi 
 |-  ( _om e. Fin -> -. _om e. Fin )
17 pm2.01 
 |-  ( ( _om e. Fin -> -. _om e. Fin ) -> -. _om e. Fin )
18 16 17 ax-mp 
 |-  -. _om e. Fin