Definition df-ltpq 7287

Description: Define pre-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, 28-Aug-1995.)

Assertion

Ref	Expression
df-ltpq	|- <pQ = { <. x , y >. | ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) ) <N ( ( 1st ` y ) .N ( 2nd ` x ) ) ) }

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-ltpq

Step	Hyp	Ref	Expression
1		cltpq 7219	. 2 class <pQ
2		vx	. . . . . . 7 setvar x
3	2	cv 1342	. . . . . 6 class x
4		cnpi 7213	. . . . . . 7 class N.
5	4, 4	cxp 4602	. . . . . 6 class ( N. X. N. )
6	3, 5	wcel 2136	. . . . 5 wff x e. ( N. X. N. )
7		vy	. . . . . . 7 setvar y
8	7	cv 1342	. . . . . 6 class y
9	8, 5	wcel 2136	. . . . 5 wff y e. ( N. X. N. )
10	6, 9	wa 103	. . . 4 wff ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) )
11		c1st 6106	. . . . . . 7 class 1st
12	3, 11	cfv 5188	. . . . . 6 class ( 1st ` x )
13		c2nd 6107	. . . . . . 7 class 2nd
14	8, 13	cfv 5188	. . . . . 6 class ( 2nd ` y )
15		cmi 7215	. . . . . 6 class .N
16	12, 14, 15	co 5842	. . . . 5 class ( ( 1st ` x ) .N ( 2nd ` y ) )
17	8, 11	cfv 5188	. . . . . 6 class ( 1st ` y )
18	3, 13	cfv 5188	. . . . . 6 class ( 2nd ` x )
19	17, 18, 15	co 5842	. . . . 5 class ( ( 1st ` y ) .N ( 2nd ` x ) )
20		clti 7216	. . . . 5 class <N
21	16, 19, 20	wbr 3982	. . . 4 wff ( ( 1st ` x ) .N ( 2nd ` y ) ) <N ( ( 1st ` y ) .N ( 2nd ` x ) )
22	10, 21	wa 103	. . 3 wff ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) ) <N ( ( 1st ` y ) .N ( 2nd ` x ) ) )
23	22, 2, 7	copab 4042	. 2 class { <. x , y >. | ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) ) <N ( ( 1st ` y ) .N ( 2nd ` x ) ) ) }
24	1, 23	wceq 1343	1 wff <pQ = { <. x , y >. | ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) ) <N ( ( 1st ` y ) .N ( 2nd ` x ) ) ) }

This definition is referenced by: (None)