ltxrlt

Description: The standard less-than and the extended real less-than < are identical when restricted to the non-extended reals RR . (Contributed by NM, 13-Oct-2005) (Revised by Mario Carneiro, 28-Apr-2015)

		Ref	Expression
	Assertion	ltxrlt	$⊢ (A \in ℝ \land B \in ℝ) \to (A < B \leftrightarrow A <_{ℝ} B)$

Proof

Step	Hyp	Ref	Expression
1		brun	$⊢ A (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ)) B \leftrightarrow (A ((ℝ \cup \{−∞\}) \times \{+∞\}) B \lor A (\{−∞\} \times ℝ) B)$
2		brxp	$⊢ A ((ℝ \cup \{−∞\}) \times \{+∞\}) B \leftrightarrow (A \in (ℝ \cup \{−∞\}) \land B \in \{+∞\})$
3		elsni	$⊢ B \in \{+∞\} \to B = +∞$
4		pnfnre	$⊢ +∞ \notin ℝ$
5	4	neli	$⊢ \neg +∞ \in ℝ$
6		simpr	$⊢ (A \in ℝ \land B \in ℝ) \to B \in ℝ$
7		eleq1	$⊢ B = +∞ \to (B \in ℝ \leftrightarrow +∞ \in ℝ)$
8	6 7	syl5ib	$⊢ B = +∞ \to ((A \in ℝ \land B \in ℝ) \to +∞ \in ℝ)$
9	5 8	mtoi	$⊢ B = +∞ \to \neg (A \in ℝ \land B \in ℝ)$
10	3 9	syl	$⊢ B \in \{+∞\} \to \neg (A \in ℝ \land B \in ℝ)$
11	2 10	simplbiim	$⊢ A ((ℝ \cup \{−∞\}) \times \{+∞\}) B \to \neg (A \in ℝ \land B \in ℝ)$
12		brxp	$⊢ A (\{−∞\} \times ℝ) B \leftrightarrow (A \in \{−∞\} \land B \in ℝ)$
13		elsni	$⊢ A \in \{−∞\} \to A = −∞$
14		mnfnre	$⊢ −∞ \notin ℝ$
15	14	neli	$⊢ \neg −∞ \in ℝ$
16		simpl	$⊢ (A \in ℝ \land B \in ℝ) \to A \in ℝ$
17		eleq1	$⊢ A = −∞ \to (A \in ℝ \leftrightarrow −∞ \in ℝ)$
18	16 17	syl5ib	$⊢ A = −∞ \to ((A \in ℝ \land B \in ℝ) \to −∞ \in ℝ)$
19	15 18	mtoi	$⊢ A = −∞ \to \neg (A \in ℝ \land B \in ℝ)$
20	13 19	syl	$⊢ A \in \{−∞\} \to \neg (A \in ℝ \land B \in ℝ)$
21	20	adantr	$⊢ (A \in \{−∞\} \land B \in ℝ) \to \neg (A \in ℝ \land B \in ℝ)$
22	12 21	sylbi	$⊢ A (\{−∞\} \times ℝ) B \to \neg (A \in ℝ \land B \in ℝ)$
23	11 22	jaoi	$⊢ (A ((ℝ \cup \{−∞\}) \times \{+∞\}) B \lor A (\{−∞\} \times ℝ) B) \to \neg (A \in ℝ \land B \in ℝ)$
24	1 23	sylbi	$⊢ A (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ)) B \to \neg (A \in ℝ \land B \in ℝ)$
25	24	con2i	$⊢ (A \in ℝ \land B \in ℝ) \to \neg A (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ)) B$
26		df-ltxr	$⊢ < = \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} \cup (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ))$
27	26	equncomi	$⊢ < = (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ)) \cup \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\}$
28	27	breqi	$⊢ A < B \leftrightarrow A ((((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ)) \cup \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\}) B$
29		brun	$⊢ A ((((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ)) \cup \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\}) B \leftrightarrow (A (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ)) B \lor A \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} B)$
30		df-or	$⊢ (A (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ)) B \lor A \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} B) \leftrightarrow (\neg A (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ)) B \to A \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} B)$
31	28 29 30	3bitri	$⊢ A < B \leftrightarrow (\neg A (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ)) B \to A \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} B)$
32		biimt	$⊢ \neg A (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ)) B \to (A \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} B \leftrightarrow (\neg A (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ)) B \to A \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} B))$
33	31 32	bitr4id	$⊢ \neg A (((ℝ \cup \{−∞\}) \times \{+∞\}) \cup (\{−∞\} \times ℝ)) B \to (A < B \leftrightarrow A \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} B)$
34	25 33	syl	$⊢ (A \in ℝ \land B \in ℝ) \to (A < B \leftrightarrow A \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} B)$
35		breq12	$⊢ (x = A \land y = B) \to (x <_{ℝ} y \leftrightarrow A <_{ℝ} B)$
36		df-3an	$⊢ (x \in ℝ \land y \in ℝ \land x <_{ℝ} y) \leftrightarrow ((x \in ℝ \land y \in ℝ) \land x <_{ℝ} y)$
37	36	opabbii	$⊢ \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} = \{⟨x, y⟩ \| ((x \in ℝ \land y \in ℝ) \land x <_{ℝ} y)\}$
38	35 37	brab2a	$⊢ A \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} B \leftrightarrow ((A \in ℝ \land B \in ℝ) \land A <_{ℝ} B)$
39	38	baibr	$⊢ (A \in ℝ \land B \in ℝ) \to (A <_{ℝ} B \leftrightarrow A \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ \land x <_{ℝ} y)\} B)$
40	34 39	bitr4d	$⊢ (A \in ℝ \land B \in ℝ) \to (A < B \leftrightarrow A <_{ℝ} B)$

Metamath Proof Explorer

Theorem ltxrlt

Proof