MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ltpq Unicode version

Definition df-ltpq 8467
Description: Define pre-ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8676, 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.)
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
StepHypRef Expression
1 cltpq 8405 . 2  class  <pQ
2 vx . . . . . . 7  set  x
32cv 1618 . . . . . 6  class  x
4 cnpi 8399 . . . . . . 7  class  N.
54, 4cxp 4624 . . . . . 6  class  ( N. 
X.  N. )
63, 5wcel 1621 . . . . 5  wff  x  e.  ( N.  X.  N. )
7 vy . . . . . . 7  set  y
87cv 1618 . . . . . 6  class  y
98, 5wcel 1621 . . . . 5  wff  y  e.  ( N.  X.  N. )
106, 9wa 360 . . . 4  wff  ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )
11 c1st 6019 . . . . . . 7  class  1st
123, 11cfv 4638 . . . . . 6  class  ( 1st `  x )
13 c2nd 6020 . . . . . . 7  class  2nd
148, 13cfv 4638 . . . . . 6  class  ( 2nd `  y )
15 cmi 8401 . . . . . 6  class  .N
1612, 14, 15co 5757 . . . . 5  class  ( ( 1st `  x )  .N  ( 2nd `  y
) )
178, 11cfv 4638 . . . . . 6  class  ( 1st `  y )
183, 13cfv 4638 . . . . . 6  class  ( 2nd `  x )
1917, 18, 15co 5757 . . . . 5  class  ( ( 1st `  y )  .N  ( 2nd `  x
) )
20 clti 8402 . . . . 5  class  <N
2116, 19, 20wbr 3963 . . . 4  wff  ( ( 1st `  x )  .N  ( 2nd `  y
) )  <N  (
( 1st `  y
)  .N  ( 2nd `  x ) )
2210, 21wa 360 . . 3  wff  ( ( x  e.  ( N. 
X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  (
( 1st `  x
)  .N  ( 2nd `  y ) )  <N 
( ( 1st `  y
)  .N  ( 2nd `  x ) ) )
2322, 2, 7copab 4016 . 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 ) ) ) }
241, 23wceq 1619 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 ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  ordpipq  8499  lterpq  8527
  Copyright terms: Public domain W3C validator