Theorem 0nnq 10909

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2149  ∀wral 3085  ∅c0 4294   class class class wbr 5113   × cxp 5660  ‘cfv 6537  2^nd c2nd 7985  Ncnpi 10829   <_N clti 10832   ~_Q ceq 10836  Qcnq 10837

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-opab 5178  df-xp 5668  df-nq 10897

This theorem is referenced by:  adderpq  10941  mulerpq  10942  addassnq  10943  mulassnq  10944  distrnq  10946  recmulnq  10949  recclnq  10951  ltanq  10956  ltmnq  10957  ltexnq  10960  nsmallnq  10962  ltbtwnnq  10963  ltrnq  10964  prlem934  11018  ltaddpr  11019  ltexprlem2  11022  ltexprlem3  11023  ltexprlem4  11024  ltexprlem6  11026  ltexprlem7  11027  prlem936  11032  reclem2pr  11033