Theorem 0nnq 10838

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2119  ∀wral 3053  ∅c0 4261   class class class wbr 5072   × cxp 5616  ‘cfv 6485  2^nd c2nd 7930  Ncnpi 10758   <_N clti 10761   ~_Q ceq 10765  Qcnq 10766

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-opab 5135  df-xp 5624  df-nq 10826

This theorem is referenced by:  adderpq  10870  mulerpq  10871  addassnq  10872  mulassnq  10873  distrnq  10875  recmulnq  10878  recclnq  10880  ltanq  10885  ltmnq  10886  ltexnq  10889  nsmallnq  10891  ltbtwnnq  10892  ltrnq  10893  prlem934  10947  ltaddpr  10948  ltexprlem2  10951  ltexprlem3  10952  ltexprlem4  10953  ltexprlem6  10955  ltexprlem7  10956  prlem936  10961  reclem2pr  10962