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

Theorem hlop 29528
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 29527 . 2  |-  ( K  e.  HL  ->  K  e.  OL )
2 olop 29380 . 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 1717   OPcops 29338   OLcol 29340   HLchlt 29516
This theorem is referenced by:  glbconN  29542  glbconxN  29543  hlhgt2  29554  hl0lt1N  29555  hl2at  29570  cvrexch  29585  atcvr0eq  29591  lnnat  29592  atle  29601  cvrat4  29608  athgt  29621  1cvrco  29637  1cvratex  29638  1cvrjat  29640  1cvrat  29641  ps-2  29643  llnn0  29681  lplnn0N  29712  llncvrlpln  29723  lvoln0N  29756  lplncvrlvol  29781  dalemkeop  29790  pmapeq0  29931  pmapglb2N  29936  pmapglb2xN  29937  2atm2atN  29950  polval2N  30071  polsubN  30072  pol1N  30075  2polpmapN  30078  2polvalN  30079  poldmj1N  30093  pmapj2N  30094  2polatN  30097  pnonsingN  30098  ispsubcl2N  30112  polsubclN  30117  poml4N  30118  pmapojoinN  30133  pl42lem1N  30144  lhp2lt  30166  lhp0lt  30168  lhpn0  30169  lhpexnle  30171  lhpoc2N  30180  lhpocnle  30181  lhpj1  30187  lhpmod2i2  30203  lhpmod6i1  30204  lhprelat3N  30205  ltrnatb  30302  ltrnmw  30316  trlcl  30329  trlle  30349  cdleme3c  30395  cdleme7e  30412  cdleme22b  30506  cdlemg12e  30812  cdlemg12g  30814  tendoid  30938  tendo0tp  30954  cdlemk39s-id  31105  tendoex  31140  dia0eldmN  31206  dia2dimlem2  31231  dia2dimlem3  31232  docaclN  31290  doca2N  31292  djajN  31303  dib0  31330  dih0  31446  dih0bN  31447  dih0rn  31450  dih1  31452  dih1rn  31453  dih1cnv  31454  dihmeetlem18N  31490  dih1dimatlem  31495  dihlspsnssN  31498  dihlspsnat  31499  dihatexv  31504  dihglb2  31508  dochcl  31519  doch0  31524  doch1  31525  dochvalr3  31529  doch2val2  31530  dochss  31531  dochocss  31532  dochoc  31533  dochnoncon  31557  djhlj  31567  dihjatc  31583
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
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 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ral 2647  df-rex 2648  df-rab 2651  df-v 2894  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-nul 3565  df-if 3676  df-sn 3756  df-pr 3757  df-op 3759  df-uni 3951  df-br 4147  df-iota 5351  df-fv 5395  df-ov 6016  df-ol 29344  df-oml 29345  df-hlat 29517
  Copyright terms: Public domain W3C validator