df-ioo

Description: Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006)

		Ref	Expression
	Assertion	df-ioo	$⊢ (.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z < y)\})$

Step	Hyp	Ref	Expression
0		cioo	$class (.)$
1		vx	$setvar x$
2		cxr	$class ℝ^{*}$
3		vy	$setvar y$
4		vz	$setvar z$
5	1	cv	$setvar x$
6		clt	$class <$
7	4	cv	$setvar z$
8	5 7 6	wbr	$wff x < z$
9	3	cv	$setvar y$
10	7 9 6	wbr	$wff z < y$
11	8 10	wa	$wff (x < z \land z < y)$
12	11 4 2	crab	$class \{z \in ℝ^{*} \| (x < z \land z < y)\}$
13	1 3 2 2 12	cmpo	$class (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z < y)\})$
14	0 13	wceq	$wff (.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z < y)\})$

Metamath Proof Explorer