MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0nnq Unicode version

Theorem 0nnq 8638
Description: The empty set is not a positive fraction. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.) (New usage is discouraged.)
Assertion
Ref Expression
0nnq  |-  -.  (/)  e.  Q.

Proof of Theorem 0nnq
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0nelxp 4799 . 2  |-  -.  (/)  e.  ( N.  X.  N. )
2 df-nq 8626 . . . 4  |-  Q.  =  { y  e.  ( N.  X.  N. )  |  A. x  e.  ( N.  X.  N. )
( y  ~Q  x  ->  -.  ( 2nd `  x
)  <N  ( 2nd `  y
) ) }
3 ssrab2 3334 . . . 4  |-  { y  e.  ( N.  X.  N. )  |  A. x  e.  ( N.  X.  N. ) ( y  ~Q  x  ->  -.  ( 2nd `  x ) 
<N  ( 2nd `  y
) ) }  C_  ( N.  X.  N. )
42, 3eqsstri 3284 . . 3  |-  Q.  C_  ( N.  X.  N. )
54sseli 3252 . 2  |-  ( (/)  e.  Q.  ->  (/)  e.  ( N.  X.  N. )
)
61, 5mto 167 1  |-  -.  (/)  e.  Q.
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1710   A.wral 2619   {crab 2623   (/)c0 3531   class class class wbr 4104    X. cxp 4769   ` cfv 5337   2ndc2nd 6208   N.cnpi 8556    <N clti 8559    ~Q ceq 8563   Q.cnq 8564
This theorem is referenced by:  adderpq  8670  mulerpq  8671  addassnq  8672  mulassnq  8673  distrnq  8675  recmulnq  8678  recclnq  8680  ltanq  8685  ltmnq  8686  ltexnq  8689  nsmallnq  8691  ltbtwnnq  8692  ltrnq  8693  prlem934  8747  ltaddpr  8748  ltexprlem2  8751  ltexprlem3  8752  ltexprlem4  8753  ltexprlem6  8755  ltexprlem7  8756  prlem936  8761  reclem2pr  8762
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pr 4295
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-opab 4159  df-xp 4777  df-nq 8626
  Copyright terms: Public domain W3C validator