Theorem 0nnq 10835

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2113  ∀wral 3051  ∅c0 4285   class class class wbr 5098   × cxp 5622  ‘cfv 6492  2^nd c2nd 7932  Ncnpi 10755   <_N clti 10758   ~_Q ceq 10762  Qcnq 10763

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 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-opab 5161  df-xp 5630  df-nq 10823

This theorem is referenced by:  adderpq  10867  mulerpq  10868  addassnq  10869  mulassnq  10870  distrnq  10872  recmulnq  10875  recclnq  10877  ltanq  10882  ltmnq  10883  ltexnq  10886  nsmallnq  10888  ltbtwnnq  10889  ltrnq  10890  prlem934  10944  ltaddpr  10945  ltexprlem2  10948  ltexprlem3  10949  ltexprlem4  10950  ltexprlem6  10952  ltexprlem7  10953  prlem936  10958  reclem2pr  10959