Theorem 0nnq 10680

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 5623	. 2 ⊢ ¬ ∅ ∈ (N × N)
2		df-nq 10668	. . . 4 ⊢ Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))}
3	2	ssrab3 4015	. . 3 ⊢ Q ⊆ (N × N)
4	3	sseli 3917	. 2 ⊢ (∅ ∈ Q → ∅ ∈ (N × N))
5	1, 4	mto 196	1 ⊢ ¬ ∅ ∈ Q

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2106  ∀wral 3064  ∅c0 4256   class class class wbr 5074   × cxp 5587  ‘cfv 6433  2^nd c2nd 7830  Ncnpi 10600   <_N clti 10603   ~_Q ceq 10607  Qcnq 10608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-opab 5137  df-xp 5595  df-nq 10668

This theorem is referenced by:  adderpq  10712  mulerpq  10713  addassnq  10714  mulassnq  10715  distrnq  10717  recmulnq  10720  recclnq  10722  ltanq  10727  ltmnq  10728  ltexnq  10731  nsmallnq  10733  ltbtwnnq  10734  ltrnq  10735  prlem934  10789  ltaddpr  10790  ltexprlem2  10793  ltexprlem3  10794  ltexprlem4  10795  ltexprlem6  10797  ltexprlem7  10798  prlem936  10803  reclem2pr  10804