df-ioc

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

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

Step	Hyp	Ref	Expression
0		cioc	$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		cle	$class \leq$
10	3	cv	$setvar y$
11	7 10 9	wbr	$wff z \leq y$
12	8 11	wa	$wff (x < z \land z \leq y)$
13	12 4 2	crab	$class \{z \in ℝ^{*} \| (x < z \land z \leq y)\}$
14	1 3 2 2 13	cmpo	$class (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z \leq y)\})$
15	0 14	wceq	$wff (.] = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z \leq y)\})$

Metamath Proof Explorer