Theorem 0nnq 11009

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2145  ∀wral 3077  ∅c0 4279   class class class wbr 5103   × cxp 5649  ‘cfv 6538  2^nd c2nd 8000  Ncnpi 10929   <_N clti 10932   ~_Q ceq 10936  Qcnq 10937

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-opab 5168  df-xp 5657  df-nq 10997

This theorem is used by:  adderpq  11041  mulerpq  11042  addassnq  11043  mulassnq  11044  distrnq  11046  recmulnq  11049  recclnq  11051  ltanq  11056  ltmnq  11057  ltexnq  11060  nsmallnq  11062  ltbtwnnq  11063  ltrnq  11064  prlem934  11118  ltaddpr  11119  ltexprlem2  11122  ltexprlem3  11123  ltexprlem4  11124  ltexprlem6  11126  ltexprlem7  11127  prlem936  11132  reclem2pr  11133