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.

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2106  ∀wral 3060  ∅c0 4318   class class class wbr 5141   × cxp 5667  ‘cfv 6532  2^nd 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