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

Theorem ltrelnq 8736
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 8728 . 2  |-  <Q  =  (  <pQ  i^i  ( Q.  X.  Q. ) )
2 inss2 3505 . 2  |-  (  <pQ  i^i  ( Q.  X.  Q. ) )  C_  ( Q.  X.  Q. )
31, 2eqsstri 3321 1  |-  <Q  C_  ( Q.  X.  Q. )
Colors of variables: wff set class
Syntax hints:    i^i cin 3262    C_ wss 3263    X. cxp 4816    <pQ cltpq 8658   Q.cnq 8660    <Q cltq 8666
This theorem is referenced by:  lterpq  8780  ltanq  8781  ltmnq  8782  ltexnq  8785  ltbtwnnq  8788  ltrnq  8789  prcdnq  8803  prnmadd  8807  genpcd  8816  nqpr  8824  1idpr  8839  prlem934  8843  ltexprlem4  8849  prlem936  8857  reclem2pr  8858  reclem3pr  8859  reclem4pr  8860
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901  df-in 3270  df-ss 3277  df-ltnq 8728
  Copyright terms: Public domain W3C validator