ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ltrelnq Unicode version

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

Proof of Theorem ltrelnq
Dummy variables  x  y  z  w  u  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ltnqqs 6451 . 2  |-  <Q  =  { <. x ,  y
>.  |  ( (
x  e.  Q.  /\  y  e.  Q. )  /\  E. z E. w E. v E. u ( ( x  =  [ <. z ,  w >. ]  ~Q  /\  y  =  [ <. v ,  u >. ]  ~Q  )  /\  ( z  .N  u
)  <N  ( w  .N  v ) ) ) }
2 opabssxp 4414 . 2  |-  { <. x ,  y >.  |  ( ( x  e.  Q.  /\  y  e.  Q. )  /\  E. z E. w E. v E. u ( ( x  =  [ <. z ,  w >. ]  ~Q  /\  y  =  [ <. v ,  u >. ]  ~Q  )  /\  ( z  .N  u
)  <N  ( w  .N  v ) ) ) }  C_  ( Q.  X.  Q. )
31, 2eqsstri 2975 1  |-  <Q  C_  ( Q.  X.  Q. )
Colors of variables: wff set class
Syntax hints:    /\ wa 97    = wceq 1243   E.wex 1381    e. wcel 1393    C_ wss 2917   <.cop 3378   class class class wbr 3764   {copab 3817    X. cxp 4343  (class class class)co 5512   [cec 6104    .N cmi 6372    <N clti 6373    ~Q ceq 6377   Q.cnq 6378    <Q cltq 6383
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-in 2924  df-ss 2931  df-opab 3819  df-xp 4351  df-ltnqqs 6451
This theorem is referenced by:  ltanqi  6500  ltmnqi  6501  lt2addnq  6502  lt2mulnq  6503  ltexnqi  6507  ltbtwnnqq  6513  ltbtwnnq  6514  prarloclemarch2  6517  ltrnqi  6519  prcdnql  6582  prcunqu  6583  prnmaxl  6586  prnminu  6587  prloc  6589  prarloclemcalc  6600  genplt2i  6608  genpcdl  6617  genpcuu  6618  genpdisj  6621  addnqprllem  6625  addnqprulem  6626  addlocprlemlt  6629  addlocprlemeq  6631  addlocprlemgt  6632  addlocprlem  6633  nqprdisj  6642  nqprloc  6643  nqprxx  6644  ltnqex  6647  gtnqex  6648  addnqprlemrl  6655  addnqprlemru  6656  addnqprlemfl  6657  addnqprlemfu  6658  appdivnq  6661  prmuloclemcalc  6663  prmuloc  6664  mulnqprlemrl  6671  mulnqprlemru  6672  mulnqprlemfl  6673  mulnqprlemfu  6674  1idprl  6688  1idpru  6689  ltnqpri  6692  ltsopr  6694  ltexprlemopl  6699  ltexprlemopu  6701  ltexprlemdisj  6704  ltexprlemloc  6705  ltexprlemfl  6707  ltexprlemru  6710  recexprlemell  6720  recexprlemelu  6721  recexprlemlol  6724  recexprlemupu  6726  recexprlemdisj  6728  recexprlemloc  6729  recexprlempr  6730  recexprlem1ssl  6731  recexprlem1ssu  6732  recexprlemss1l  6733  recexprlemss1u  6734  cauappcvgprlemm  6743  cauappcvgprlemopl  6744  cauappcvgprlemlol  6745  cauappcvgprlemupu  6747  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  caucvgprlemk  6763  caucvgprlemnkj  6764  caucvgprlemnbj  6765  caucvgprlemm  6766  caucvgprlemopl  6767  caucvgprlemlol  6768  caucvgprlemupu  6770  caucvgprlemloc  6773  caucvgprlemladdfu  6775  caucvgprprlemloccalc  6782  caucvgprprlemml  6792  caucvgprprlemopl  6795  caucvgprprlemlol  6796  caucvgprprlemupu  6798  caucvgprprlemloc  6801
  Copyright terms: Public domain W3C validator