df-ltr

Description: Define ordering relation on signed reals. This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. From Proposition 9-4.4 of Gleason p. 127. (Contributed by NM, 14-Feb-1996) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-ltr	$⊢ <_{𝑹} = \{⟨x, y⟩ \| ((x \in 𝑹 \land y \in 𝑹) \land \exists z \exists w \exists v \exists u ((x = [⟨z, w⟩] ~_{𝑹} \land y = [⟨v, u⟩] ~_{𝑹}) \land (z +_{𝑷} u) <_{𝑷} (w +_{𝑷} v)))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cltr	$class <_{𝑹}$
1		vx	$setvar x$
2		vy	$setvar y$
3	1	cv	$setvar x$
4		cnr	$class 𝑹$
5	3 4	wcel	$wff x \in 𝑹$
6	2	cv	$setvar y$
7	6 4	wcel	$wff y \in 𝑹$
8	5 7	wa	$wff (x \in 𝑹 \land y \in 𝑹)$
9		vz	$setvar z$
10		vw	$setvar w$
11		vv	$setvar v$
12		vu	$setvar u$
13	9	cv	$setvar z$
14	10	cv	$setvar w$
15	13 14	cop	$class ⟨z, w⟩$
16		cer	$class ~_{𝑹}$
17	15 16	cec	$class [⟨z, w⟩] ~_{𝑹}$
18	3 17	wceq	$wff x = [⟨z, w⟩] ~_{𝑹}$
19	11	cv	$setvar v$
20	12	cv	$setvar u$
21	19 20	cop	$class ⟨v, u⟩$
22	21 16	cec	$class [⟨v, u⟩] ~_{𝑹}$
23	6 22	wceq	$wff y = [⟨v, u⟩] ~_{𝑹}$
24	18 23	wa	$wff (x = [⟨z, w⟩] ~_{𝑹} \land y = [⟨v, u⟩] ~_{𝑹})$
25		cpp	$class +_{𝑷}$
26	13 20 25	co	$class (z +_{𝑷} u)$
27		cltp	$class <_{𝑷}$
28	14 19 25	co	$class (w +_{𝑷} v)$
29	26 28 27	wbr	$wff (z +_{𝑷} u) <_{𝑷} (w +_{𝑷} v)$
30	24 29	wa	$wff ((x = [⟨z, w⟩] ~_{𝑹} \land y = [⟨v, u⟩] ~_{𝑹}) \land (z +_{𝑷} u) <_{𝑷} (w +_{𝑷} v))$
31	30 12	wex	$wff \exists u ((x = [⟨z, w⟩] ~_{𝑹} \land y = [⟨v, u⟩] ~_{𝑹}) \land (z +_{𝑷} u) <_{𝑷} (w +_{𝑷} v))$
32	31 11	wex	$wff \exists v \exists u ((x = [⟨z, w⟩] ~_{𝑹} \land y = [⟨v, u⟩] ~_{𝑹}) \land (z +_{𝑷} u) <_{𝑷} (w +_{𝑷} v))$
33	32 10	wex	$wff \exists w \exists v \exists u ((x = [⟨z, w⟩] ~_{𝑹} \land y = [⟨v, u⟩] ~_{𝑹}) \land (z +_{𝑷} u) <_{𝑷} (w +_{𝑷} v))$
34	33 9	wex	$wff \exists z \exists w \exists v \exists u ((x = [⟨z, w⟩] ~_{𝑹} \land y = [⟨v, u⟩] ~_{𝑹}) \land (z +_{𝑷} u) <_{𝑷} (w +_{𝑷} v))$
35	8 34	wa	$wff ((x \in 𝑹 \land y \in 𝑹) \land \exists z \exists w \exists v \exists u ((x = [⟨z, w⟩] ~_{𝑹} \land y = [⟨v, u⟩] ~_{𝑹}) \land (z +_{𝑷} u) <_{𝑷} (w +_{𝑷} v)))$
36	35 1 2	copab	$class \{⟨x, y⟩ \| ((x \in 𝑹 \land y \in 𝑹) \land \exists z \exists w \exists v \exists u ((x = [⟨z, w⟩] ~_{𝑹} \land y = [⟨v, u⟩] ~_{𝑹}) \land (z +_{𝑷} u) <_{𝑷} (w +_{𝑷} v)))\}$
37	0 36	wceq	$wff <_{𝑹} = \{⟨x, y⟩ \| ((x \in 𝑹 \land y \in 𝑹) \land \exists z \exists w \exists v \exists u ((x = [⟨z, w⟩] ~_{𝑹} \land y = [⟨v, u⟩] ~_{𝑹}) \land (z +_{𝑷} u) <_{𝑷} (w +_{𝑷} v)))\}$

Metamath Proof Explorer

Definition df-ltr

Detailed syntax breakdown