Theorem 0nnq 10841

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114  ∀wral 3052  ∅c0 4274   class class class wbr 5086   × cxp 5623  ‘cfv 6493  2^nd c2nd 7935  Ncnpi 10761   <_N clti 10764   ~_Q ceq 10768  Qcnq 10769

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-opab 5149  df-xp 5631  df-nq 10829

This theorem is referenced by:  adderpq  10873  mulerpq  10874  addassnq  10875  mulassnq  10876  distrnq  10878  recmulnq  10881  recclnq  10883  ltanq  10888  ltmnq  10889  ltexnq  10892  nsmallnq  10894  ltbtwnnq  10895  ltrnq  10896  prlem934  10950  ltaddpr  10951  ltexprlem2  10954  ltexprlem3  10955  ltexprlem4  10956  ltexprlem6  10958  ltexprlem7  10959  prlem936  10964  reclem2pr  10965