Theorem elpqn 10808

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2110  ∀wral 3045   class class class wbr 5089   × cxp 5612  ‘cfv 6477  2^nd c2nd 7915  Ncnpi 10727   <_N clti 10730   ~_Q ceq 10734  Qcnq 10735

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-ss 3917  df-nq 10795

This theorem is referenced by:  nqereu  10812  nqerid  10816  enqeq  10817  addpqnq  10821  mulpqnq  10824  ordpinq  10826  addclnq  10828  mulclnq  10830  addnqf  10831  mulnqf  10832  adderpq  10839  mulerpq  10840  addassnq  10841  mulassnq  10842  distrnq  10844  mulidnq  10846  recmulnq  10847  ltsonq  10852  lterpq  10853  ltanq  10854  ltmnq  10855  ltexnq  10858  archnq  10863  wuncn  11053