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