elfzoel2

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

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

Step	Hyp	Ref	Expression
1		ne0i	$⊢ A \in (B ..^C) \to (B ..^C) \neq \emptyset$
2		fzof	$⊢ ..^: ℤ \times ℤ ⟶ 𝒫 ℤ$
3	2	fdmi	$⊢ dom ..^= ℤ \times ℤ$
4	3	ndmov	$⊢ \neg (B \in ℤ \land C \in ℤ) \to (B ..^C) = \emptyset$
5	4	necon1ai	$⊢ (B ..^C) \neq \emptyset \to (B \in ℤ \land C \in ℤ)$
6	1 5	syl	$⊢ A \in (B ..^C) \to (B \in ℤ \land C \in ℤ)$
7	6	simprd	$⊢ A \in (B ..^C) \to C \in ℤ$

Metamath Proof Explorer