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		elioore	$⊢ x \in (A, B) \to x \in ℝ$
3	2	ssriv	$⊢ (A, B) \subseteq ℝ$
4	1 3	eqsstrrdi	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to \{x \in ℝ^{*} \| (A < x \land x < B)\} \subseteq ℝ$
5		dfss2	$⊢ \{x \in ℝ^{} \| (A < x \land x < B)\} \subseteq ℝ \leftrightarrow \{x \in ℝ^{} \| (A < x \land x < B)\} \cap ℝ = \{x \in ℝ^{*} \| (A < x \land x < B)\}$
6	4 5	sylib	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to \{x \in ℝ^{} \| (A < x \land x < B)\} \cap ℝ = \{x \in ℝ^{} \| (A < x \land x < B)\}$
7		inrab2	$⊢ \{x \in ℝ^{} \| (A < x \land x < B)\} \cap ℝ = \{x \in (ℝ^{} \cap ℝ) \| (A < x \land x < B)\}$
8		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
9		sseqin2	$⊢ ℝ \subseteq ℝ^{} \leftrightarrow ℝ^{} \cap ℝ = ℝ$
10	8 9	mpbi	$⊢ ℝ^{*} \cap ℝ = ℝ$
11	10	rabeqi	$⊢ \{x \in (ℝ^{*} \cap ℝ) \| (A < x \land x < B)\} = \{x \in ℝ \| (A < x \land x < B)\}$
12	7 11	eqtri	$⊢ \{x \in ℝ^{*} \| (A < x \land x < B)\} \cap ℝ = \{x \in ℝ \| (A < x \land x < B)\}$
13	6 12	eqtr3di	$⊢ (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