Metamath Proof Explorer


Theorem elfzoel1

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

Ref Expression
Assertion elfzoel1 A B ..^ C B

Proof

Step Hyp Ref Expression
1 ne0i A B ..^ C B ..^ C
2 fzof ..^ : × 𝒫
3 2 fdmi dom ..^ = ×
4 3 ndmov ¬ B C B ..^ C =
5 4 necon1ai B ..^ C B C
6 1 5 syl A B ..^ C B C
7 6 simpld A B ..^ C B