Theorem hlop 39861

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

Syntax hints:   → wi 4   ∈ wcel 2119  OPcops 39671  OLcol 39673  HLchlt 39849

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-ol 39677  df-oml 39678  df-hlat 39850

This theorem is referenced by:  glbconN  39876  glbconxN  39877  hlhgt2  39888  hl0lt1N  39889  hl2at  39904  cvrexch  39919  atcvr0eq  39925  lnnat  39926  atle  39935  cvrat4  39942  athgt  39955  1cvrco  39971  1cvratex  39972  1cvrjat  39974  1cvrat  39975  ps-2  39977  llnn0  40015  lplnn0N  40046  llncvrlpln  40057  lvoln0N  40090  lplncvrlvol  40115  dalemkeop  40124  pmapeq0  40265  pmapglb2N  40270  pmapglb2xN  40271  2atm2atN  40284  polval2N  40405  polsubN  40406  pol1N  40409  2polpmapN  40412  2polvalN  40413  poldmj1N  40427  pmapj2N  40428  2polatN  40431  pnonsingN  40432  ispsubcl2N  40446  polsubclN  40451  poml4N  40452  pmapojoinN  40467  pl42lem1N  40478  lhp2lt  40500  lhp0lt  40502  lhpn0  40503  lhpexnle  40505  lhpoc2N  40514  lhpocnle  40515  lhpj1  40521  lhpmod2i2  40537  lhpmod6i1  40538  lhprelat3N  40539  ltrnatb  40636  trlcl  40663  trlle  40683  cdleme3c  40729  cdleme7e  40746  cdleme22b  40840  cdlemg12e  41146  cdlemg12g  41148  tendoid  41272  tendo0tp  41288  cdlemk39s-id  41439  tendoex  41474  dia0eldmN  41539  dia2dimlem2  41564  dia2dimlem3  41565  docaclN  41623  doca2N  41625  djajN  41636  dib0  41663  dih0  41779  dih0bN  41780  dih0rn  41783  dih1  41785  dih1rn  41786  dih1cnv  41787  dihmeetlem18N  41823  dih1dimatlem  41828  dihlspsnssN  41831  dihlspsnat  41832  dihatexv  41837  dihglb2  41841  dochcl  41852  doch0  41857  doch1  41858  dochvalr3  41862  doch2val2  41863  dochss  41864  dochocss  41865  dochoc  41866  dochnoncon  41890  djhlj  41900  dihjatc  41916