Theorem uzf

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

	Ref	Expression
Assertion	uzf	|- ZZ>= : ZZ --> ~P ZZ

Proof

Step	Hyp	Ref	Expression
1		zex	|- ZZ e. _V
2		ssrab2	|- { k e. ZZ | j <_ k } C_ ZZ
3	1 2	elpwi2	|- { k e. ZZ | j <_ k } e. ~P ZZ
4	3	rgenw	|- A. j e. ZZ { k e. ZZ | j <_ k } e. ~P ZZ
5		df-uz	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
6	5	fmpt	|- ( A. j e. ZZ { k e. ZZ | j <_ k } e. ~P ZZ <-> ZZ>= : ZZ --> ~P ZZ )
7	4 6	mpbi	|- ZZ>= : ZZ --> ~P ZZ