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

Theorem elpqn 10345
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 10332 . . 3 Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd𝑥) <N (2nd𝑦))}
21ssrab3 4043 . 2 Q ⊆ (N × N)
32sseli 3949 1 (𝐴Q𝐴 ∈ (N × N))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2115  wral 3133   class class class wbr 5052   × cxp 5540  cfv 6343  2nd c2nd 7683  Ncnpi 10264   <N clti 10267   ~Q ceq 10271  Qcnq 10272
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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-rab 3142  df-v 3482  df-in 3926  df-ss 3936  df-nq 10332
This theorem is referenced by:  nqereu  10349  nqerid  10353  enqeq  10354  addpqnq  10358  mulpqnq  10361  ordpinq  10363  addclnq  10365  mulclnq  10367  addnqf  10368  mulnqf  10369  adderpq  10376  mulerpq  10377  addassnq  10378  mulassnq  10379  distrnq  10381  mulidnq  10383  recmulnq  10384  ltsonq  10389  lterpq  10390  ltanq  10391  ltmnq  10392  ltexnq  10395  archnq  10400  wuncn  10590
  Copyright terms: Public domain W3C validator