Theorem hlop 39340

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

Syntax hints:   → wi 4   ∈ wcel 2109  OPcops 39150  OLcol 39152  HLchlt 39328

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-ol 39156  df-oml 39157  df-hlat 39329

This theorem is referenced by:  glbconN  39355  glbconNOLD  39356  glbconxN  39357  hlhgt2  39368  hl0lt1N  39369  hl2at  39384  cvrexch  39399  atcvr0eq  39405  lnnat  39406  atle  39415  cvrat4  39422  athgt  39435  1cvrco  39451  1cvratex  39452  1cvrjat  39454  1cvrat  39455  ps-2  39457  llnn0  39495  lplnn0N  39526  llncvrlpln  39537  lvoln0N  39570  lplncvrlvol  39595  dalemkeop  39604  pmapeq0  39745  pmapglb2N  39750  pmapglb2xN  39751  2atm2atN  39764  polval2N  39885  polsubN  39886  pol1N  39889  2polpmapN  39892  2polvalN  39893  poldmj1N  39907  pmapj2N  39908  2polatN  39911  pnonsingN  39912  ispsubcl2N  39926  polsubclN  39931  poml4N  39932  pmapojoinN  39947  pl42lem1N  39958  lhp2lt  39980  lhp0lt  39982  lhpn0  39983  lhpexnle  39985  lhpoc2N  39994  lhpocnle  39995  lhpj1  40001  lhpmod2i2  40017  lhpmod6i1  40018  lhprelat3N  40019  ltrnatb  40116  trlcl  40143  trlle  40163  cdleme3c  40209  cdleme7e  40226  cdleme22b  40320  cdlemg12e  40626  cdlemg12g  40628  tendoid  40752  tendo0tp  40768  cdlemk39s-id  40919  tendoex  40954  dia0eldmN  41019  dia2dimlem2  41044  dia2dimlem3  41045  docaclN  41103  doca2N  41105  djajN  41116  dib0  41143  dih0  41259  dih0bN  41260  dih0rn  41263  dih1  41265  dih1rn  41266  dih1cnv  41267  dihmeetlem18N  41303  dih1dimatlem  41308  dihlspsnssN  41311  dihlspsnat  41312  dihatexv  41317  dihglb2  41321  dochcl  41332  doch0  41337  doch1  41338  dochvalr3  41342  doch2val2  41343  dochss  41344  dochocss  41345  dochoc  41346  dochnoncon  41370  djhlj  41380  dihjatc  41396