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

Theorem elpqn 10966
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 10953 . . 3 Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd𝑥) <N (2nd𝑦))}
21ssrab3 4081 . 2 Q ⊆ (N × N)
32sseli 3978 1 (𝐴Q𝐴 ∈ (N × N))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2107  wral 3060   class class class wbr 5142   × cxp 5682  cfv 6560  2nd c2nd 8014  Ncnpi 10885   <N clti 10888   ~Q ceq 10892  Qcnq 10893
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-ss 3967  df-nq 10953
This theorem is referenced by:  nqereu  10970  nqerid  10974  enqeq  10975  addpqnq  10979  mulpqnq  10982  ordpinq  10984  addclnq  10986  mulclnq  10988  addnqf  10989  mulnqf  10990  adderpq  10997  mulerpq  10998  addassnq  10999  mulassnq  11000  distrnq  11002  mulidnq  11004  recmulnq  11005  ltsonq  11010  lterpq  11011  ltanq  11012  ltmnq  11013  ltexnq  11016  archnq  11021  wuncn  11211
  Copyright terms: Public domain W3C validator