Theorem 0nnq 10847

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.

Step	Hyp	Ref	Expression
1		0nelxp 5666	. 2 ⊢ ¬ ∅ ∈ (N × N)
2		df-nq 10835	. . . 4 ⊢ Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))}
3	2	ssrab3 4036	. . 3 ⊢ Q ⊆ (N × N)
4	3	sseli 3931	. 2 ⊢ (∅ ∈ Q → ∅ ∈ (N × N))
5	1, 4	mto 197	1 ⊢ ¬ ∅ ∈ Q

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114  ∀wral 3052  ∅c0 4287   class class class wbr 5100   × cxp 5630  ‘cfv 6500  2^nd c2nd 7942  Ncnpi 10767   <_N clti 10770   ~_Q ceq 10774  Qcnq 10775

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-opab 5163  df-xp 5638  df-nq 10835

This theorem is referenced by:  adderpq  10879  mulerpq  10880  addassnq  10881  mulassnq  10882  distrnq  10884  recmulnq  10887  recclnq  10889  ltanq  10894  ltmnq  10895  ltexnq  10898  nsmallnq  10900  ltbtwnnq  10901  ltrnq  10902  prlem934  10956  ltaddpr  10957  ltexprlem2  10960  ltexprlem3  10961  ltexprlem4  10962  ltexprlem6  10964  ltexprlem7  10965  prlem936  10970  reclem2pr  10971