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

Theorem hlop 29845
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 29844 . 2  |-  ( K  e.  HL  ->  K  e.  OL )
2 olop 29697 . 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 1721   OPcops 29655   OLcol 29657   HLchlt 29833
This theorem is referenced by:  glbconN  29859  glbconxN  29860  hlhgt2  29871  hl0lt1N  29872  hl2at  29887  cvrexch  29902  atcvr0eq  29908  lnnat  29909  atle  29918  cvrat4  29925  athgt  29938  1cvrco  29954  1cvratex  29955  1cvrjat  29957  1cvrat  29958  ps-2  29960  llnn0  29998  lplnn0N  30029  llncvrlpln  30040  lvoln0N  30073  lplncvrlvol  30098  dalemkeop  30107  pmapeq0  30248  pmapglb2N  30253  pmapglb2xN  30254  2atm2atN  30267  polval2N  30388  polsubN  30389  pol1N  30392  2polpmapN  30395  2polvalN  30396  poldmj1N  30410  pmapj2N  30411  2polatN  30414  pnonsingN  30415  ispsubcl2N  30429  polsubclN  30434  poml4N  30435  pmapojoinN  30450  pl42lem1N  30461  lhp2lt  30483  lhp0lt  30485  lhpn0  30486  lhpexnle  30488  lhpoc2N  30497  lhpocnle  30498  lhpj1  30504  lhpmod2i2  30520  lhpmod6i1  30521  lhprelat3N  30522  ltrnatb  30619  ltrnmw  30633  trlcl  30646  trlle  30666  cdleme3c  30712  cdleme7e  30729  cdleme22b  30823  cdlemg12e  31129  cdlemg12g  31131  tendoid  31255  tendo0tp  31271  cdlemk39s-id  31422  tendoex  31457  dia0eldmN  31523  dia2dimlem2  31548  dia2dimlem3  31549  docaclN  31607  doca2N  31609  djajN  31620  dib0  31647  dih0  31763  dih0bN  31764  dih0rn  31767  dih1  31769  dih1rn  31770  dih1cnv  31771  dihmeetlem18N  31807  dih1dimatlem  31812  dihlspsnssN  31815  dihlspsnat  31816  dihatexv  31821  dihglb2  31825  dochcl  31836  doch0  31841  doch1  31842  dochvalr3  31846  doch2val2  31847  dochss  31848  dochocss  31849  dochoc  31850  dochnoncon  31874  djhlj  31884  dihjatc  31900
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-ol 29661  df-oml 29662  df-hlat 29834
  Copyright terms: Public domain W3C validator