Theorem elpqn 10347

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114  ∀wral 3138   class class class wbr 5066   × cxp 5553  ‘cfv 6355  2^nd c2nd 7688  Ncnpi 10266   <_N clti 10269   ~_Q ceq 10273  Qcnq 10274

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-in 3943  df-ss 3952  df-nq 10334

This theorem is referenced by:  nqereu  10351  nqerid  10355  enqeq  10356  addpqnq  10360  mulpqnq  10363  ordpinq  10365  addclnq  10367  mulclnq  10369  addnqf  10370  mulnqf  10371  adderpq  10378  mulerpq  10379  addassnq  10380  mulassnq  10381  distrnq  10383  mulidnq  10385  recmulnq  10386  ltsonq  10391  lterpq  10392  ltanq  10393  ltmnq  10394  ltexnq  10397  archnq  10402  wuncn  10592