Definition df-ltr 7692

Description: Define ordering relation on signed reals. This is a "temporary" set used in the construction of complex numbers, 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.)

Assertion

Ref	Expression
df-ltr	|- <R = { <. x , y >. | ( ( x e. R. /\ y e. R. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u ) <P ( w +P. v ) ) ) }

Distinct variable group:   x, y, z, w, v, u

Detailed syntax breakdown of Definition df-ltr

Step	Hyp	Ref	Expression
1		cltr 7265	. 2 class <R
2		vx	. . . . . . 7 setvar x
3	2	cv 1347	. . . . . 6 class x
4		cnr 7259	. . . . . 6 class R.
5	3, 4	wcel 2141	. . . . 5 wff x e. R.
6		vy	. . . . . . 7 setvar y
7	6	cv 1347	. . . . . 6 class y
8	7, 4	wcel 2141	. . . . 5 wff y e. R.
9	5, 8	wa 103	. . . 4 wff ( x e. R. /\ y e. R. )
10		vz	. . . . . . . . . . . . . 14 setvar z
11	10	cv 1347	. . . . . . . . . . . . 13 class z
12		vw	. . . . . . . . . . . . . 14 setvar w
13	12	cv 1347	. . . . . . . . . . . . 13 class w
14	11, 13	cop 3586	. . . . . . . . . . . 12 class <. z , w >.
15		cer 7258	. . . . . . . . . . . 12 class ~R
16	14, 15	cec 6511	. . . . . . . . . . 11 class [ <. z , w >. ] ~R
17	3, 16	wceq 1348	. . . . . . . . . 10 wff x = [ <. z , w >. ] ~R
18		vv	. . . . . . . . . . . . . 14 setvar v
19	18	cv 1347	. . . . . . . . . . . . 13 class v
20		vu	. . . . . . . . . . . . . 14 setvar u
21	20	cv 1347	. . . . . . . . . . . . 13 class u
22	19, 21	cop 3586	. . . . . . . . . . . 12 class <. v , u >.
23	22, 15	cec 6511	. . . . . . . . . . 11 class [ <. v , u >. ] ~R
24	7, 23	wceq 1348	. . . . . . . . . 10 wff y = [ <. v , u >. ] ~R
25	17, 24	wa 103	. . . . . . . . 9 wff ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R )
26		cpp 7255	. . . . . . . . . . 11 class +P.
27	11, 21, 26	co 5853	. . . . . . . . . 10 class ( z +P. u )
28	13, 19, 26	co 5853	. . . . . . . . . 10 class ( w +P. v )
29		cltp 7257	. . . . . . . . . 10 class <P
30	27, 28, 29	wbr 3989	. . . . . . . . 9 wff ( z +P. u ) <P ( w +P. v )
31	25, 30	wa 103	. . . . . . . 8 wff ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u ) <P ( w +P. v ) )
32	31, 20	wex 1485	. . . . . . 7 wff E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u ) <P ( w +P. v ) )
33	32, 18	wex 1485	. . . . . 6 wff E. v E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u ) <P ( w +P. v ) )
34	33, 12	wex 1485	. . . . 5 wff E. w E. v E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u ) <P ( w +P. v ) )
35	34, 10	wex 1485	. . . 4 wff E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u ) <P ( w +P. v ) )
36	9, 35	wa 103	. . 3 wff ( ( x e. R. /\ y e. R. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u ) <P ( w +P. v ) ) )
37	36, 2, 6	copab 4049	. 2 class { <. x , y >. | ( ( x e. R. /\ y e. R. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u ) <P ( w +P. v ) ) ) }
38	1, 37	wceq 1348	1 wff <R = { <. x , y >. | ( ( x e. R. /\ y e. R. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u ) <P ( w +P. v ) ) ) }

This definition is referenced by:  ltrelsr  7700  ltsrprg  7709