This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )