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

Theorem elpqn 10963
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 10950 . . 3 Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd𝑥) <N (2nd𝑦))}
21ssrab3 4092 . 2 Q ⊆ (N × N)
32sseli 3991 1 (𝐴Q𝐴 ∈ (N × N))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2106  wral 3059   class class class wbr 5148   × cxp 5687  cfv 6563  2nd c2nd 8012  Ncnpi 10882   <N clti 10885   ~Q ceq 10889  Qcnq 10890
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-ss 3980  df-nq 10950
This theorem is referenced by:  nqereu  10967  nqerid  10971  enqeq  10972  addpqnq  10976  mulpqnq  10979  ordpinq  10981  addclnq  10983  mulclnq  10985  addnqf  10986  mulnqf  10987  adderpq  10994  mulerpq  10995  addassnq  10996  mulassnq  10997  distrnq  10999  mulidnq  11001  recmulnq  11002  ltsonq  11007  lterpq  11008  ltanq  11009  ltmnq  11010  ltexnq  11013  archnq  11018  wuncn  11208
  Copyright terms: Public domain W3C validator