Theorem elpqn 10848

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114  ∀wral 3052   class class class wbr 5100   × cxp 5630  ‘cfv 6500  2^nd c2nd 7942  Ncnpi 10767   <_N clti 10770   ~_Q ceq 10774  Qcnq 10775

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-ss 3920  df-nq 10835

This theorem is referenced by:  nqereu  10852  nqerid  10856  enqeq  10857  addpqnq  10861  mulpqnq  10864  ordpinq  10866  addclnq  10868  mulclnq  10870  addnqf  10871  mulnqf  10872  adderpq  10879  mulerpq  10880  addassnq  10881  mulassnq  10882  distrnq  10884  mulidnq  10886  recmulnq  10887  ltsonq  10892  lterpq  10893  ltanq  10894  ltmnq  10895  ltexnq  10898  archnq  10903  wuncn  11093