Metamath Proof Explorer


Theorem elfzoelz

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

Ref Expression
Assertion elfzoelz AB..^CA

Proof

Step Hyp Ref Expression
1 elfzoel1 AB..^CB
2 elfzoel2 AB..^CC
3 fzof ..^:×𝒫
4 3 fovcl BCB..^C𝒫
5 1 2 4 syl2anc AB..^CB..^C𝒫
6 5 elpwid AB..^CB..^C
7 id AB..^CAB..^C
8 6 7 sseldd AB..^CA