Theorem elpqn 10823

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2113  ∀wral 3048   class class class wbr 5093   × cxp 5617  ‘cfv 6486  2^nd c2nd 7926  Ncnpi 10742   <_N clti 10745   ~_Q ceq 10749  Qcnq 10750

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-ss 3915  df-nq 10810

This theorem is referenced by:  nqereu  10827  nqerid  10831  enqeq  10832  addpqnq  10836  mulpqnq  10839  ordpinq  10841  addclnq  10843  mulclnq  10845  addnqf  10846  mulnqf  10847  adderpq  10854  mulerpq  10855  addassnq  10856  mulassnq  10857  distrnq  10859  mulidnq  10861  recmulnq  10862  ltsonq  10867  lterpq  10868  ltanq  10869  ltmnq  10870  ltexnq  10873  archnq  10878  wuncn  11068