Theorem uzf

Description: The domain and codomain of the upper integers function. (Contributed by Scott Fenton, 8-Aug-2013) (Revised by Mario Carneiro, 3-Nov-2013)

	Ref	Expression
Assertion	uzf	$$⊢{\mathbb{Z}}_{\ge }:\mathbb{Z}⟶𝒫\mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		zex	$$⊢\mathbb{Z}\in \mathrm{V}$$
2		ssrab2	$$⊢\left\{k\in \mathbb{Z}|j\le k\right\}\subseteq \mathbb{Z}$$
3	1 2	elpwi2	$$⊢\left\{k\in \mathbb{Z}|j\le k\right\}\in 𝒫\mathbb{Z}$$
4	3	rgenw	$$⊢\forall j\in \mathbb{Z}\left\{k\in \mathbb{Z}|j\le k\right\}\in 𝒫\mathbb{Z}$$
5		df-uz	$$⊢{\mathbb{Z}}_{\ge }=\left(j\in \mathbb{Z}⟼\left\{k\in \mathbb{Z}|j\le k\right\}\right)$$
6	5	fmpt	$$⊢\forall j\in \mathbb{Z}\left\{k\in \mathbb{Z}|j\le k\right\}\in 𝒫\mathbb{Z}\leftrightarrow {\mathbb{Z}}_{\ge }:\mathbb{Z}⟶𝒫\mathbb{Z}$$
7	4 6	mpbi	$$⊢{\mathbb{Z}}_{\ge }:\mathbb{Z}⟶𝒫\mathbb{Z}$$