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

Theorem hlop 32729
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 32728 . 2  |-  ( K  e.  HL  ->  K  e.  OL )
2 olop 32581 . 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 1761   OPcops 32539   OLcol 32541   HLchlt 32717
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-iota 5378  df-fv 5423  df-ov 6093  df-ol 32545  df-oml 32546  df-hlat 32718
This theorem is referenced by:  glbconN  32743  glbconxN  32744  hlhgt2  32755  hl0lt1N  32756  hl2at  32771  cvrexch  32786  atcvr0eq  32792  lnnat  32793  atle  32802  cvrat4  32809  athgt  32822  1cvrco  32838  1cvratex  32839  1cvrjat  32841  1cvrat  32842  ps-2  32844  llnn0  32882  lplnn0N  32913  llncvrlpln  32924  lvoln0N  32957  lplncvrlvol  32982  dalemkeop  32991  pmapeq0  33132  pmapglb2N  33137  pmapglb2xN  33138  2atm2atN  33151  polval2N  33272  polsubN  33273  pol1N  33276  2polpmapN  33279  2polvalN  33280  poldmj1N  33294  pmapj2N  33295  2polatN  33298  pnonsingN  33299  ispsubcl2N  33313  polsubclN  33318  poml4N  33319  pmapojoinN  33334  pl42lem1N  33345  lhp2lt  33367  lhp0lt  33369  lhpn0  33370  lhpexnle  33372  lhpoc2N  33381  lhpocnle  33382  lhpj1  33388  lhpmod2i2  33404  lhpmod6i1  33405  lhprelat3N  33406  ltrnatb  33503  ltrnmw  33517  trlcl  33530  trlle  33550  cdleme3c  33596  cdleme7e  33613  cdleme22b  33707  cdlemg12e  34013  cdlemg12g  34015  tendoid  34139  tendo0tp  34155  cdlemk39s-id  34306  tendoex  34341  dia0eldmN  34407  dia2dimlem2  34432  dia2dimlem3  34433  docaclN  34491  doca2N  34493  djajN  34504  dib0  34531  dih0  34647  dih0bN  34648  dih0rn  34651  dih1  34653  dih1rn  34654  dih1cnv  34655  dihmeetlem18N  34691  dih1dimatlem  34696  dihlspsnssN  34699  dihlspsnat  34700  dihatexv  34705  dihglb2  34709  dochcl  34720  doch0  34725  doch1  34726  dochvalr3  34730  doch2val2  34731  dochss  34732  dochocss  34733  dochoc  34734  dochnoncon  34758  djhlj  34768  dihjatc  34784
  Copyright terms: Public domain W3C validator