Theorem fzf

Description: Establish the domain and codomain of the finite integer sequence function. (Contributed by Scott Fenton, 8-Aug-2013) (Revised by Mario Carneiro, 16-Nov-2013)

	Ref	Expression
Assertion	fzf	⊢ ... : ( ℤ × ℤ ) ⟶ 𝒫 ℤ

Proof

Step	Hyp	Ref	Expression
1		zex	⊢ ℤ ∈ V
2		ssrab2	⊢ { 𝑘 ∈ ℤ ∣ ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) } ⊆ ℤ
3	1 2	elpwi2	⊢ { 𝑘 ∈ ℤ ∣ ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) } ∈ 𝒫 ℤ
4	3	rgen2w	⊢ ∀ 𝑚 ∈ ℤ ∀ 𝑛 ∈ ℤ { 𝑘 ∈ ℤ ∣ ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) } ∈ 𝒫 ℤ
5		df-fz	⊢ ... = ( 𝑚 ∈ ℤ , 𝑛 ∈ ℤ ↦ { 𝑘 ∈ ℤ ∣ ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) } )
6	5	fmpo	⊢ ( ∀ 𝑚 ∈ ℤ ∀ 𝑛 ∈ ℤ { 𝑘 ∈ ℤ ∣ ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) } ∈ 𝒫 ℤ ↔ ... : ( ℤ × ℤ ) ⟶ 𝒫 ℤ )
7	4 6	mpbi	⊢ ... : ( ℤ × ℤ ) ⟶ 𝒫 ℤ