This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )