Theorem hlop 39822

Description: A Hilbert lattice is an orthoposet. (Contributed by NM, 20-Oct-2011.)

Assertion

Ref	Expression
hlop	⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)

Proof of Theorem hlop

Step	Hyp	Ref	Expression
1		hlol 39821	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
2		olop 39674	. 2 ⊢ (𝐾 ∈ OL → 𝐾 ∈ OP)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)

Syntax hints:   → wi 4   ∈ wcel 2114  OPcops 39632  OLcol 39634  HLchlt 39810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363  df-ol 39638  df-oml 39639  df-hlat 39811

This theorem is referenced by:  glbconN  39837  glbconxN  39838  hlhgt2  39849  hl0lt1N  39850  hl2at  39865  cvrexch  39880  atcvr0eq  39886  lnnat  39887  atle  39896  cvrat4  39903  athgt  39916  1cvrco  39932  1cvratex  39933  1cvrjat  39935  1cvrat  39936  ps-2  39938  llnn0  39976  lplnn0N  40007  llncvrlpln  40018  lvoln0N  40051  lplncvrlvol  40076  dalemkeop  40085  pmapeq0  40226  pmapglb2N  40231  pmapglb2xN  40232  2atm2atN  40245  polval2N  40366  polsubN  40367  pol1N  40370  2polpmapN  40373  2polvalN  40374  poldmj1N  40388  pmapj2N  40389  2polatN  40392  pnonsingN  40393  ispsubcl2N  40407  polsubclN  40412  poml4N  40413  pmapojoinN  40428  pl42lem1N  40439  lhp2lt  40461  lhp0lt  40463  lhpn0  40464  lhpexnle  40466  lhpoc2N  40475  lhpocnle  40476  lhpj1  40482  lhpmod2i2  40498  lhpmod6i1  40499  lhprelat3N  40500  ltrnatb  40597  trlcl  40624  trlle  40644  cdleme3c  40690  cdleme7e  40707  cdleme22b  40801  cdlemg12e  41107  cdlemg12g  41109  tendoid  41233  tendo0tp  41249  cdlemk39s-id  41400  tendoex  41435  dia0eldmN  41500  dia2dimlem2  41525  dia2dimlem3  41526  docaclN  41584  doca2N  41586  djajN  41597  dib0  41624  dih0  41740  dih0bN  41741  dih0rn  41744  dih1  41746  dih1rn  41747  dih1cnv  41748  dihmeetlem18N  41784  dih1dimatlem  41789  dihlspsnssN  41792  dihlspsnat  41793  dihatexv  41798  dihglb2  41802  dochcl  41813  doch0  41818  doch1  41819  dochvalr3  41823  doch2val2  41824  dochss  41825  dochocss  41826  dochoc  41827  dochnoncon  41851  djhlj  41861  dihjatc  41877