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 ∈ B ..^ C → C ∈ ℤ

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 simprd ⊢ A ∈ B ..^ C → C ∈ ℤ