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

Theorem hlop 33026
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 33025 . 2  |-  ( K  e.  HL  ->  K  e.  OL )
2 olop 32878 . 2  |-  ( K  e.  OL  ->  K  e.  OP )
31, 2syl 16 1  |-  ( K  e.  HL  ->  K  e.  OP )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   OPcops 32836   OLcol 32838   HLchlt 33014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ral 2735  df-rex 2736  df-rab 2739  df-v 2989  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-nul 3653  df-if 3807  df-sn 3893  df-pr 3895  df-op 3899  df-uni 4107  df-br 4308  df-iota 5396  df-fv 5441  df-ov 6109  df-ol 32842  df-oml 32843  df-hlat 33015
This theorem is referenced by:  glbconN  33040  glbconxN  33041  hlhgt2  33052  hl0lt1N  33053  hl2at  33068  cvrexch  33083  atcvr0eq  33089  lnnat  33090  atle  33099  cvrat4  33106  athgt  33119  1cvrco  33135  1cvratex  33136  1cvrjat  33138  1cvrat  33139  ps-2  33141  llnn0  33179  lplnn0N  33210  llncvrlpln  33221  lvoln0N  33254  lplncvrlvol  33279  dalemkeop  33288  pmapeq0  33429  pmapglb2N  33434  pmapglb2xN  33435  2atm2atN  33448  polval2N  33569  polsubN  33570  pol1N  33573  2polpmapN  33576  2polvalN  33577  poldmj1N  33591  pmapj2N  33592  2polatN  33595  pnonsingN  33596  ispsubcl2N  33610  polsubclN  33615  poml4N  33616  pmapojoinN  33631  pl42lem1N  33642  lhp2lt  33664  lhp0lt  33666  lhpn0  33667  lhpexnle  33669  lhpoc2N  33678  lhpocnle  33679  lhpj1  33685  lhpmod2i2  33701  lhpmod6i1  33702  lhprelat3N  33703  ltrnatb  33800  ltrnmw  33814  trlcl  33827  trlle  33847  cdleme3c  33893  cdleme7e  33910  cdleme22b  34004  cdlemg12e  34310  cdlemg12g  34312  tendoid  34436  tendo0tp  34452  cdlemk39s-id  34603  tendoex  34638  dia0eldmN  34704  dia2dimlem2  34729  dia2dimlem3  34730  docaclN  34788  doca2N  34790  djajN  34801  dib0  34828  dih0  34944  dih0bN  34945  dih0rn  34948  dih1  34950  dih1rn  34951  dih1cnv  34952  dihmeetlem18N  34988  dih1dimatlem  34993  dihlspsnssN  34996  dihlspsnat  34997  dihatexv  35002  dihglb2  35006  dochcl  35017  doch0  35022  doch1  35023  dochvalr3  35027  doch2val2  35028  dochss  35029  dochocss  35030  dochoc  35031  dochnoncon  35055  djhlj  35065  dihjatc  35081
  Copyright terms: Public domain W3C validator