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