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 ) |
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 ) |