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

Theorem elpqn 10335
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 10322 . . 3 Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd𝑥) <N (2nd𝑦))}
21ssrab3 4054 . 2 Q ⊆ (N × N)
32sseli 3960 1 (𝐴Q𝐴 ∈ (N × N))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2105  wral 3135   class class class wbr 5057   × cxp 5546  cfv 6348  2nd c2nd 7677  Ncnpi 10254   <N clti 10257   ~Q ceq 10261  Qcnq 10262
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-in 3940  df-ss 3949  df-nq 10322
This theorem is referenced by:  nqereu  10339  nqerid  10343  enqeq  10344  addpqnq  10348  mulpqnq  10351  ordpinq  10353  addclnq  10355  mulclnq  10357  addnqf  10358  mulnqf  10359  adderpq  10366  mulerpq  10367  addassnq  10368  mulassnq  10369  distrnq  10371  mulidnq  10373  recmulnq  10374  ltsonq  10379  lterpq  10380  ltanq  10381  ltmnq  10382  ltexnq  10385  archnq  10390  wuncn  10580
  Copyright terms: Public domain W3C validator