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

Theorem hlop 30061
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 30060 . 2  |-  ( K  e.  HL  ->  K  e.  OL )
2 olop 29913 . 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 1725   OPcops 29871   OLcol 29873   HLchlt 30049
This theorem is referenced by:  glbconN  30075  glbconxN  30076  hlhgt2  30087  hl0lt1N  30088  hl2at  30103  cvrexch  30118  atcvr0eq  30124  lnnat  30125  atle  30134  cvrat4  30141  athgt  30154  1cvrco  30170  1cvratex  30171  1cvrjat  30173  1cvrat  30174  ps-2  30176  llnn0  30214  lplnn0N  30245  llncvrlpln  30256  lvoln0N  30289  lplncvrlvol  30314  dalemkeop  30323  pmapeq0  30464  pmapglb2N  30469  pmapglb2xN  30470  2atm2atN  30483  polval2N  30604  polsubN  30605  pol1N  30608  2polpmapN  30611  2polvalN  30612  poldmj1N  30626  pmapj2N  30627  2polatN  30630  pnonsingN  30631  ispsubcl2N  30645  polsubclN  30650  poml4N  30651  pmapojoinN  30666  pl42lem1N  30677  lhp2lt  30699  lhp0lt  30701  lhpn0  30702  lhpexnle  30704  lhpoc2N  30713  lhpocnle  30714  lhpj1  30720  lhpmod2i2  30736  lhpmod6i1  30737  lhprelat3N  30738  ltrnatb  30835  ltrnmw  30849  trlcl  30862  trlle  30882  cdleme3c  30928  cdleme7e  30945  cdleme22b  31039  cdlemg12e  31345  cdlemg12g  31347  tendoid  31471  tendo0tp  31487  cdlemk39s-id  31638  tendoex  31673  dia0eldmN  31739  dia2dimlem2  31764  dia2dimlem3  31765  docaclN  31823  doca2N  31825  djajN  31836  dib0  31863  dih0  31979  dih0bN  31980  dih0rn  31983  dih1  31985  dih1rn  31986  dih1cnv  31987  dihmeetlem18N  32023  dih1dimatlem  32028  dihlspsnssN  32031  dihlspsnat  32032  dihatexv  32037  dihglb2  32041  dochcl  32052  doch0  32057  doch1  32058  dochvalr3  32062  doch2val2  32063  dochss  32064  dochocss  32065  dochoc  32066  dochnoncon  32090  djhlj  32100  dihjatc  32116
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-iota 5410  df-fv 5454  df-ov 6076  df-ol 29877  df-oml 29878  df-hlat 30050
  Copyright terms: Public domain W3C validator