Description: Functionality of the half-open integer set function. (Contributed by Stefan O'Rear, 14-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | fzof | ⊢ ..^ : ( ℤ × ℤ ) ⟶ 𝒫 ℤ |
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 | ⊢ ..^ : ( ℤ × ℤ ) ⟶ 𝒫 ℤ |