Metamath Proof Explorer

Theorem fzofi

Description: Half-open integer sets are finite. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion fzofi ⊢ M ..^ N ∈ Fin

Proof

Step Hyp Ref Expression
1 fzoval ⊢ N ∈ ℤ → M ..^ N = M … N − 1
2 1 adantl ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ..^ N = M … N − 1
3 fzfi ⊢ M … N − 1 ∈ Fin
4 2 3 eqeltrdi ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ..^ N ∈ Fin
5 fzof ⊢ ..^ : ℤ × ℤ ⟶ 𝒫 ℤ
6 5 fdmi ⊢ dom ⁡ ..^ = ℤ × ℤ
7 6 ndmov ⊢ ¬ M ∈ ℤ ∧ N ∈ ℤ → M ..^ N = ∅
8 0fin ⊢ ∅ ∈ Fin
9 7 8 eqeltrdi ⊢ ¬ M ∈ ℤ ∧ N ∈ ℤ → M ..^ N ∈ Fin
10 4 9 pm2.61i ⊢ M ..^ N ∈ Fin