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

Theorem 0nnq 9375
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 4881 . 2  |-  -.  (/)  e.  ( N.  X.  N. )
2 df-nq 9363 . . . 4  |-  Q.  =  { y  e.  ( N.  X.  N. )  |  A. x  e.  ( N.  X.  N. )
( y  ~Q  x  ->  -.  ( 2nd `  x
)  <N  ( 2nd `  y
) ) }
3 ssrab2 3526 . . . 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 3474 . . 3  |-  Q.  C_  ( N.  X.  N. )
54sseli 3440 . 2  |-  ( (/)  e.  Q.  ->  (/)  e.  ( N.  X.  N. )
)
61, 5mto 181 1  |-  -.  (/)  e.  Q.
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1898   A.wral 2749   {crab 2753   (/)c0 3743   class class class wbr 4416    X. cxp 4851   ` cfv 5601   2ndc2nd 6819   N.cnpi 9295    <N clti 9298    ~Q ceq 9302   Q.cnq 9303
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-opab 4476  df-xp 4859  df-nq 9363
This theorem is referenced by:  adderpq  9407  mulerpq  9408  addassnq  9409  mulassnq  9410  distrnq  9412  recmulnq  9415  recclnq  9417  ltanq  9422  ltmnq  9423  ltexnq  9426  nsmallnq  9428  ltbtwnnq  9429  ltrnq  9430  prlem934  9484  ltaddpr  9485  ltexprlem2  9488  ltexprlem3  9489  ltexprlem4  9490  ltexprlem6  9492  ltexprlem7  9493  prlem936  9498  reclem2pr  9499
  Copyright terms: Public domain W3C validator