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)

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 ensym 
 |-  ( _om ~~ x -> x ~~ _om )
10 pssinf 
 |-  ( ( x C. _om /\ x ~~ _om ) -> -. _om e. Fin )
11 8 9 10 syl2an 
 |-  ( ( x e. _om /\ _om ~~ x ) -> -. _om e. Fin )
12 11 rexlimiva 
 |-  ( E. x e. _om _om ~~ x -> -. _om e. Fin )
13 1 12 sylbi 
 |-  ( _om e. Fin -> -. _om e. Fin )
14 pm2.01 
 |-  ( ( _om e. Fin -> -. _om e. Fin ) -> -. _om e. Fin )
15 13 14 ax-mp 
 |-  -. _om e. Fin