Theorem elfzoelz

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

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

Proof

Step	Hyp	Ref	Expression
1		elfzoel1	|- ( A e. ( B ..^ C ) -> B e. ZZ )
2		elfzoel2	|- ( A e. ( B ..^ C ) -> C e. ZZ )
3		fzof	|- ..^ : ( ZZ X. ZZ ) --> ~P ZZ
4	3	fovcl	|- ( ( B e. ZZ /\ C e. ZZ ) -> ( B ..^ C ) e. ~P ZZ )
5	1 2 4	syl2anc	|- ( A e. ( B ..^ C ) -> ( B ..^ C ) e. ~P ZZ )
6	5	elpwid	|- ( A e. ( B ..^ C ) -> ( B ..^ C ) C_ ZZ )
7		id	|- ( A e. ( B ..^ C ) -> A e. ( B ..^ C ) )
8	6 7	sseldd	|- ( A e. ( B ..^ C ) -> A e. ZZ )