Definition df-ltq 6560

Description: Define ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 6758, and is intended to be used only by the construction. Similar to Definition 5 of [Suppes] p. 162.

Assertion

Ref	Expression
df-ltq	|- <Q = {<.x, y>. | ((x e. Q. /\ y e. Q.) /\ E.zE.wE.vE.u((x = [<.z, w>.] ~Q /\ y = [<.v, u>.] ~Q ) /\ (z .N u) <N (w .N v)))}

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

Detailed syntax breakdown of Definition df-ltq

Step	Hyp	Ref	Expression
1		cltq 6502	. 2 class <Q
2		vx	. . . . . . 7 set x
3	2	cv 1585	. . . . . 6 class x
4		cnq 6497	. . . . . 6 class Q.
5	3, 4	wcel 1588	. . . . 5 wff x e. Q.
6		vy	. . . . . . 7 set y
7	6	cv 1585	. . . . . 6 class y
8	7, 4	wcel 1588	. . . . 5 wff y e. Q.
9	5, 8	wa 337	. . . 4 wff (x e. Q. /\ y e. Q.)
10		vz	. . . . . . . . . . . . . 14 set z
11	10	cv 1585	. . . . . . . . . . . . 13 class z
12		vw	. . . . . . . . . . . . . 14 set w
13	12	cv 1585	. . . . . . . . . . . . 13 class w
14	11, 13	cop 3240	. . . . . . . . . . . 12 class <.z, w>.
15		ceq 6496	. . . . . . . . . . . 12 class ~Q
16	14, 15	cec 5477	. . . . . . . . . . 11 class [<.z, w>.] ~Q
17	3, 16	wceq 1586	. . . . . . . . . 10 wff x = [<.z, w>.] ~Q
18		vv	. . . . . . . . . . . . . 14 set v
19	18	cv 1585	. . . . . . . . . . . . 13 class v
20		vu	. . . . . . . . . . . . . 14 set u
21	20	cv 1585	. . . . . . . . . . . . 13 class u
22	19, 21	cop 3240	. . . . . . . . . . . 12 class <.v, u>.
23	22, 15	cec 5477	. . . . . . . . . . 11 class [<.v, u>.] ~Q
24	7, 23	wceq 1586	. . . . . . . . . 10 wff y = [<.v, u>.] ~Q
25	17, 24	wa 337	. . . . . . . . 9 wff (x = [<.z, w>.] ~Q /\ y = [<.v, u>.] ~Q )
26		cmi 6492	. . . . . . . . . . 11 class .N
27	11, 21, 26	co 4981	. . . . . . . . . 10 class (z .N u)
28	13, 19, 26	co 4981	. . . . . . . . . 10 class (w .N v)
29		clti 6493	. . . . . . . . . 10 class <N
30	27, 28, 29	wbr 3507	. . . . . . . . 9 wff (z .N u) <N (w .N v)
31	25, 30	wa 337	. . . . . . . 8 wff ((x = [<.z, w>.] ~Q /\ y = [<.v, u>.] ~Q ) /\ (z .N u) <N (w .N v))
32	31, 20	wex 1615	. . . . . . 7 wff E.u((x = [<.z, w>.] ~Q /\ y = [<.v, u>.] ~Q ) /\ (z .N u) <N (w .N v))
33	32, 18	wex 1615	. . . . . 6 wff E.vE.u((x = [<.z, w>.] ~Q /\ y = [<.v, u>.] ~Q ) /\ (z .N u) <N (w .N v))
34	33, 12	wex 1615	. . . . 5 wff E.wE.vE.u((x = [<.z, w>.] ~Q /\ y = [<.v, u>.] ~Q ) /\ (z .N u) <N (w .N v))
35	34, 10	wex 1615	. . . 4 wff E.zE.wE.vE.u((x = [<.z, w>.] ~Q /\ y = [<.v, u>.] ~Q ) /\ (z .N u) <N (w .N v))
36	9, 35	wa 337	. . 3 wff ((x e. Q. /\ y e. Q.) /\ E.zE.wE.vE.u((x = [<.z, w>.] ~Q /\ y = [<.v, u>.] ~Q ) /\ (z .N u) <N (w .N v)))
37	36, 2, 6	copab 3565	. 2 class {<.x, y>. | ((x e. Q. /\ y e. Q.) /\ E.zE.wE.vE.u((x = [<.z, w>.] ~Q /\ y = [<.v, u>.] ~Q ) /\ (z .N u) <N (w .N v)))}
38	1, 37	wceq 1586	1 wff <Q = {<.x, y>. | ((x e. Q. /\ y e. Q.) /\ E.zE.wE.vE.u((x = [<.z, w>.] ~Q /\ y = [<.v, u>.] ~Q ) /\ (z .N u) <N (w .N v)))}

This definition is referenced by:  ltrelpq 6569  ordpipq 6574

Copyright terms: Public domain