Definition df-ltnqqs 7437

Description: Define ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. Similar to Definition 5 of [Suppes] p. 162. (Contributed by NM, 13-Feb-1996.)

Assertion

Ref	Expression
df-ltnqqs	|- <Q = { <. x , y >. | ( ( x e. Q. /\ y e. Q. ) /\ E. z E. w E. v E. 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-ltnqqs

Step	Hyp	Ref	Expression
1		cltq 7369	. 2 class <Q
2		vx	. . . . . . 7 setvar x
3	2	cv 1363	. . . . . 6 class x
4		cnq 7364	. . . . . 6 class Q.
5	3, 4	wcel 2167	. . . . 5 wff x e. Q.
6		vy	. . . . . . 7 setvar y
7	6	cv 1363	. . . . . 6 class y
8	7, 4	wcel 2167	. . . . 5 wff y e. Q.
9	5, 8	wa 104	. . . 4 wff ( x e. Q. /\ y e. Q. )
10		vz	. . . . . . . . . . . . . 14 setvar z
11	10	cv 1363	. . . . . . . . . . . . 13 class z
12		vw	. . . . . . . . . . . . . 14 setvar w
13	12	cv 1363	. . . . . . . . . . . . 13 class w
14	11, 13	cop 3626	. . . . . . . . . . . 12 class <. z , w >.
15		ceq 7363	. . . . . . . . . . . 12 class ~Q
16	14, 15	cec 6599	. . . . . . . . . . 11 class [ <. z , w >. ] ~Q
17	3, 16	wceq 1364	. . . . . . . . . 10 wff x = [ <. z , w >. ] ~Q
18		vv	. . . . . . . . . . . . . 14 setvar v
19	18	cv 1363	. . . . . . . . . . . . 13 class v
20		vu	. . . . . . . . . . . . . 14 setvar u
21	20	cv 1363	. . . . . . . . . . . . 13 class u
22	19, 21	cop 3626	. . . . . . . . . . . 12 class <. v , u >.
23	22, 15	cec 6599	. . . . . . . . . . 11 class [ <. v , u >. ] ~Q
24	7, 23	wceq 1364	. . . . . . . . . 10 wff y = [ <. v , u >. ] ~Q
25	17, 24	wa 104	. . . . . . . . 9 wff ( x = [ <. z , w >. ] ~Q /\ y = [ <. v , u >. ] ~Q )
26		cmi 7358	. . . . . . . . . . 11 class .N
27	11, 21, 26	co 5925	. . . . . . . . . 10 class ( z .N u )
28	13, 19, 26	co 5925	. . . . . . . . . 10 class ( w .N v )
29		clti 7359	. . . . . . . . . 10 class <N
30	27, 28, 29	wbr 4034	. . . . . . . . 9 wff ( z .N u ) <N ( w .N v )
31	25, 30	wa 104	. . . . . . . 8 wff ( ( x = [ <. z , w >. ] ~Q /\ y = [ <. v , u >. ] ~Q ) /\ ( z .N u ) <N ( w .N v ) )
32	31, 20	wex 1506	. . . . . . 7 wff E. u ( ( x = [ <. z , w >. ] ~Q /\ y = [ <. v , u >. ] ~Q ) /\ ( z .N u ) <N ( w .N v ) )
33	32, 18	wex 1506	. . . . . 6 wff E. v E. u ( ( x = [ <. z , w >. ] ~Q /\ y = [ <. v , u >. ] ~Q ) /\ ( z .N u ) <N ( w .N v ) )
34	33, 12	wex 1506	. . . . 5 wff E. w E. v E. u ( ( x = [ <. z , w >. ] ~Q /\ y = [ <. v , u >. ] ~Q ) /\ ( z .N u ) <N ( w .N v ) )
35	34, 10	wex 1506	. . . 4 wff E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~Q /\ y = [ <. v , u >. ] ~Q ) /\ ( z .N u ) <N ( w .N v ) )
36	9, 35	wa 104	. . 3 wff ( ( x e. Q. /\ y e. Q. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~Q /\ y = [ <. v , u >. ] ~Q ) /\ ( z .N u ) <N ( w .N v ) ) )
37	36, 2, 6	copab 4094	. 2 class { <. x , y >. | ( ( x e. Q. /\ y e. Q. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~Q /\ y = [ <. v , u >. ] ~Q ) /\ ( z .N u ) <N ( w .N v ) ) ) }
38	1, 37	wceq 1364	1 wff <Q = { <. x , y >. | ( ( x e. Q. /\ y e. Q. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~Q /\ y = [ <. v , u >. ] ~Q ) /\ ( z .N u ) <N ( w .N v ) ) ) }

This definition is referenced by:  ltrelnq  7449  ordpipqqs  7458