Theorem 0nnq 10877

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109  ∀wral 3044  ∅c0 4296   class class class wbr 5107   × cxp 5636  ‘cfv 6511  2^nd c2nd 7967  Ncnpi 10797   <_N clti 10800   ~_Q ceq 10804  Qcnq 10805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-opab 5170  df-xp 5644  df-nq 10865

This theorem is referenced by:  adderpq  10909  mulerpq  10910  addassnq  10911  mulassnq  10912  distrnq  10914  recmulnq  10917  recclnq  10919  ltanq  10924  ltmnq  10925  ltexnq  10928  nsmallnq  10930  ltbtwnnq  10931  ltrnq  10932  prlem934  10986  ltaddpr  10987  ltexprlem2  10990  ltexprlem3  10991  ltexprlem4  10992  ltexprlem6  10994  ltexprlem7  10995  prlem936  11000  reclem2pr  11001