Theorem hlop 39363

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 39362	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
2		olop 39215	. 2 ⊢ (𝐾 ∈ OL → 𝐾 ∈ OP)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)

Syntax hints:   → wi 4   ∈ wcel 2108  OPcops 39173  OLcol 39175  HLchlt 39351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-ol 39179  df-oml 39180  df-hlat 39352

This theorem is referenced by:  glbconN  39378  glbconNOLD  39379  glbconxN  39380  hlhgt2  39391  hl0lt1N  39392  hl2at  39407  cvrexch  39422  atcvr0eq  39428  lnnat  39429  atle  39438  cvrat4  39445  athgt  39458  1cvrco  39474  1cvratex  39475  1cvrjat  39477  1cvrat  39478  ps-2  39480  llnn0  39518  lplnn0N  39549  llncvrlpln  39560  lvoln0N  39593  lplncvrlvol  39618  dalemkeop  39627  pmapeq0  39768  pmapglb2N  39773  pmapglb2xN  39774  2atm2atN  39787  polval2N  39908  polsubN  39909  pol1N  39912  2polpmapN  39915  2polvalN  39916  poldmj1N  39930  pmapj2N  39931  2polatN  39934  pnonsingN  39935  ispsubcl2N  39949  polsubclN  39954  poml4N  39955  pmapojoinN  39970  pl42lem1N  39981  lhp2lt  40003  lhp0lt  40005  lhpn0  40006  lhpexnle  40008  lhpoc2N  40017  lhpocnle  40018  lhpj1  40024  lhpmod2i2  40040  lhpmod6i1  40041  lhprelat3N  40042  ltrnatb  40139  trlcl  40166  trlle  40186  cdleme3c  40232  cdleme7e  40249  cdleme22b  40343  cdlemg12e  40649  cdlemg12g  40651  tendoid  40775  tendo0tp  40791  cdlemk39s-id  40942  tendoex  40977  dia0eldmN  41042  dia2dimlem2  41067  dia2dimlem3  41068  docaclN  41126  doca2N  41128  djajN  41139  dib0  41166  dih0  41282  dih0bN  41283  dih0rn  41286  dih1  41288  dih1rn  41289  dih1cnv  41290  dihmeetlem18N  41326  dih1dimatlem  41331  dihlspsnssN  41334  dihlspsnat  41335  dihatexv  41340  dihglb2  41344  dochcl  41355  doch0  41360  doch1  41361  dochvalr3  41365  doch2val2  41366  dochss  41367  dochocss  41368  dochoc  41369  dochnoncon  41393  djhlj  41403  dihjatc  41419