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

Theorem 0nnq 8761
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 4869 . 2  |-  -.  (/)  e.  ( N.  X.  N. )
2 df-nq 8749 . . . 4  |-  Q.  =  { y  e.  ( N.  X.  N. )  |  A. x  e.  ( N.  X.  N. )
( y  ~Q  x  ->  -.  ( 2nd `  x
)  <N  ( 2nd `  y
) ) }
3 ssrab2 3392 . . . 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 3342 . . 3  |-  Q.  C_  ( N.  X.  N. )
54sseli 3308 . 2  |-  ( (/)  e.  Q.  ->  (/)  e.  ( N.  X.  N. )
)
61, 5mto 169 1  |-  -.  (/)  e.  Q.
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1721   A.wral 2670   {crab 2674   (/)c0 3592   class class class wbr 4176    X. cxp 4839   ` cfv 5417   2ndc2nd 6311   N.cnpi 8679    <N clti 8682    ~Q ceq 8686   Q.cnq 8687
This theorem is referenced by:  adderpq  8793  mulerpq  8794  addassnq  8795  mulassnq  8796  distrnq  8798  recmulnq  8801  recclnq  8803  ltanq  8808  ltmnq  8809  ltexnq  8812  nsmallnq  8814  ltbtwnnq  8815  ltrnq  8816  prlem934  8870  ltaddpr  8871  ltexprlem2  8874  ltexprlem3  8875  ltexprlem4  8876  ltexprlem6  8878  ltexprlem7  8879  prlem936  8884  reclem2pr  8885
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pr 4367
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-rab 2679  df-v 2922  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-opab 4231  df-xp 4847  df-nq 8749
  Copyright terms: Public domain W3C validator