Theorem fzof

Description: Functionality of the half-open integer set function. (Contributed by Stefan O'Rear, 14-Aug-2015)

	Ref	Expression
Assertion	fzof	|- ..^ : ( ZZ X. ZZ ) --> ~P ZZ

Proof

Step	Hyp	Ref	Expression
1		fzssz	|- ( m ... ( n - 1 ) ) C_ ZZ
2		ovex	|- ( m ... ( n - 1 ) ) e. _V
3	2	elpw	|- ( ( m ... ( n - 1 ) ) e. ~P ZZ <-> ( m ... ( n - 1 ) ) C_ ZZ )
4	1 3	mpbir	|- ( m ... ( n - 1 ) ) e. ~P ZZ
5	4	rgen2w	|- A. m e. ZZ A. n e. ZZ ( m ... ( n - 1 ) ) e. ~P ZZ
6		df-fzo	|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
7	6	fmpo	|- ( A. m e. ZZ A. n e. ZZ ( m ... ( n - 1 ) ) e. ~P ZZ <-> ..^ : ( ZZ X. ZZ ) --> ~P ZZ )
8	5 7	mpbi	|- ..^ : ( ZZ X. ZZ ) --> ~P ZZ