Metamath Proof Explorer

Theorem nnnfi

Description: The set of positive integers is infinite. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Assertion nnnfi 
|- -. NN e. Fin

Proof

Step Hyp Ref Expression
1 1z 
 |-  1 e. ZZ
2 nnuz 
 |-  NN = ( ZZ>= ` 1 )
3 2 uzinf 
 |-  ( 1 e. ZZ -> -. NN e. Fin )
4 1 3 ax-mp 
 |-  -. NN e. Fin