Theorem elfzoelz

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

	Ref	Expression
Assertion	elfzoelz	⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → 𝐴 ∈ ℤ )

Proof

Step	Hyp	Ref	Expression
1		elfzoel1	⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → 𝐵 ∈ ℤ )
2		elfzoel2	⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → 𝐶 ∈ ℤ )
3		fzof	⊢ ..^ : ( ℤ × ℤ ) ⟶ 𝒫 ℤ
4	3	fovcl	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 ..^ 𝐶 ) ∈ 𝒫 ℤ )
5	1 2 4	syl2anc	⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → ( 𝐵 ..^ 𝐶 ) ∈ 𝒫 ℤ )
6	5	elpwid	⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → ( 𝐵 ..^ 𝐶 ) ⊆ ℤ )
7		id	⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) )
8	6 7	sseldd	⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → 𝐴 ∈ ℤ )