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	$$⊢\dots :\mathbb{Z}\times \mathbb{Z}⟶𝒫\mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		zex	$$⊢\mathbb{Z}\in \mathrm{V}$$
2		ssrab2	$$⊢\left\{k\in \mathbb{Z}|\left(m\le k\wedge k\le n\right)\right\}\subseteq \mathbb{Z}$$
3	1 2	elpwi2	$$⊢\left\{k\in \mathbb{Z}|\left(m\le k\wedge k\le n\right)\right\}\in 𝒫\mathbb{Z}$$
4	3	rgen2w	$$⊢\forall m\in \mathbb{Z}\forall n\in \mathbb{Z}\left\{k\in \mathbb{Z}|\left(m\le k\wedge k\le n\right)\right\}\in 𝒫\mathbb{Z}$$
5		df-fz	$$⊢\dots =\left(m\in \mathbb{Z},n\in \mathbb{Z}⟼\left\{k\in \mathbb{Z}|\left(m\le k\wedge k\le n\right)\right\}\right)$$
6	5	fmpo	$$⊢\forall m\in \mathbb{Z}\forall n\in \mathbb{Z}\left\{k\in \mathbb{Z}|\left(m\le k\wedge k\le n\right)\right\}\in 𝒫\mathbb{Z}\leftrightarrow \dots :\mathbb{Z}\times \mathbb{Z}⟶𝒫\mathbb{Z}$$
7	4 6	mpbi	$$⊢\dots :\mathbb{Z}\times \mathbb{Z}⟶𝒫\mathbb{Z}$$