Theorem hlop 39867

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

Syntax hints:   → wi 4   ∈ wcel 2121  OPcops 39677  OLcol 39679  HLchlt 39855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-iota 6444  df-fv 6496  df-ov 7362  df-ol 39683  df-oml 39684  df-hlat 39856

This theorem is referenced by:  glbconN  39882  glbconxN  39883  hlhgt2  39894  hl0lt1N  39895  hl2at  39910  cvrexch  39925  atcvr0eq  39931  lnnat  39932  atle  39941  cvrat4  39948  athgt  39961  1cvrco  39977  1cvratex  39978  1cvrjat  39980  1cvrat  39981  ps-2  39983  llnn0  40021  lplnn0N  40052  llncvrlpln  40063  lvoln0N  40096  lplncvrlvol  40121  dalemkeop  40130  pmapeq0  40271  pmapglb2N  40276  pmapglb2xN  40277  2atm2atN  40290  polval2N  40411  polsubN  40412  pol1N  40415  2polpmapN  40418  2polvalN  40419  poldmj1N  40433  pmapj2N  40434  2polatN  40437  pnonsingN  40438  ispsubcl2N  40452  polsubclN  40457  poml4N  40458  pmapojoinN  40473  pl42lem1N  40484  lhp2lt  40506  lhp0lt  40508  lhpn0  40509  lhpexnle  40511  lhpoc2N  40520  lhpocnle  40521  lhpj1  40527  lhpmod2i2  40543  lhpmod6i1  40544  lhprelat3N  40545  ltrnatb  40642  trlcl  40669  trlle  40689  cdleme3c  40735  cdleme7e  40752  cdleme22b  40846  cdlemg12e  41152  cdlemg12g  41154  tendoid  41278  tendo0tp  41294  cdlemk39s-id  41445  tendoex  41480  dia0eldmN  41545  dia2dimlem2  41570  dia2dimlem3  41571  docaclN  41629  doca2N  41631  djajN  41642  dib0  41669  dih0  41785  dih0bN  41786  dih0rn  41789  dih1  41791  dih1rn  41792  dih1cnv  41793  dihmeetlem18N  41829  dih1dimatlem  41834  dihlspsnssN  41837  dihlspsnat  41838  dihatexv  41843  dihglb2  41847  dochcl  41858  doch0  41863  doch1  41864  dochvalr3  41868  doch2val2  41869  dochss  41870  dochocss  41871  dochoc  41872  dochnoncon  41896  djhlj  41906  dihjatc  41922