Definition df-ltpq

Description: Define pre-ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. Similar to Definition 5 of Suppes p. 162. (Contributed by NM, 28-Aug-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	df-ltpq	|- . | ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cltpq	|-
1		vx	|- x
2		vy	|- y
3	1	cv	|- x
4		cnpi	|- N.
5	4 4	cxp	|- ( N. X. N. )
6	3 5	wcel	|- x e. ( N. X. N. )
7	2	cv	|- y
8	7 5	wcel	|- y e. ( N. X. N. )
9	6 8	wa	|- ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) )
10		c1st	|- 1st
11	3 10	cfv	|- ( 1st ` x )
12		cmi	|- .N
13		c2nd	|- 2nd
14	7 13	cfv	|- ( 2nd ` y )
15	11 14 12	co	|- ( ( 1st ` x ) .N ( 2nd ` y ) )
16		clti	|-
17	7 10	cfv	|- ( 1st ` y )
18	3 13	cfv	|- ( 2nd ` x )
19	17 18 12	co	|- ( ( 1st ` y ) .N ( 2nd ` x ) )
20	15 19 16	wbr	|- ( ( 1st ` x ) .N ( 2nd ` y ) )
21	9 20	wa	|- ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) )
22	21 1 2	copab	|- { <. x , y >. | ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) )
23	0 22	wceq	|- . | ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) )