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

Theorem ltrelnq 8566
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 8558 . 2  |-  <Q  =  (  <pQ  i^i  ( Q.  X.  Q. ) )
2 inss2 3403 . 2  |-  (  <pQ  i^i  ( Q.  X.  Q. ) )  C_  ( Q.  X.  Q. )
31, 2eqsstri 3221 1  |-  <Q  C_  ( Q.  X.  Q. )
Colors of variables: wff set class
Syntax hints:    i^i cin 3164    C_ wss 3165    X. cxp 4703    <pQ cltpq 8488   Q.cnq 8490    <Q cltq 8496
This theorem is referenced by:  lterpq  8610  ltanq  8611  ltmnq  8612  ltexnq  8615  ltbtwnnq  8618  ltrnq  8619  prcdnq  8633  prnmadd  8637  genpcd  8646  nqpr  8654  1idpr  8669  prlem934  8673  ltexprlem4  8679  prlem936  8687  reclem2pr  8688  reclem3pr  8689  reclem4pr  8690
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179  df-ltnq 8558
  Copyright terms: Public domain W3C validator