MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elpqn Structured version   Visualization version   GIF version

Theorem elpqn 10950
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.
StepHypRef Expression
1 df-nq 10937 . . 3 Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd𝑥) <N (2nd𝑦))}
21ssrab3 4076 . 2 Q ⊆ (N × N)
32sseli 3972 1 (𝐴Q𝐴 ∈ (N × N))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2098  wral 3050   class class class wbr 5149   × cxp 5676  cfv 6549  2nd c2nd 7993  Ncnpi 10869   <N clti 10872   ~Q ceq 10876  Qcnq 10877
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-ss 3961  df-nq 10937
This theorem is referenced by:  nqereu  10954  nqerid  10958  enqeq  10959  addpqnq  10963  mulpqnq  10966  ordpinq  10968  addclnq  10970  mulclnq  10972  addnqf  10973  mulnqf  10974  adderpq  10981  mulerpq  10982  addassnq  10983  mulassnq  10984  distrnq  10986  mulidnq  10988  recmulnq  10989  ltsonq  10994  lterpq  10995  ltanq  10996  ltmnq  10997  ltexnq  11000  archnq  11005  wuncn  11195
  Copyright terms: Public domain W3C validator