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

Theorem ltrelnq 8550
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 8542 . 2  |-  <Q  =  (  <pQ  i^i  ( Q.  X.  Q. ) )
2 inss2 3390 . 2  |-  (  <pQ  i^i  ( Q.  X.  Q. ) )  C_  ( Q.  X.  Q. )
31, 2eqsstri 3208 1  |-  <Q  C_  ( Q.  X.  Q. )
Colors of variables: wff set class
Syntax hints:    i^i cin 3151    C_ wss 3152    X. cxp 4687    <pQ cltpq 8472   Q.cnq 8474    <Q cltq 8480
This theorem is referenced by:  lterpq  8594  ltanq  8595  ltmnq  8596  ltexnq  8599  ltbtwnnq  8602  ltrnq  8603  prcdnq  8617  prnmadd  8621  genpcd  8630  nqpr  8638  1idpr  8653  prlem934  8657  ltexprlem4  8663  prlem936  8671  reclem2pr  8672  reclem3pr  8673  reclem4pr  8674
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166  df-ltnq 8542
  Copyright terms: Public domain W3C validator