fzon0

Description: A half-open integer interval is nonempty iff it contains its left endpoint. (Contributed by Mario Carneiro, 29-Sep-2015)

		Ref	Expression
	Assertion	fzon0	$⊢ (M ..^N) \neq \emptyset \leftrightarrow M \in (M ..^N)$

Step	Hyp	Ref	Expression
1		n0	$⊢ (M ..^N) \neq \emptyset \leftrightarrow \exists x x \in (M ..^N)$
2		elfzolt3b	$⊢ x \in (M ..^N) \to M \in (M ..^N)$
3	2	exlimiv	$⊢ \exists x x \in (M ..^N) \to M \in (M ..^N)$
4	1 3	sylbi	$⊢ (M ..^N) \neq \emptyset \to M \in (M ..^N)$
5		ne0i	$⊢ M \in (M ..^N) \to (M ..^N) \neq \emptyset$
6	4 5	impbii	$⊢ (M ..^N) \neq \emptyset \leftrightarrow M \in (M ..^N)$

Metamath Proof Explorer