Metamath Proof Explorer


Theorem nnnfi

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

Ref Expression
Assertion nnnfi ¬ ℕ ∈ Fin

Proof

Step Hyp Ref Expression
1 1z 1 ∈ ℤ
2 nnuz ℕ = ( ℤ ‘ 1 )
3 2 uzinf ( 1 ∈ ℤ → ¬ ℕ ∈ Fin )
4 1 3 ax-mp ¬ ℕ ∈ Fin