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	⊢ ..^ : ( ℤ × ℤ ) ⟶ 𝒫 ℤ