Theorem 0nnq 10818

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109  ∀wral 3044  ∅c0 4284   class class class wbr 5092   × cxp 5617  ‘cfv 6482  2^nd c2nd 7923  Ncnpi 10738   <_N clti 10741   ~_Q ceq 10745  Qcnq 10746

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-opab 5155  df-xp 5625  df-nq 10806

This theorem is referenced by:  adderpq  10850  mulerpq  10851  addassnq  10852  mulassnq  10853  distrnq  10855  recmulnq  10858  recclnq  10860  ltanq  10865  ltmnq  10866  ltexnq  10869  nsmallnq  10871  ltbtwnnq  10872  ltrnq  10873  prlem934  10927  ltaddpr  10928  ltexprlem2  10931  ltexprlem3  10932  ltexprlem4  10933  ltexprlem6  10935  ltexprlem7  10936  prlem936  10941  reclem2pr  10942