Metamath Proof Explorer

Theorem fzof

Description: Functionality of the half-open integer set function. (Contributed by Stefan O'Rear, 14-Aug-2015)

Ref Expression
Assertion fzof ⊢ ..^ : ℤ × ℤ ⟶ 𝒫 ℤ

Proof

Step Hyp Ref Expression
1 fzssz ⊢ m … n − 1 ⊆ ℤ
2 ovex ⊢ m … n − 1 ∈ V
3 2 elpw ⊢ m … n − 1 ∈ 𝒫 ℤ ↔ m … n − 1 ⊆ ℤ
4 1 3 mpbir ⊢ m … n − 1 ∈ 𝒫 ℤ
5 4 rgen2w ⊢ ∀ m ∈ ℤ ∀ n ∈ ℤ m … n − 1 ∈ 𝒫 ℤ
6 df-fzo ⊢ ..^ = m ∈ ℤ , n ∈ ℤ ⟼ m … n − 1
7 6 fmpo ⊢ ∀ m ∈ ℤ ∀ n ∈ ℤ m … n − 1 ∈ 𝒫 ℤ ↔ ..^ : ℤ × ℤ ⟶ 𝒫 ℤ
8 5 7 mpbi ⊢ ..^ : ℤ × ℤ ⟶ 𝒫 ℤ