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

Theorem elpqn 9949
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 9936 . . 3 Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd𝑥) <N (2nd𝑦))}
2 ssrab2 3836 . . 3 {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd𝑥) <N (2nd𝑦))} ⊆ (N × N)
31, 2eqsstri 3784 . 2 Q ⊆ (N × N)
43sseli 3748 1 (𝐴Q𝐴 ∈ (N × N))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2145  wral 3061  {crab 3065   class class class wbr 4786   × cxp 5247  cfv 6031  2nd c2nd 7314  Ncnpi 9868   <N clti 9871   ~Q ceq 9875  Qcnq 9876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-in 3730  df-ss 3737  df-nq 9936
This theorem is referenced by:  nqereu  9953  nqerid  9957  enqeq  9958  addpqnq  9962  mulpqnq  9965  ordpinq  9967  addclnq  9969  mulclnq  9971  addnqf  9972  mulnqf  9973  adderpq  9980  mulerpq  9981  addassnq  9982  mulassnq  9983  distrnq  9985  mulidnq  9987  recmulnq  9988  ltsonq  9993  lterpq  9994  ltanq  9995  ltmnq  9996  ltexnq  9999  archnq  10004  wuncn  10193
  Copyright terms: Public domain W3C validator