Theorem 0nnq 10821

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2111  ∀wral 3047  ∅c0 4282   class class class wbr 5093   × cxp 5617  ‘cfv 6487  2^nd c2nd 7926  Ncnpi 10741   <_N clti 10744   ~_Q ceq 10748  Qcnq 10749

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-opab 5156  df-xp 5625  df-nq 10809

This theorem is referenced by:  adderpq  10853  mulerpq  10854  addassnq  10855  mulassnq  10856  distrnq  10858  recmulnq  10861  recclnq  10863  ltanq  10868  ltmnq  10869  ltexnq  10872  nsmallnq  10874  ltbtwnnq  10875  ltrnq  10876  prlem934  10930  ltaddpr  10931  ltexprlem2  10934  ltexprlem3  10935  ltexprlem4  10936  ltexprlem6  10938  ltexprlem7  10939  prlem936  10944  reclem2pr  10945