Theorem hlop 39380

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

Syntax hints:   → wi 4   ∈ wcel 2108  OPcops 39190  OLcol 39192  HLchlt 39368

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-ov 7408  df-ol 39196  df-oml 39197  df-hlat 39369

This theorem is referenced by:  glbconN  39395  glbconNOLD  39396  glbconxN  39397  hlhgt2  39408  hl0lt1N  39409  hl2at  39424  cvrexch  39439  atcvr0eq  39445  lnnat  39446  atle  39455  cvrat4  39462  athgt  39475  1cvrco  39491  1cvratex  39492  1cvrjat  39494  1cvrat  39495  ps-2  39497  llnn0  39535  lplnn0N  39566  llncvrlpln  39577  lvoln0N  39610  lplncvrlvol  39635  dalemkeop  39644  pmapeq0  39785  pmapglb2N  39790  pmapglb2xN  39791  2atm2atN  39804  polval2N  39925  polsubN  39926  pol1N  39929  2polpmapN  39932  2polvalN  39933  poldmj1N  39947  pmapj2N  39948  2polatN  39951  pnonsingN  39952  ispsubcl2N  39966  polsubclN  39971  poml4N  39972  pmapojoinN  39987  pl42lem1N  39998  lhp2lt  40020  lhp0lt  40022  lhpn0  40023  lhpexnle  40025  lhpoc2N  40034  lhpocnle  40035  lhpj1  40041  lhpmod2i2  40057  lhpmod6i1  40058  lhprelat3N  40059  ltrnatb  40156  trlcl  40183  trlle  40203  cdleme3c  40249  cdleme7e  40266  cdleme22b  40360  cdlemg12e  40666  cdlemg12g  40668  tendoid  40792  tendo0tp  40808  cdlemk39s-id  40959  tendoex  40994  dia0eldmN  41059  dia2dimlem2  41084  dia2dimlem3  41085  docaclN  41143  doca2N  41145  djajN  41156  dib0  41183  dih0  41299  dih0bN  41300  dih0rn  41303  dih1  41305  dih1rn  41306  dih1cnv  41307  dihmeetlem18N  41343  dih1dimatlem  41348  dihlspsnssN  41351  dihlspsnat  41352  dihatexv  41357  dihglb2  41361  dochcl  41372  doch0  41377  doch1  41378  dochvalr3  41382  doch2val2  41383  dochss  41384  dochocss  41385  dochoc  41386  dochnoncon  41410  djhlj  41420  dihjatc  41436