Theorem elpqn 10870

Description: Each positive fraction is an ordered pair of positive integers (the numerator and denominator, in "lowest terms". (Contributed by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)

Assertion

Ref	Expression
elpqn	⊢ (𝐴 ∈ Q → 𝐴 ∈ (N × N))

Proof of Theorem elpqn

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-nq 10857	. . 3 ⊢ Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))}
2	1	ssrab3 4045	. 2 ⊢ Q ⊆ (N × N)
3	2	sseli 3943	1 ⊢ (𝐴 ∈ Q → 𝐴 ∈ (N × N))

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2106  ∀wral 3060   class class class wbr 5110   × cxp 5636  ‘cfv 6501  2^nd c2nd 7925  Ncnpi 10789   <_N clti 10792   ~_Q ceq 10796  Qcnq 10797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-in 3920  df-ss 3930  df-nq 10857

This theorem is referenced by:  nqereu  10874  nqerid  10878  enqeq  10879  addpqnq  10883  mulpqnq  10886  ordpinq  10888  addclnq  10890  mulclnq  10892  addnqf  10893  mulnqf  10894  adderpq  10901  mulerpq  10902  addassnq  10903  mulassnq  10904  distrnq  10906  mulidnq  10908  recmulnq  10909  ltsonq  10914  lterpq  10915  ltanq  10916  ltmnq  10917  ltexnq  10920  archnq  10925  wuncn  11115