Theorem 0nnq 10925

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2105  ∀wral 3060  ∅c0 4322   class class class wbr 5148   × cxp 5674  ‘cfv 6543  2^nd c2nd 7978  Ncnpi 10845   <_N clti 10848   ~_Q ceq 10852  Qcnq 10853

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-opab 5211  df-xp 5682  df-nq 10913

This theorem is referenced by:  adderpq  10957  mulerpq  10958  addassnq  10959  mulassnq  10960  distrnq  10962  recmulnq  10965  recclnq  10967  ltanq  10972  ltmnq  10973  ltexnq  10976  nsmallnq  10978  ltbtwnnq  10979  ltrnq  10980  prlem934  11034  ltaddpr  11035  ltexprlem2  11038  ltexprlem3  11039  ltexprlem4  11040  ltexprlem6  11042  ltexprlem7  11043  prlem936  11048  reclem2pr  11049