Definition df-ltr 6322

Description: Define ordering relation on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 6392, and is intended to be used only by the construction. From Proposition 9-4.4 of [Gleason] p. 127.

Assertion

Ref	Expression
df-ltr	|- <R = {<.x, y>. | ((x e. R. /\ y e. R.) /\ E.zE.wE.vE.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 6151	. 2 class <R
2		vx	. . . . . . 7 set x
3	2	cv 1297	. . . . . 6 class x
4		cnr 6145	. . . . . 6 class R.
5	3, 4	wcel 1300	. . . . 5 wff x e. R.
6		vy	. . . . . . 7 set y
7	6	cv 1297	. . . . . 6 class y
8	7, 4	wcel 1300	. . . . 5 wff y e. R.
9	5, 8	wa 240	. . . 4 wff (x e. R. /\ y e. R.)
10		vz	. . . . . . . . . . . . . 14 set z
11	10	cv 1297	. . . . . . . . . . . . 13 class z
12		vw	. . . . . . . . . . . . . 14 set w
13	12	cv 1297	. . . . . . . . . . . . 13 class w
14	11, 13	cop 3046	. . . . . . . . . . . 12 class <.z, w>.
15		cer 6144	. . . . . . . . . . . 12 class ~R
16	14, 15	cec 5316	. . . . . . . . . . 11 class [<.z, w>.] ~R
17	3, 16	wceq 1298	. . . . . . . . . 10 wff x = [<.z, w>.] ~R
18		vv	. . . . . . . . . . . . . 14 set v
19	18	cv 1297	. . . . . . . . . . . . 13 class v
20		vu	. . . . . . . . . . . . . 14 set u
21	20	cv 1297	. . . . . . . . . . . . 13 class u
22	19, 21	cop 3046	. . . . . . . . . . . 12 class <.v, u>.
23	22, 15	cec 5316	. . . . . . . . . . 11 class [<.v, u>.] ~R
24	7, 23	wceq 1298	. . . . . . . . . 10 wff y = [<.v, u>.] ~R
25	17, 24	wa 240	. . . . . . . . 9 wff (x = [<.z, w>.] ~R /\ y = [<.v, u>.] ~R )
26		cpp 6139	. . . . . . . . . . 11 class +P.
27	11, 21, 26	co 4884	. . . . . . . . . 10 class (z +P. u)
28	13, 19, 26	co 4884	. . . . . . . . . 10 class (w +P. v)
29		cltp 6141	. . . . . . . . . 10 class <P
30	27, 28, 29	wbr 3338	. . . . . . . . 9 wff (z +P. u) <P (w +P. v)
31	25, 30	wa 240	. . . . . . . 8 wff ((x = [<.z, w>.] ~R /\ y = [<.v, u>.] ~R ) /\ (z +P. u) <P (w +P. v))
32	31, 20	wex 1326	. . . . . . 7 wff E.u((x = [<.z, w>.] ~R /\ y = [<.v, u>.] ~R ) /\ (z +P. u) <P (w +P. v))
33	32, 18	wex 1326	. . . . . 6 wff E.vE.u((x = [<.z, w>.] ~R /\ y = [<.v, u>.] ~R ) /\ (z +P. u) <P (w +P. v))
34	33, 12	wex 1326	. . . . 5 wff E.wE.vE.u((x = [<.z, w>.] ~R /\ y = [<.v, u>.] ~R ) /\ (z +P. u) <P (w +P. v))
35	34, 10	wex 1326	. . . 4 wff E.zE.wE.vE.u((x = [<.z, w>.] ~R /\ y = [<.v, u>.] ~R ) /\ (z +P. u) <P (w +P. v))
36	9, 35	wa 240	. . 3 wff ((x e. R. /\ y e. R.) /\ E.zE.wE.vE.u((x = [<.z, w>.] ~R /\ y = [<.v, u>.] ~R ) /\ (z +P. u) <P (w +P. v)))
37	36, 2, 6	copab 3395	. 2 class {<.x, y>. | ((x e. R. /\ y e. R.) /\ E.zE.wE.vE.u((x = [<.z, w>.] ~R /\ y = [<.v, u>.] ~R ) /\ (z +P. u) <P (w +P. v)))}
38	1, 37	wceq 1298	1 wff <R = {<.x, y>. | ((x e. R. /\ y e. R.) /\ E.zE.wE.vE.u((x = [<.z, w>.] ~R /\ y = [<.v, u>.] ~R ) /\ (z +P. u) <P (w +P. v)))}

This definition is referenced by:  ltrelsr 6332  ltsrpr 6338

Copyright terms: Public domain