Metamath Proof Explorer

Theorem unben

Description: An unbounded set of positive integers is infinite. (Contributed by NM, 5-May-2005) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Assertion unben 
|- ( ( A C_ NN /\ A. m e. NN E. n e. A m < n ) -> A ~~ NN )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` _om )
2 1 unbenlem 
 |-  ( ( A C_ NN /\ A. m e. NN E. n e. A m < n ) -> A ~~ _om )
3 nnenom 
 |-  NN ~~ _om
4 3 ensymi 
 |-  _om ~~ NN
5 entr 
 |-  ( ( A ~~ _om /\ _om ~~ NN ) -> A ~~ NN )
6 2 4 5 sylancl 
 |-  ( ( A C_ NN /\ A. m e. NN E. n e. A m < n ) -> A ~~ NN )