Metamath Proof Explorer


Theorem elfzoel2

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

Ref Expression
Assertion elfzoel2
|- ( A e. ( B ..^ C ) -> C 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 simprd
 |-  ( A e. ( B ..^ C ) -> C e. ZZ )