Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hlop Structured version   Unicode version

Theorem hlop 30234
Description: A Hilbert lattice is an orthoposet. (Contributed by NM, 20-Oct-2011.)
Assertion
Ref Expression
hlop  |-  ( K  e.  HL  ->  K  e.  OP )

Proof of Theorem hlop
StepHypRef Expression
1 hlol 30233 . 2  |-  ( K  e.  HL  ->  K  e.  OL )
2 olop 30086 . 2  |-  ( K  e.  OL  ->  K  e.  OP )
31, 2syl 16 1  |-  ( K  e.  HL  ->  K  e.  OP )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   OPcops 30044   OLcol 30046   HLchlt 30222
This theorem is referenced by:  glbconN  30248  glbconxN  30249  hlhgt2  30260  hl0lt1N  30261  hl2at  30276  cvrexch  30291  atcvr0eq  30297  lnnat  30298  atle  30307  cvrat4  30314  athgt  30327  1cvrco  30343  1cvratex  30344  1cvrjat  30346  1cvrat  30347  ps-2  30349  llnn0  30387  lplnn0N  30418  llncvrlpln  30429  lvoln0N  30462  lplncvrlvol  30487  dalemkeop  30496  pmapeq0  30637  pmapglb2N  30642  pmapglb2xN  30643  2atm2atN  30656  polval2N  30777  polsubN  30778  pol1N  30781  2polpmapN  30784  2polvalN  30785  poldmj1N  30799  pmapj2N  30800  2polatN  30803  pnonsingN  30804  ispsubcl2N  30818  polsubclN  30823  poml4N  30824  pmapojoinN  30839  pl42lem1N  30850  lhp2lt  30872  lhp0lt  30874  lhpn0  30875  lhpexnle  30877  lhpoc2N  30886  lhpocnle  30887  lhpj1  30893  lhpmod2i2  30909  lhpmod6i1  30910  lhprelat3N  30911  ltrnatb  31008  ltrnmw  31022  trlcl  31035  trlle  31055  cdleme3c  31101  cdleme7e  31118  cdleme22b  31212  cdlemg12e  31518  cdlemg12g  31520  tendoid  31644  tendo0tp  31660  cdlemk39s-id  31811  tendoex  31846  dia0eldmN  31912  dia2dimlem2  31937  dia2dimlem3  31938  docaclN  31996  doca2N  31998  djajN  32009  dib0  32036  dih0  32152  dih0bN  32153  dih0rn  32156  dih1  32158  dih1rn  32159  dih1cnv  32160  dihmeetlem18N  32196  dih1dimatlem  32201  dihlspsnssN  32204  dihlspsnat  32205  dihatexv  32210  dihglb2  32214  dochcl  32225  doch0  32230  doch1  32231  dochvalr3  32235  doch2val2  32236  dochss  32237  dochocss  32238  dochoc  32239  dochnoncon  32263  djhlj  32273  dihjatc  32289
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-iota 5421  df-fv 5465  df-ov 6087  df-ol 30050  df-oml 30051  df-hlat 30223
  Copyright terms: Public domain W3C validator