iooval2

Description: Value of the open interval function. (Contributed by NM, 6-Feb-2007) (Revised by Mario Carneiro, 3-Nov-2013)

		Ref	Expression
	Assertion	iooval2	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A, B) = \{x \in ℝ \| (A < x \land x < B)\}$

Step	Hyp	Ref	Expression
1		iooval	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A, B) = \{x \in ℝ^{*} \| (A < x \land x < B)\}$
2		inrab2	$⊢ \{x \in ℝ^{} \| (A < x \land x < B)\} \cap ℝ = \{x \in (ℝ^{} \cap ℝ) \| (A < x \land x < B)\}$
3		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
4		sseqin2	$⊢ ℝ \subseteq ℝ^{} \leftrightarrow ℝ^{} \cap ℝ = ℝ$
5	3 4	mpbi	$⊢ ℝ^{*} \cap ℝ = ℝ$
6	5	rabeqi	$⊢ \{x \in (ℝ^{*} \cap ℝ) \| (A < x \land x < B)\} = \{x \in ℝ \| (A < x \land x < B)\}$
7	2 6	eqtri	$⊢ \{x \in ℝ^{*} \| (A < x \land x < B)\} \cap ℝ = \{x \in ℝ \| (A < x \land x < B)\}$
8		elioore	$⊢ x \in (A, B) \to x \in ℝ$
9	8	ssriv	$⊢ (A, B) \subseteq ℝ$
10	1 9	eqsstrrdi	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to \{x \in ℝ^{*} \| (A < x \land x < B)\} \subseteq ℝ$
11		df-ss	$⊢ \{x \in ℝ^{} \| (A < x \land x < B)\} \subseteq ℝ \leftrightarrow \{x \in ℝ^{} \| (A < x \land x < B)\} \cap ℝ = \{x \in ℝ^{*} \| (A < x \land x < B)\}$
12	10 11	sylib	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to \{x \in ℝ^{} \| (A < x \land x < B)\} \cap ℝ = \{x \in ℝ^{} \| (A < x \land x < B)\}$
13	7 12	syl5reqr	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to \{x \in ℝ^{*} \| (A < x \land x < B)\} = \{x \in ℝ \| (A < x \land x < B)\}$
14	1 13	eqtrd	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A, B) = \{x \in ℝ \| (A < x \land x < B)\}$

Metamath Proof Explorer