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

Theorem 0nnq 9314
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 5033 . 2  |-  -.  (/)  e.  ( N.  X.  N. )
2 df-nq 9302 . . . 4  |-  Q.  =  { y  e.  ( N.  X.  N. )  |  A. x  e.  ( N.  X.  N. )
( y  ~Q  x  ->  -.  ( 2nd `  x
)  <N  ( 2nd `  y
) ) }
3 ssrab2 3590 . . . 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 3539 . . 3  |-  Q.  C_  ( N.  X.  N. )
54sseli 3505 . 2  |-  ( (/)  e.  Q.  ->  (/)  e.  ( N.  X.  N. )
)
61, 5mto 176 1  |-  -.  (/)  e.  Q.
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1767   A.wral 2817   {crab 2821   (/)c0 3790   class class class wbr 4453    X. cxp 5003   ` cfv 5594   2ndc2nd 6794   N.cnpi 9234    <N clti 9237    ~Q ceq 9241   Q.cnq 9242
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pr 4692
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-rab 2826  df-v 3120  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-sn 4034  df-pr 4036  df-op 4040  df-opab 4512  df-xp 5011  df-nq 9302
This theorem is referenced by:  adderpq  9346  mulerpq  9347  addassnq  9348  mulassnq  9349  distrnq  9351  recmulnq  9354  recclnq  9356  ltanq  9361  ltmnq  9362  ltexnq  9365  nsmallnq  9367  ltbtwnnq  9368  ltrnq  9369  prlem934  9423  ltaddpr  9424  ltexprlem2  9427  ltexprlem3  9428  ltexprlem4  9429  ltexprlem6  9431  ltexprlem7  9432  prlem936  9437  reclem2pr  9438
  Copyright terms: Public domain W3C validator