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	|- ... : ( ZZ X. ZZ ) --> ~P ZZ

Proof

Step	Hyp	Ref	Expression
1		zex	|- ZZ e. _V
2		ssrab2	|- { k e. ZZ | ( m <_ k /\ k <_ n ) } C_ ZZ
3	1 2	elpwi2	|- { k e. ZZ | ( m <_ k /\ k <_ n ) } e. ~P ZZ
4	3	rgen2w	|- A. m e. ZZ A. n e. ZZ { k e. ZZ | ( m <_ k /\ k <_ n ) } e. ~P ZZ
5		df-fz	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
6	5	fmpo	|- ( A. m e. ZZ A. n e. ZZ { k e. ZZ | ( m <_ k /\ k <_ n ) } e. ~P ZZ <-> ... : ( ZZ X. ZZ ) --> ~P ZZ )
7	4 6	mpbi	|- ... : ( ZZ X. ZZ ) --> ~P ZZ