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

Theorem hlop 32922
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 32921 . 2  |-  ( K  e.  HL  ->  K  e.  OL )
2 olop 32774 . 2  |-  ( K  e.  OL  ->  K  e.  OP )
31, 2syl 17 1  |-  ( K  e.  HL  ->  K  e.  OP )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1886   OPcops 32732   OLcol 32734   HLchlt 32910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-br 4402  df-iota 5545  df-fv 5589  df-ov 6291  df-ol 32738  df-oml 32739  df-hlat 32911
This theorem is referenced by:  glbconN  32936  glbconxN  32937  hlhgt2  32948  hl0lt1N  32949  hl2at  32964  cvrexch  32979  atcvr0eq  32985  lnnat  32986  atle  32995  cvrat4  33002  athgt  33015  1cvrco  33031  1cvratex  33032  1cvrjat  33034  1cvrat  33035  ps-2  33037  llnn0  33075  lplnn0N  33106  llncvrlpln  33117  lvoln0N  33150  lplncvrlvol  33175  dalemkeop  33184  pmapeq0  33325  pmapglb2N  33330  pmapglb2xN  33331  2atm2atN  33344  polval2N  33465  polsubN  33466  pol1N  33469  2polpmapN  33472  2polvalN  33473  poldmj1N  33487  pmapj2N  33488  2polatN  33491  pnonsingN  33492  ispsubcl2N  33506  polsubclN  33511  poml4N  33512  pmapojoinN  33527  pl42lem1N  33538  lhp2lt  33560  lhp0lt  33562  lhpn0  33563  lhpexnle  33565  lhpoc2N  33574  lhpocnle  33575  lhpj1  33581  lhpmod2i2  33597  lhpmod6i1  33598  lhprelat3N  33599  ltrnatb  33696  ltrnmwOLD  33711  trlcl  33724  trlle  33744  cdleme3c  33790  cdleme7e  33807  cdleme22b  33902  cdlemg12e  34208  cdlemg12g  34210  tendoid  34334  tendo0tp  34350  cdlemk39s-id  34501  tendoex  34536  dia0eldmN  34602  dia2dimlem2  34627  dia2dimlem3  34628  docaclN  34686  doca2N  34688  djajN  34699  dib0  34726  dih0  34842  dih0bN  34843  dih0rn  34846  dih1  34848  dih1rn  34849  dih1cnv  34850  dihmeetlem18N  34886  dih1dimatlem  34891  dihlspsnssN  34894  dihlspsnat  34895  dihatexv  34900  dihglb2  34904  dochcl  34915  doch0  34920  doch1  34921  dochvalr3  34925  doch2val2  34926  dochss  34927  dochocss  34928  dochoc  34929  dochnoncon  34953  djhlj  34963  dihjatc  34979
  Copyright terms: Public domain W3C validator