df-ltxr

Description: Define 'less than' on the set of extended reals. Definition 12-3.1 of Gleason p. 173. Note that in our postulates for complex numbers, is primitive and not necessarily a relation on RR . (Contributed by NM, 13-Oct-2005)

		Ref	Expression
	Assertion	df-ltxr	$⊢ < = \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} \cup (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clt	$class <$
1		vx	$setvar x$
2		vy	$setvar y$
3	1	cv	$setvar x$
4		cr	$class ℝ$
5	3 4	wcel	$wff x \in ℝ$
6	2	cv	$setvar y$
7	6 4	wcel	$wff y \in ℝ$
8		cltrr	$class <_{ℝ}$
9	3 6 8	wbr	$wff x <_{ℝ} y$
10	5 7 9	w3a	$wff (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)$
11	10 1 2	copab	$class \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\}$
12		cmnf	$class −∞$
13	12	csn	$class \{−∞\}$
14	4 13	cun	$class (ℝ \cup \{−∞\})$
15		cpnf	$class +∞$
16	15	csn	$class \{+∞\}$
17	14 16	cxp	$class ((ℝ \cup \{−∞\}) \times \{+∞\})$
18	13 4	cxp	$class (\{−∞\} \times ℝ)$
19	17 18	cun	$class (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ))$
20	11 19	cun	$class (\{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} \cup (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ)))$
21	0 20	wceq	$wff < = \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} \cup (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ))$

Metamath Proof Explorer

Definition df-ltxr

Detailed syntax breakdown