Theorem 0nnq 10833

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2113  ∀wral 3049  ∅c0 4283   class class class wbr 5096   × cxp 5620  ‘cfv 6490  2^nd c2nd 7930  Ncnpi 10753   <_N clti 10756   ~_Q ceq 10760  Qcnq 10761

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-opab 5159  df-xp 5628  df-nq 10821

This theorem is referenced by:  adderpq  10865  mulerpq  10866  addassnq  10867  mulassnq  10868  distrnq  10870  recmulnq  10873  recclnq  10875  ltanq  10880  ltmnq  10881  ltexnq  10884  nsmallnq  10886  ltbtwnnq  10887  ltrnq  10888  prlem934  10942  ltaddpr  10943  ltexprlem2  10946  ltexprlem3  10947  ltexprlem4  10948  ltexprlem6  10950  ltexprlem7  10951  prlem936  10956  reclem2pr  10957