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 ( 𝑚 ... ( 𝑛 − 1 ) ) ⊆ ℤ
2 ovex ( 𝑚 ... ( 𝑛 − 1 ) ) ∈ V
3 2 elpw ( ( 𝑚 ... ( 𝑛 − 1 ) ) ∈ 𝒫 ℤ ↔ ( 𝑚 ... ( 𝑛 − 1 ) ) ⊆ ℤ )
4 1 3 mpbir ( 𝑚 ... ( 𝑛 − 1 ) ) ∈ 𝒫 ℤ
5 4 rgen2w 𝑚 ∈ ℤ ∀ 𝑛 ∈ ℤ ( 𝑚 ... ( 𝑛 − 1 ) ) ∈ 𝒫 ℤ
6 df-fzo ..^ = ( 𝑚 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( 𝑚 ... ( 𝑛 − 1 ) ) )
7 6 fmpo ( ∀ 𝑚 ∈ ℤ ∀ 𝑛 ∈ ℤ ( 𝑚 ... ( 𝑛 − 1 ) ) ∈ 𝒫 ℤ ↔ ..^ : ( ℤ × ℤ ) ⟶ 𝒫 ℤ )
8 5 7 mpbi ..^ : ( ℤ × ℤ ) ⟶ 𝒫 ℤ