ltresr

Description: Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996) (New usage is discouraged.)

		Ref	Expression
	Assertion	ltresr	$⊢ ⟨A, 0_{𝑹}⟩ <_{ℝ} ⟨B, 0_{𝑹}⟩ \leftrightarrow A <_{𝑹} B$

Proof

Step	Hyp	Ref	Expression
1		ltrelre	$⊢ <_{ℝ} \subseteq ℝ^{2}$
2	1	brel	$⊢ ⟨A, 0_{𝑹}⟩ <_{ℝ} ⟨B, 0_{𝑹}⟩ \to (⟨A, 0_{𝑹}⟩ \in ℝ \land ⟨B, 0_{𝑹}⟩ \in ℝ)$
3		opelreal	$⊢ ⟨A, 0_{𝑹}⟩ \in ℝ \leftrightarrow A \in 𝑹$
4		opelreal	$⊢ ⟨B, 0_{𝑹}⟩ \in ℝ \leftrightarrow B \in 𝑹$
5	3 4	anbi12i	$⊢ (⟨A, 0_{𝑹}⟩ \in ℝ \land ⟨B, 0_{𝑹}⟩ \in ℝ) \leftrightarrow (A \in 𝑹 \land B \in 𝑹)$
6	2 5	sylib	$⊢ ⟨A, 0_{𝑹}⟩ <_{ℝ} ⟨B, 0_{𝑹}⟩ \to (A \in 𝑹 \land B \in 𝑹)$
7		ltrelsr	$⊢ <_{𝑹} \subseteq 𝑹 \times 𝑹$
8	7	brel	$⊢ A <_{𝑹} B \to (A \in 𝑹 \land B \in 𝑹)$
9		opex	$⊢ ⟨A, 0_{𝑹}⟩ \in V$
10		opex	$⊢ ⟨B, 0_{𝑹}⟩ \in V$
11		eleq1	$⊢ x = ⟨A, 0_{𝑹}⟩ \to (x \in ℝ \leftrightarrow ⟨A, 0_{𝑹}⟩ \in ℝ)$
12	11	anbi1d	$⊢ x = ⟨A, 0_{𝑹}⟩ \to ((x \in ℝ \land y \in ℝ) \leftrightarrow (⟨A, 0_{𝑹}⟩ \in ℝ \land y \in ℝ))$
13		eqeq1	$⊢ x = ⟨A, 0_{𝑹}⟩ \to (x = ⟨z, 0_{𝑹}⟩ \leftrightarrow ⟨A, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩)$
14	13	anbi1d	$⊢ x = ⟨A, 0_{𝑹}⟩ \to ((x = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩) \leftrightarrow (⟨A, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩))$
15	14	anbi1d	$⊢ x = ⟨A, 0_{𝑹}⟩ \to (((x = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w) \leftrightarrow ((⟨A, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w))$
16	15	2exbidv	$⊢ x = ⟨A, 0_{𝑹}⟩ \to (\exists z \exists w ((x = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w) \leftrightarrow \exists z \exists w ((⟨A, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w))$
17	12 16	anbi12d	$⊢ x = ⟨A, 0_{𝑹}⟩ \to (((x \in ℝ \land y \in ℝ) \land \exists z \exists w ((x = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w)) \leftrightarrow ((⟨A, 0_{𝑹}⟩ \in ℝ \land y \in ℝ) \land \exists z \exists w ((⟨A, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w)))$
18		eleq1	$⊢ y = ⟨B, 0_{𝑹}⟩ \to (y \in ℝ \leftrightarrow ⟨B, 0_{𝑹}⟩ \in ℝ)$
19	18	anbi2d	$⊢ y = ⟨B, 0_{𝑹}⟩ \to ((⟨A, 0_{𝑹}⟩ \in ℝ \land y \in ℝ) \leftrightarrow (⟨A, 0_{𝑹}⟩ \in ℝ \land ⟨B, 0_{𝑹}⟩ \in ℝ))$
20		eqeq1	$⊢ y = ⟨B, 0_{𝑹}⟩ \to (y = ⟨w, 0_{𝑹}⟩ \leftrightarrow ⟨B, 0_{𝑹}⟩ = ⟨w, 0_{𝑹}⟩)$
21	20	anbi2d	$⊢ y = ⟨B, 0_{𝑹}⟩ \to ((⟨A, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩) \leftrightarrow (⟨A, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩ \land ⟨B, 0_{𝑹}⟩ = ⟨w, 0_{𝑹}⟩))$
22	21	anbi1d	$⊢ y = ⟨B, 0_{𝑹}⟩ \to (((⟨A, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w) \leftrightarrow ((⟨A, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩ \land ⟨B, 0_{𝑹}⟩ = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w))$
23	22	2exbidv	$⊢ y = ⟨B, 0_{𝑹}⟩ \to (\exists z \exists w ((⟨A, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w) \leftrightarrow \exists z \exists w ((⟨A, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩ \land ⟨B, 0_{𝑹}⟩ = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w))$
24	19 23	anbi12d	$⊢ y = ⟨B, 0_{𝑹}⟩ \to (((⟨A, 0_{𝑹}⟩ \in ℝ \land y \in ℝ) \land \exists z \exists w ((⟨A, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w)) \leftrightarrow ((⟨A, 0_{𝑹}⟩ \in ℝ \land ⟨B, 0_{𝑹}⟩ \in ℝ) \land \exists z \exists w ((⟨A, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩ \land ⟨B, 0_{𝑹}⟩ = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w)))$
25		df-lt	$⊢ <_{ℝ} = \{⟨x, y⟩ \| ((x \in ℝ \land y \in ℝ) \land \exists z \exists w ((x = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w))\}$
26	9 10 17 24 25	brab	$⊢ ⟨A, 0_{𝑹}⟩ <_{ℝ} ⟨B, 0_{𝑹}⟩ \leftrightarrow ((⟨A, 0_{𝑹}⟩ \in ℝ \land ⟨B, 0_{𝑹}⟩ \in ℝ) \land \exists z \exists w ((⟨A, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩ \land ⟨B, 0_{𝑹}⟩ = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w))$
27	26	baib	$⊢ (⟨A, 0_{𝑹}⟩ \in ℝ \land ⟨B, 0_{𝑹}⟩ \in ℝ) \to (⟨A, 0_{𝑹}⟩ <_{ℝ} ⟨B, 0_{𝑹}⟩ \leftrightarrow \exists z \exists w ((⟨A, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩ \land ⟨B, 0_{𝑹}⟩ = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w))$
28		vex	$⊢ z \in V$
29	28	eqresr	$⊢ ⟨z, 0_{𝑹}⟩ = ⟨A, 0_{𝑹}⟩ \leftrightarrow z = A$
30		eqcom	$⊢ ⟨A, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩ \leftrightarrow ⟨z, 0_{𝑹}⟩ = ⟨A, 0_{𝑹}⟩$
31		eqcom	$⊢ A = z \leftrightarrow z = A$
32	29 30 31	3bitr4i	$⊢ ⟨A, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩ \leftrightarrow A = z$
33		vex	$⊢ w \in V$
34	33	eqresr	$⊢ ⟨w, 0_{𝑹}⟩ = ⟨B, 0_{𝑹}⟩ \leftrightarrow w = B$
35		eqcom	$⊢ ⟨B, 0_{𝑹}⟩ = ⟨w, 0_{𝑹}⟩ \leftrightarrow ⟨w, 0_{𝑹}⟩ = ⟨B, 0_{𝑹}⟩$
36		eqcom	$⊢ B = w \leftrightarrow w = B$
37	34 35 36	3bitr4i	$⊢ ⟨B, 0_{𝑹}⟩ = ⟨w, 0_{𝑹}⟩ \leftrightarrow B = w$
38	32 37	anbi12i	$⊢ (⟨A, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩ \land ⟨B, 0_{𝑹}⟩ = ⟨w, 0_{𝑹}⟩) \leftrightarrow (A = z \land B = w)$
39	28 33	opth2	$⊢ ⟨A, B⟩ = ⟨z, w⟩ \leftrightarrow (A = z \land B = w)$
40	38 39	bitr4i	$⊢ (⟨A, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩ \land ⟨B, 0_{𝑹}⟩ = ⟨w, 0_{𝑹}⟩) \leftrightarrow ⟨A, B⟩ = ⟨z, w⟩$
41	40	anbi1i	$⊢ ((⟨A, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩ \land ⟨B, 0_{𝑹}⟩ = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w) \leftrightarrow (⟨A, B⟩ = ⟨z, w⟩ \land z <_{𝑹} w)$
42	41	2exbii	$⊢ \exists z \exists w ((⟨A, 0_{𝑹}⟩ = ⟨z, 0_{𝑹}⟩ \land ⟨B, 0_{𝑹}⟩ = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w) \leftrightarrow \exists z \exists w (⟨A, B⟩ = ⟨z, w⟩ \land z <_{𝑹} w)$
43	27 42	bitrdi	$⊢ (⟨A, 0_{𝑹}⟩ \in ℝ \land ⟨B, 0_{𝑹}⟩ \in ℝ) \to (⟨A, 0_{𝑹}⟩ <_{ℝ} ⟨B, 0_{𝑹}⟩ \leftrightarrow \exists z \exists w (⟨A, B⟩ = ⟨z, w⟩ \land z <_{𝑹} w))$
44	3 4 43	syl2anbr	$⊢ (A \in 𝑹 \land B \in 𝑹) \to (⟨A, 0_{𝑹}⟩ <_{ℝ} ⟨B, 0_{𝑹}⟩ \leftrightarrow \exists z \exists w (⟨A, B⟩ = ⟨z, w⟩ \land z <_{𝑹} w))$
45		breq12	$⊢ (z = A \land w = B) \to (z <_{𝑹} w \leftrightarrow A <_{𝑹} B)$
46	45	copsex2g	$⊢ (A \in 𝑹 \land B \in 𝑹) \to (\exists z \exists w (⟨A, B⟩ = ⟨z, w⟩ \land z <_{𝑹} w) \leftrightarrow A <_{𝑹} B)$
47	44 46	bitrd	$⊢ (A \in 𝑹 \land B \in 𝑹) \to (⟨A, 0_{𝑹}⟩ <_{ℝ} ⟨B, 0_{𝑹}⟩ \leftrightarrow A <_{𝑹} B)$
48	6 8 47	pm5.21nii	$⊢ ⟨A, 0_{𝑹}⟩ <_{ℝ} ⟨B, 0_{𝑹}⟩ \leftrightarrow A <_{𝑹} B$

Metamath Proof Explorer

Theorem ltresr

Proof