Theorem uzinf

Description: An upper integer set is infinite. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypothesis	uzinf.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion	uzinf	⊢ ( 𝑀 ∈ ℤ → ¬ 𝑍 ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		uzinf.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		ominf	⊢ ¬ ω ∈ Fin
3	1	uzenom	⊢ ( 𝑀 ∈ ℤ → 𝑍 ≈ ω )
4		enfi	⊢ ( 𝑍 ≈ ω → ( 𝑍 ∈ Fin ↔ ω ∈ Fin ) )
5	3 4	syl	⊢ ( 𝑀 ∈ ℤ → ( 𝑍 ∈ Fin ↔ ω ∈ Fin ) )
6	2 5	mtbiri	⊢ ( 𝑀 ∈ ℤ → ¬ 𝑍 ∈ Fin )