Theorem elpqn 10336

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2111  ∀wral 3106   class class class wbr 5030   × cxp 5517  ‘cfv 6324  2^nd c2nd 7670  Ncnpi 10255   <_N clti 10258   ~_Q ceq 10262  Qcnq 10263

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898  df-nq 10323

This theorem is referenced by:  nqereu  10340  nqerid  10344  enqeq  10345  addpqnq  10349  mulpqnq  10352  ordpinq  10354  addclnq  10356  mulclnq  10358  addnqf  10359  mulnqf  10360  adderpq  10367  mulerpq  10368  addassnq  10369  mulassnq  10370  distrnq  10372  mulidnq  10374  recmulnq  10375  ltsonq  10380  lterpq  10381  ltanq  10382  ltmnq  10383  ltexnq  10386  archnq  10391  wuncn  10581