elfzoelz

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

		Ref	Expression
	Assertion	elfzoelz	$⊢ A \in (B ..^C) \to A \in ℤ$

Step	Hyp	Ref	Expression
1		elfzoel1	$⊢ A \in (B ..^C) \to B \in ℤ$
2		elfzoel2	$⊢ A \in (B ..^C) \to C \in ℤ$
3		fzof	$⊢ ..^: ℤ \times ℤ ⟶ 𝒫 ℤ$
4	3	fovcl	$⊢ (B \in ℤ \land C \in ℤ) \to (B ..^C) \in 𝒫 ℤ$
5	1 2 4	syl2anc	$⊢ A \in (B ..^C) \to (B ..^C) \in 𝒫 ℤ$
6	5	elpwid	$⊢ A \in (B ..^C) \to (B ..^C) \subseteq ℤ$
7		id	$⊢ A \in (B ..^C) \to A \in (B ..^C)$
8	6 7	sseldd	$⊢ A \in (B ..^C) \to A \in ℤ$

Metamath Proof Explorer