Theorem hlop 39400

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

Syntax hints:   → wi 4   ∈ wcel 2111  OPcops 39210  OLcol 39212  HLchlt 39388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349  df-ol 39216  df-oml 39217  df-hlat 39389

This theorem is referenced by:  glbconN  39415  glbconxN  39416  hlhgt2  39427  hl0lt1N  39428  hl2at  39443  cvrexch  39458  atcvr0eq  39464  lnnat  39465  atle  39474  cvrat4  39481  athgt  39494  1cvrco  39510  1cvratex  39511  1cvrjat  39513  1cvrat  39514  ps-2  39516  llnn0  39554  lplnn0N  39585  llncvrlpln  39596  lvoln0N  39629  lplncvrlvol  39654  dalemkeop  39663  pmapeq0  39804  pmapglb2N  39809  pmapglb2xN  39810  2atm2atN  39823  polval2N  39944  polsubN  39945  pol1N  39948  2polpmapN  39951  2polvalN  39952  poldmj1N  39966  pmapj2N  39967  2polatN  39970  pnonsingN  39971  ispsubcl2N  39985  polsubclN  39990  poml4N  39991  pmapojoinN  40006  pl42lem1N  40017  lhp2lt  40039  lhp0lt  40041  lhpn0  40042  lhpexnle  40044  lhpoc2N  40053  lhpocnle  40054  lhpj1  40060  lhpmod2i2  40076  lhpmod6i1  40077  lhprelat3N  40078  ltrnatb  40175  trlcl  40202  trlle  40222  cdleme3c  40268  cdleme7e  40285  cdleme22b  40379  cdlemg12e  40685  cdlemg12g  40687  tendoid  40811  tendo0tp  40827  cdlemk39s-id  40978  tendoex  41013  dia0eldmN  41078  dia2dimlem2  41103  dia2dimlem3  41104  docaclN  41162  doca2N  41164  djajN  41175  dib0  41202  dih0  41318  dih0bN  41319  dih0rn  41322  dih1  41324  dih1rn  41325  dih1cnv  41326  dihmeetlem18N  41362  dih1dimatlem  41367  dihlspsnssN  41370  dihlspsnat  41371  dihatexv  41376  dihglb2  41380  dochcl  41391  doch0  41396  doch1  41397  dochvalr3  41401  doch2val2  41402  dochss  41403  dochocss  41404  dochoc  41405  dochnoncon  41429  djhlj  41439  dihjatc  41455