Theorem 0nnq 10611

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108  ∀wral 3063  ∅c0 4253   class class class wbr 5070   × cxp 5578  ‘cfv 6418  2^nd c2nd 7803  Ncnpi 10531   <_N clti 10534   ~_Q ceq 10538  Qcnq 10539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-opab 5133  df-xp 5586  df-nq 10599

This theorem is referenced by:  adderpq  10643  mulerpq  10644  addassnq  10645  mulassnq  10646  distrnq  10648  recmulnq  10651  recclnq  10653  ltanq  10658  ltmnq  10659  ltexnq  10662  nsmallnq  10664  ltbtwnnq  10665  ltrnq  10666  prlem934  10720  ltaddpr  10721  ltexprlem2  10724  ltexprlem3  10725  ltexprlem4  10726  ltexprlem6  10728  ltexprlem7  10729  prlem936  10734  reclem2pr  10735