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

Theorem 0nnq 10901
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 ¬ ∅ ∈ Q

Proof of Theorem 0nnq
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0nelxp 5703 . 2 ¬ ∅ ∈ (N × N)
2 df-nq 10889 . . . 4 Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd𝑥) <N (2nd𝑦))}
32ssrab3 4076 . . 3 Q ⊆ (N × N)
43sseli 3974 . 2 (∅ ∈ Q → ∅ ∈ (N × N))
51, 4mto 196 1 ¬ ∅ ∈ Q
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2106  wral 3060  c0 4318   class class class wbr 5141   × cxp 5667  cfv 6532  2nd c2nd 7956  Ncnpi 10821   <N clti 10824   ~Q ceq 10828  Qcnq 10829
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-opab 5204  df-xp 5675  df-nq 10889
This theorem is referenced by:  adderpq  10933  mulerpq  10934  addassnq  10935  mulassnq  10936  distrnq  10938  recmulnq  10941  recclnq  10943  ltanq  10948  ltmnq  10949  ltexnq  10952  nsmallnq  10954  ltbtwnnq  10955  ltrnq  10956  prlem934  11010  ltaddpr  11011  ltexprlem2  11014  ltexprlem3  11015  ltexprlem4  11016  ltexprlem6  11018  ltexprlem7  11019  prlem936  11024  reclem2pr  11025
  Copyright terms: Public domain W3C validator