Theorem 0nnq 11019

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2146  ∀wral 3079  ∅c0 4280   class class class wbr 5105   × cxp 5652  ‘cfv 6546  2^nd c2nd 8007  Ncnpi 10939   <_N clti 10942   ~_Q ceq 10946  Qcnq 10947

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5251  ax-pr 5394

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-opab 5170  df-xp 5660  df-nq 11007

This theorem is used by:  adderpq  11051  mulerpq  11052  addassnq  11053  mulassnq  11054  distrnq  11056  recmulnq  11059  recclnq  11061  ltanq  11066  ltmnq  11067  ltexnq  11070  nsmallnq  11072  ltbtwnnq  11073  ltrnq  11074  prlem934  11128  ltaddpr  11129  ltexprlem2  11132  ltexprlem3  11133  ltexprlem4  11134  ltexprlem6  11136  ltexprlem7  11137  prlem936  11142  reclem2pr  11143