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

Theorem hlop 32380
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 32379 . 2  |-  ( K  e.  HL  ->  K  e.  OL )
2 olop 32232 . 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 1842   OPcops 32190   OLcol 32192   HLchlt 32368
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-br 4396  df-iota 5533  df-fv 5577  df-ov 6281  df-ol 32196  df-oml 32197  df-hlat 32369
This theorem is referenced by:  glbconN  32394  glbconxN  32395  hlhgt2  32406  hl0lt1N  32407  hl2at  32422  cvrexch  32437  atcvr0eq  32443  lnnat  32444  atle  32453  cvrat4  32460  athgt  32473  1cvrco  32489  1cvratex  32490  1cvrjat  32492  1cvrat  32493  ps-2  32495  llnn0  32533  lplnn0N  32564  llncvrlpln  32575  lvoln0N  32608  lplncvrlvol  32633  dalemkeop  32642  pmapeq0  32783  pmapglb2N  32788  pmapglb2xN  32789  2atm2atN  32802  polval2N  32923  polsubN  32924  pol1N  32927  2polpmapN  32930  2polvalN  32931  poldmj1N  32945  pmapj2N  32946  2polatN  32949  pnonsingN  32950  ispsubcl2N  32964  polsubclN  32969  poml4N  32970  pmapojoinN  32985  pl42lem1N  32996  lhp2lt  33018  lhp0lt  33020  lhpn0  33021  lhpexnle  33023  lhpoc2N  33032  lhpocnle  33033  lhpj1  33039  lhpmod2i2  33055  lhpmod6i1  33056  lhprelat3N  33057  ltrnatb  33154  ltrnmwOLD  33169  trlcl  33182  trlle  33202  cdleme3c  33248  cdleme7e  33265  cdleme22b  33360  cdlemg12e  33666  cdlemg12g  33668  tendoid  33792  tendo0tp  33808  cdlemk39s-id  33959  tendoex  33994  dia0eldmN  34060  dia2dimlem2  34085  dia2dimlem3  34086  docaclN  34144  doca2N  34146  djajN  34157  dib0  34184  dih0  34300  dih0bN  34301  dih0rn  34304  dih1  34306  dih1rn  34307  dih1cnv  34308  dihmeetlem18N  34344  dih1dimatlem  34349  dihlspsnssN  34352  dihlspsnat  34353  dihatexv  34358  dihglb2  34362  dochcl  34373  doch0  34378  doch1  34379  dochvalr3  34383  doch2val2  34384  dochss  34385  dochocss  34386  dochoc  34387  dochnoncon  34411  djhlj  34421  dihjatc  34437
  Copyright terms: Public domain W3C validator