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 ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → 𝐶 ∈ ℤ )

Proof

Step Hyp Ref Expression
1 ne0i ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → ( 𝐵 ..^ 𝐶 ) ≠ ∅ )
2 fzof ..^ : ( ℤ × ℤ ) ⟶ 𝒫 ℤ
3 2 fdmi dom ..^ = ( ℤ × ℤ )
4 3 ndmov ( ¬ ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 ..^ 𝐶 ) = ∅ )
5 4 necon1ai ( ( 𝐵 ..^ 𝐶 ) ≠ ∅ → ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) )
6 1 5 syl ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) )
7 6 simprd ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → 𝐶 ∈ ℤ )