Description: Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | elfzoel2 | ⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → 𝐶 ∈ ℤ ) |
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 | ⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → 𝐶 ∈ ℤ ) |