Theorem hlop 38221

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

Syntax hints:   → wi 4   ∈ wcel 2107  OPcops 38031  OLcol 38033  HLchlt 38209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6493  df-fv 6549  df-ov 7409  df-ol 38037  df-oml 38038  df-hlat 38210

This theorem is referenced by:  glbconN  38236  glbconNOLD  38237  glbconxN  38238  hlhgt2  38249  hl0lt1N  38250  hl2at  38265  cvrexch  38280  atcvr0eq  38286  lnnat  38287  atle  38296  cvrat4  38303  athgt  38316  1cvrco  38332  1cvratex  38333  1cvrjat  38335  1cvrat  38336  ps-2  38338  llnn0  38376  lplnn0N  38407  llncvrlpln  38418  lvoln0N  38451  lplncvrlvol  38476  dalemkeop  38485  pmapeq0  38626  pmapglb2N  38631  pmapglb2xN  38632  2atm2atN  38645  polval2N  38766  polsubN  38767  pol1N  38770  2polpmapN  38773  2polvalN  38774  poldmj1N  38788  pmapj2N  38789  2polatN  38792  pnonsingN  38793  ispsubcl2N  38807  polsubclN  38812  poml4N  38813  pmapojoinN  38828  pl42lem1N  38839  lhp2lt  38861  lhp0lt  38863  lhpn0  38864  lhpexnle  38866  lhpoc2N  38875  lhpocnle  38876  lhpj1  38882  lhpmod2i2  38898  lhpmod6i1  38899  lhprelat3N  38900  ltrnatb  38997  trlcl  39024  trlle  39044  cdleme3c  39090  cdleme7e  39107  cdleme22b  39201  cdlemg12e  39507  cdlemg12g  39509  tendoid  39633  tendo0tp  39649  cdlemk39s-id  39800  tendoex  39835  dia0eldmN  39900  dia2dimlem2  39925  dia2dimlem3  39926  docaclN  39984  doca2N  39986  djajN  39997  dib0  40024  dih0  40140  dih0bN  40141  dih0rn  40144  dih1  40146  dih1rn  40147  dih1cnv  40148  dihmeetlem18N  40184  dih1dimatlem  40189  dihlspsnssN  40192  dihlspsnat  40193  dihatexv  40198  dihglb2  40202  dochcl  40213  doch0  40218  doch1  40219  dochvalr3  40223  doch2val2  40224  dochss  40225  dochocss  40226  dochoc  40227  dochnoncon  40251  djhlj  40261  dihjatc  40277