Theorem elpqn 10920

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2107  ∀wral 3062   class class class wbr 5149   × cxp 5675  ‘cfv 6544  2^nd c2nd 7974  Ncnpi 10839   <_N clti 10842   ~_Q ceq 10846  Qcnq 10847

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-nq 10907

This theorem is referenced by:  nqereu  10924  nqerid  10928  enqeq  10929  addpqnq  10933  mulpqnq  10936  ordpinq  10938  addclnq  10940  mulclnq  10942  addnqf  10943  mulnqf  10944  adderpq  10951  mulerpq  10952  addassnq  10953  mulassnq  10954  distrnq  10956  mulidnq  10958  recmulnq  10959  ltsonq  10964  lterpq  10965  ltanq  10966  ltmnq  10967  ltexnq  10970  archnq  10975  wuncn  11165