Theorem elfzoel1

Description: Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015)

	Ref	Expression
Assertion	elfzoel1	|- ( A e. ( B ..^ C ) -> B e. ZZ )

Proof

Step	Hyp	Ref	Expression
1		ne0i	|- ( A e. ( B ..^ C ) -> ( B ..^ C ) =/= (/) )
2		fzof	|- ..^ : ( ZZ X. ZZ ) --> ~P ZZ
3	2	fdmi	|- dom ..^ = ( ZZ X. ZZ )
4	3	ndmov	|- ( -. ( B e. ZZ /\ C e. ZZ ) -> ( B ..^ C ) = (/) )
5	4	necon1ai	|- ( ( B ..^ C ) =/= (/) -> ( B e. ZZ /\ C e. ZZ ) )
6	1 5	syl	|- ( A e. ( B ..^ C ) -> ( B e. ZZ /\ C e. ZZ ) )
7	6	simpld	|- ( A e. ( B ..^ C ) -> B e. ZZ )