ltrelxr

Description: "Less than" is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015)

		Ref	Expression
	Assertion	ltrelxr	$⊢ < \subseteq ℝ^{} \times ℝ^{}$

Proof

Step	Hyp	Ref	Expression
1		df-ltxr	$⊢ < = \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} \cup (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ))$
2		df-3an	$⊢ (x \in ℝ \land y \in ℝ \land x <_{ℝ} y) \leftrightarrow ((x \in ℝ \land y \in ℝ) \land x <_{ℝ} y)$
3	2	opabbii	$⊢ \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} = \{⟨x, y⟩ \| ((x \in ℝ \land y \in ℝ) \land x <_{ℝ} y)\}$
4		opabssxp	$⊢ \{⟨x, y⟩ \| ((x \in ℝ \land y \in ℝ) \land x <_{ℝ} y)\} \subseteq ℝ^{2}$
5	3 4	eqsstri	$⊢ \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} \subseteq ℝ^{2}$
6		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
7	5 6	sstri	$⊢ \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} \subseteq ℝ^{} \times ℝ^{}$
8		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
9		snsspr2	$⊢ \{−∞\} \subseteq \{+∞, −∞\}$
10		ssun2	$⊢ \{+∞, −∞\} \subseteq ℝ \cup \{+∞, −∞\}$
11		df-xr	$⊢ ℝ^{*} = ℝ \cup \{+∞, −∞\}$
12	10 11	sseqtrri	$⊢ \{+∞, −∞\} \subseteq ℝ^{*}$
13	9 12	sstri	$⊢ \{−∞\} \subseteq ℝ^{*}$
14	8 13	unssi	$⊢ ℝ \cup \{−∞\} \subseteq ℝ^{*}$
15		snsspr1	$⊢ \{+∞\} \subseteq \{+∞, −∞\}$
16	15 12	sstri	$⊢ \{+∞\} \subseteq ℝ^{*}$
17		xpss12	$⊢ (ℝ \cup \{−∞\} \subseteq ℝ^{} \land \{+∞\} \subseteq ℝ^{}) \to (ℝ \cup \{−∞\}) \times \{+∞\} \subseteq ℝ^{} \times ℝ^{}$
18	14 16 17	mp2an	$⊢ (ℝ \cup \{−∞\}) \times \{+∞\} \subseteq ℝ^{} \times ℝ^{}$
19		xpss12	$⊢ (\{−∞\} \subseteq ℝ^{} \land ℝ \subseteq ℝ^{}) \to \{−∞\} \times ℝ \subseteq ℝ^{} \times ℝ^{}$
20	13 8 19	mp2an	$⊢ \{−∞\} \times ℝ \subseteq ℝ^{} \times ℝ^{}$
21	18 20	unssi	$⊢ ((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ) \subseteq ℝ^{} \times ℝ^{}$
22	7 21	unssi	$⊢ \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} \cup (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ)) \subseteq ℝ^{} \times ℝ^{}$
23	1 22	eqsstri	$⊢ < \subseteq ℝ^{} \times ℝ^{}$

Metamath Proof Explorer

Theorem ltrelxr

Proof