iooinlbub

Description: An open interval has empty intersection with its bounds. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Assertion	iooinlbub	$⊢ (A, B) \cap \{A, B\} = \emptyset$

Step	Hyp	Ref	Expression
1		disjr	$⊢ (A, B) \cap \{A, B\} = \emptyset \leftrightarrow \forall x \in \{A, B\} \neg x \in (A, B)$
2		elpri	$⊢ x \in \{A, B\} \to (x = A \lor x = B)$
3		lbioo	$⊢ \neg A \in (A, B)$
4		eleq1	$⊢ x = A \to (x \in (A, B) \leftrightarrow A \in (A, B))$
5	3 4	mtbiri	$⊢ x = A \to \neg x \in (A, B)$
6		ubioo	$⊢ \neg B \in (A, B)$
7		eleq1	$⊢ x = B \to (x \in (A, B) \leftrightarrow B \in (A, B))$
8	6 7	mtbiri	$⊢ x = B \to \neg x \in (A, B)$
9	5 8	jaoi	$⊢ (x = A \lor x = B) \to \neg x \in (A, B)$
10	2 9	syl	$⊢ x \in \{A, B\} \to \neg x \in (A, B)$
11	1 10	mprgbir	$⊢ (A, B) \cap \{A, B\} = \emptyset$

Metamath Proof Explorer