Theorem elpqn 10681

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 10668	. . 3 ⊢ Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))}
2	1	ssrab3 4015	. 2 ⊢ Q ⊆ (N × N)
3	2	sseli 3917	1 ⊢ (𝐴 ∈ Q → 𝐴 ∈ (N × N))

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2106  ∀wral 3064   class class class wbr 5074   × cxp 5587  ‘cfv 6433  2^nd c2nd 7830  Ncnpi 10600   <_N clti 10603   ~_Q ceq 10607  Qcnq 10608

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904  df-nq 10668

This theorem is referenced by:  nqereu  10685  nqerid  10689  enqeq  10690  addpqnq  10694  mulpqnq  10697  ordpinq  10699  addclnq  10701  mulclnq  10703  addnqf  10704  mulnqf  10705  adderpq  10712  mulerpq  10713  addassnq  10714  mulassnq  10715  distrnq  10717  mulidnq  10719  recmulnq  10720  ltsonq  10725  lterpq  10726  ltanq  10727  ltmnq  10728  ltexnq  10731  archnq  10736  wuncn  10926