Theorem 0nnq 10904

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2143  ∀wral 3079  ∅c0 4286   class class class wbr 5109   × cxp 5659  ‘cfv 6536  2^nd c2nd 7981  Ncnpi 10824   <_N clti 10827   ~_Q ceq 10831  Qcnq 10832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-opab 5174  df-xp 5667  df-nq 10892

This theorem is referenced by:  adderpq  10936  mulerpq  10937  addassnq  10938  mulassnq  10939  distrnq  10941  recmulnq  10944  recclnq  10946  ltanq  10951  ltmnq  10952  ltexnq  10955  nsmallnq  10957  ltbtwnnq  10958  ltrnq  10959  prlem934  11013  ltaddpr  11014  ltexprlem2  11017  ltexprlem3  11018  ltexprlem4  11019  ltexprlem6  11021  ltexprlem7  11022  prlem936  11027  reclem2pr  11028