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

Definition df-nq 8504
Description: Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8711, and is intended to be used only by the construction. From Proposition 9-2.2 of [Gleason] p. 117. (Contributed by NM, 16-Aug-1995.) (New usage is discouraged.)
Assertion
Ref Expression
df-nq  |-  Q.  =  { x  e.  ( N.  X.  N. )  | 
A. y  e.  ( N.  X.  N. )
( x  ~Q  y  ->  -.  ( 2nd `  y
)  <N  ( 2nd `  x
) ) }
Distinct variable group:    x, y

Detailed syntax breakdown of Definition df-nq
StepHypRef Expression
1 cnq 8442 . 2  class  Q.
2 vx . . . . . . 7  set  x
32cv 1618 . . . . . 6  class  x
4 vy . . . . . . 7  set  y
54cv 1618 . . . . . 6  class  y
6 ceq 8441 . . . . . 6  class  ~Q
73, 5, 6wbr 3997 . . . . 5  wff  x  ~Q  y
8 c2nd 6055 . . . . . . . 8  class  2nd
95, 8cfv 4673 . . . . . . 7  class  ( 2nd `  y )
103, 8cfv 4673 . . . . . . 7  class  ( 2nd `  x )
11 clti 8437 . . . . . . 7  class  <N
129, 10, 11wbr 3997 . . . . . 6  wff  ( 2nd `  y )  <N  ( 2nd `  x )
1312wn 5 . . . . 5  wff  -.  ( 2nd `  y )  <N 
( 2nd `  x
)
147, 13wi 6 . . . 4  wff  ( x  ~Q  y  ->  -.  ( 2nd `  y ) 
<N  ( 2nd `  x
) )
15 cnpi 8434 . . . . 5  class  N.
1615, 15cxp 4659 . . . 4  class  ( N. 
X.  N. )
1714, 4, 16wral 2518 . . 3  wff  A. y  e.  ( N.  X.  N. ) ( x  ~Q  y  ->  -.  ( 2nd `  y )  <N  ( 2nd `  x ) )
1817, 2, 16crab 2522 . 2  class  { x  e.  ( N.  X.  N. )  |  A. y  e.  ( N.  X.  N. ) ( x  ~Q  y  ->  -.  ( 2nd `  y )  <N  ( 2nd `  x ) ) }
191, 18wceq 1619 1  wff  Q.  =  { x  e.  ( N.  X.  N. )  | 
A. y  e.  ( N.  X.  N. )
( x  ~Q  y  ->  -.  ( 2nd `  y
)  <N  ( 2nd `  x
) ) }
Colors of variables: wff set class
This definition is referenced by:  nqex  8515  0nnq  8516  elpqn  8517  pinq  8519  nqereu  8521
  Copyright terms: Public domain W3C validator