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

Theorem 0nnq 8548
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 4717 . 2  |-  -.  (/)  e.  ( N.  X.  N. )
2 df-nq 8536 . . . 4  |-  Q.  =  { y  e.  ( N.  X.  N. )  |  A. x  e.  ( N.  X.  N. )
( y  ~Q  x  ->  -.  ( 2nd `  x
)  <N  ( 2nd `  y
) ) }
3 ssrab2 3258 . . . 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 3208 . . 3  |-  Q.  C_  ( N.  X.  N. )
54sseli 3176 . 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 1684   A.wral 2543   {crab 2547   (/)c0 3455   class class class wbr 4023    X. cxp 4687   ` cfv 5255   2ndc2nd 6121   N.cnpi 8466    <N clti 8469    ~Q ceq 8473   Q.cnq 8474
This theorem is referenced by:  adderpq  8580  mulerpq  8581  addassnq  8582  mulassnq  8583  distrnq  8585  recmulnq  8588  recclnq  8590  ltanq  8595  ltmnq  8596  ltexnq  8599  nsmallnq  8601  ltbtwnnq  8602  ltrnq  8603  prlem934  8657  ltaddpr  8658  ltexprlem2  8661  ltexprlem3  8662  ltexprlem4  8663  ltexprlem6  8665  ltexprlem7  8666  prlem936  8671  reclem2pr  8672
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-opab 4078  df-xp 4695  df-nq 8536
  Copyright terms: Public domain W3C validator