Theorem elpqn 10909

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2149  ∀wral 3085   class class class wbr 5113   × cxp 5660  ‘cfv 6537  2^nd c2nd 7984  Ncnpi 10828   <_N clti 10831   ~_Q ceq 10835  Qcnq 10836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-ss 3930  df-nq 10896

This theorem is referenced by:  nqereu  10913  nqerid  10917  enqeq  10918  addpqnq  10922  mulpqnq  10925  ordpinq  10927  addclnq  10929  mulclnq  10931  addnqf  10932  mulnqf  10933  adderpq  10940  mulerpq  10941  addassnq  10942  mulassnq  10943  distrnq  10945  mulidnq  10947  recmulnq  10948  ltsonq  10953  lterpq  10954  ltanq  10955  ltmnq  10956  ltexnq  10959  archnq  10964  wuncn  11154