ltxr

Description: The 'less than' binary relation on the set of extended reals. Definition 12-3.1 of Gleason p. 173. (Contributed by NM, 14-Oct-2005)

		Ref	Expression
	Assertion	ltxr	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A < B \leftrightarrow ((((A \in ℝ \land B \in ℝ) \land A <_{ℝ} B) \lor (A = −∞ \land B = +∞)) \lor ((A \in ℝ \land B = +∞) \lor (A = −∞ \land B \in ℝ))))$

Proof

Step	Hyp	Ref	Expression
1		breq12	$⊢ (x = A \land y = B) \to (x <_{ℝ} y \leftrightarrow A <_{ℝ} B)$
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	1 3	brab2a	$⊢ A \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} B \leftrightarrow ((A \in ℝ \land B \in ℝ) \land A <_{ℝ} B)$
5	4	a1i	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} B \leftrightarrow ((A \in ℝ \land B \in ℝ) \land A <_{ℝ} B))$
6		brun	$⊢ A (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ)) B \leftrightarrow (A ((ℝ \cup \{−∞\}) \times \{+∞\}) B \lor A (\{−∞\} \times ℝ) B)$
7		brxp	$⊢ A ((ℝ \cup \{−∞\}) \times \{+∞\}) B \leftrightarrow (A \in (ℝ \cup \{−∞\}) \land B \in \{+∞\})$
8		elun	$⊢ A \in (ℝ \cup \{−∞\}) \leftrightarrow (A \in ℝ \lor A \in \{−∞\})$
9		orcom	$⊢ (A \in ℝ \lor A \in \{−∞\}) \leftrightarrow (A \in \{−∞\} \lor A \in ℝ)$
10	8 9	bitri	$⊢ A \in (ℝ \cup \{−∞\}) \leftrightarrow (A \in \{−∞\} \lor A \in ℝ)$
11		elsng	$⊢ A \in ℝ^{*} \to (A \in \{−∞\} \leftrightarrow A = −∞)$
12	11	orbi1d	$⊢ A \in ℝ^{*} \to ((A \in \{−∞\} \lor A \in ℝ) \leftrightarrow (A = −∞ \lor A \in ℝ))$
13	10 12	syl5bb	$⊢ A \in ℝ^{*} \to (A \in (ℝ \cup \{−∞\}) \leftrightarrow (A = −∞ \lor A \in ℝ))$
14		elsng	$⊢ B \in ℝ^{*} \to (B \in \{+∞\} \leftrightarrow B = +∞)$
15	13 14	bi2anan9	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A \in (ℝ \cup \{−∞\}) \land B \in \{+∞\}) \leftrightarrow ((A = −∞ \lor A \in ℝ) \land B = +∞))$
16		andir	$⊢ ((A = −∞ \lor A \in ℝ) \land B = +∞) \leftrightarrow ((A = −∞ \land B = +∞) \lor (A \in ℝ \land B = +∞))$
17	15 16	bitrdi	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A \in (ℝ \cup \{−∞\}) \land B \in \{+∞\}) \leftrightarrow ((A = −∞ \land B = +∞) \lor (A \in ℝ \land B = +∞)))$
18	7 17	syl5bb	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A ((ℝ \cup \{−∞\}) \times \{+∞\}) B \leftrightarrow ((A = −∞ \land B = +∞) \lor (A \in ℝ \land B = +∞)))$
19		brxp	$⊢ A (\{−∞\} \times ℝ) B \leftrightarrow (A \in \{−∞\} \land B \in ℝ)$
20	11	anbi1d	$⊢ A \in ℝ^{*} \to ((A \in \{−∞\} \land B \in ℝ) \leftrightarrow (A = −∞ \land B \in ℝ))$
21	20	adantr	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A \in \{−∞\} \land B \in ℝ) \leftrightarrow (A = −∞ \land B \in ℝ))$
22	19 21	syl5bb	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A (\{−∞\} \times ℝ) B \leftrightarrow (A = −∞ \land B \in ℝ))$
23	18 22	orbi12d	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A ((ℝ \cup \{−∞\}) \times \{+∞\}) B \lor A (\{−∞\} \times ℝ) B) \leftrightarrow (((A = −∞ \land B = +∞) \lor (A \in ℝ \land B = +∞)) \lor (A = −∞ \land B \in ℝ)))$
24		orass	$⊢ (((A = −∞ \land B = +∞) \lor (A \in ℝ \land B = +∞)) \lor (A = −∞ \land B \in ℝ)) \leftrightarrow ((A = −∞ \land B = +∞) \lor ((A \in ℝ \land B = +∞) \lor (A = −∞ \land B \in ℝ)))$
25	23 24	bitrdi	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A ((ℝ \cup \{−∞\}) \times \{+∞\}) B \lor A (\{−∞\} \times ℝ) B) \leftrightarrow ((A = −∞ \land B = +∞) \lor ((A \in ℝ \land B = +∞) \lor (A = −∞ \land B \in ℝ))))$
26	6 25	syl5bb	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ)) B \leftrightarrow ((A = −∞ \land B = +∞) \lor ((A \in ℝ \land B = +∞) \lor (A = −∞ \land B \in ℝ))))$
27	5 26	orbi12d	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} B \lor A (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ)) B) \leftrightarrow (((A \in ℝ \land B \in ℝ) \land A <_{ℝ} B) \lor ((A = −∞ \land B = +∞) \lor ((A \in ℝ \land B = +∞) \lor (A = −∞ \land B \in ℝ)))))$
28		df-ltxr	$⊢ < = \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} \cup (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ))$
29	28	breqi	$⊢ A < B \leftrightarrow A (\{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} \cup (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ))) B$
30		brun	$⊢ A (\{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} \cup (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ))) B \leftrightarrow (A \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} B \lor A (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ)) B)$
31	29 30	bitri	$⊢ A < B \leftrightarrow (A \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} B \lor A (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ)) B)$
32		orass	$⊢ ((((A \in ℝ \land B \in ℝ) \land A <_{ℝ} B) \lor (A = −∞ \land B = +∞)) \lor ((A \in ℝ \land B = +∞) \lor (A = −∞ \land B \in ℝ))) \leftrightarrow (((A \in ℝ \land B \in ℝ) \land A <_{ℝ} B) \lor ((A = −∞ \land B = +∞) \lor ((A \in ℝ \land B = +∞) \lor (A = −∞ \land B \in ℝ))))$
33	27 31 32	3bitr4g	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A < B \leftrightarrow ((((A \in ℝ \land B \in ℝ) \land A <_{ℝ} B) \lor (A = −∞ \land B = +∞)) \lor ((A \in ℝ \land B = +∞) \lor (A = −∞ \land B \in ℝ))))$

Metamath Proof Explorer

Theorem ltxr

Proof