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

Theorem elpqn 10082
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 10069 . . 3 Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd𝑥) <N (2nd𝑦))}
21ssrab3 3909 . 2 Q ⊆ (N × N)
32sseli 3817 1 (𝐴Q𝐴 ∈ (N × N))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2107  wral 3090   class class class wbr 4886   × cxp 5353  cfv 6135  2nd c2nd 7444  Ncnpi 10001   <N clti 10004   ~Q ceq 10008  Qcnq 10009
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-in 3799  df-ss 3806  df-nq 10069
This theorem is referenced by:  nqereu  10086  nqerid  10090  enqeq  10091  addpqnq  10095  mulpqnq  10098  ordpinq  10100  addclnq  10102  mulclnq  10104  addnqf  10105  mulnqf  10106  adderpq  10113  mulerpq  10114  addassnq  10115  mulassnq  10116  distrnq  10118  mulidnq  10120  recmulnq  10121  ltsonq  10126  lterpq  10127  ltanq  10128  ltmnq  10129  ltexnq  10132  archnq  10137  wuncn  10327
  Copyright terms: Public domain W3C validator