Definition df-ltpq 7413

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 7345	. 2 class <pQ
2		vx	. . . . . . 7 setvar x
3	2	cv 1363	. . . . . 6 class x
4		cnpi 7339	. . . . . . 7 class N.
5	4, 4	cxp 4661	. . . . . 6 class ( N. X. N. )
6	3, 5	wcel 2167	. . . . 5 wff x e. ( N. X. N. )
7		vy	. . . . . . 7 setvar y
8	7	cv 1363	. . . . . 6 class y
9	8, 5	wcel 2167	. . . . 5 wff y e. ( N. X. N. )
10	6, 9	wa 104	. . . 4 wff ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) )
11		c1st 6196	. . . . . . 7 class 1st
12	3, 11	cfv 5258	. . . . . 6 class ( 1st ` x )
13		c2nd 6197	. . . . . . 7 class 2nd
14	8, 13	cfv 5258	. . . . . 6 class ( 2nd ` y )
15		cmi 7341	. . . . . 6 class .N
16	12, 14, 15	co 5922	. . . . 5 class ( ( 1st ` x ) .N ( 2nd ` y ) )
17	8, 11	cfv 5258	. . . . . 6 class ( 1st ` y )
18	3, 13	cfv 5258	. . . . . 6 class ( 2nd ` x )
19	17, 18, 15	co 5922	. . . . 5 class ( ( 1st ` y ) .N ( 2nd ` x ) )
20		clti 7342	. . . . 5 class <N
21	16, 19, 20	wbr 4033	. . . 4 wff ( ( 1st ` x ) .N ( 2nd ` y ) ) <N ( ( 1st ` y ) .N ( 2nd ` x ) )
22	10, 21	wa 104	. . 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 4093	. 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 1364	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)