MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltrelnq Structured version   Unicode version

Theorem ltrelnq 9207
Description: Positive fraction 'less than' is a relation on positive fractions. (Contributed by NM, 14-Feb-1996.) (Revised by Mario Carneiro, 27-Apr-2013.) (New usage is discouraged.)
Assertion
Ref Expression
ltrelnq  |-  <Q  C_  ( Q.  X.  Q. )

Proof of Theorem ltrelnq
StepHypRef Expression
1 df-ltnq 9199 . 2  |-  <Q  =  (  <pQ  i^i  ( Q.  X.  Q. ) )
2 inss2 3680 . 2  |-  (  <pQ  i^i  ( Q.  X.  Q. ) )  C_  ( Q.  X.  Q. )
31, 2eqsstri 3495 1  |-  <Q  C_  ( Q.  X.  Q. )
Colors of variables: wff setvar class
Syntax hints:    i^i cin 3436    C_ wss 3437    X. cxp 4947    <pQ cltpq 9129   Q.cnq 9131    <Q cltq 9137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-in 3444  df-ss 3451  df-ltnq 9199
This theorem is referenced by:  lterpq  9251  ltanq  9252  ltmnq  9253  ltexnq  9256  ltbtwnnq  9259  ltrnq  9260  prcdnq  9274  prnmadd  9278  genpcd  9287  nqpr  9295  1idpr  9310  prlem934  9314  ltexprlem4  9320  prlem936  9328  reclem2pr  9329  reclem3pr  9330  reclem4pr  9331
  Copyright terms: Public domain W3C validator