Theorem hlop 39998

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

Syntax hints:   → wi 4   ∈ wcel 2145  OPcops 39808  OLcol 39810  HLchlt 39986

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-ov 7403  df-ol 39814  df-oml 39815  df-hlat 39987

This theorem is referenced by:  glbconN  40013  glbconxN  40014  hlhgt2  40025  hl0lt1N  40026  hl2at  40041  cvrexch  40056  atcvr0eq  40062  lnnat  40063  atle  40072  cvrat4  40079  athgt  40092  1cvrco  40108  1cvratex  40109  1cvrjat  40111  1cvrat  40112  ps-2  40114  llnn0  40152  lplnn0N  40183  llncvrlpln  40194  lvoln0N  40227  lplncvrlvol  40252  dalemkeop  40261  pmapeq0  40402  pmapglb2N  40407  pmapglb2xN  40408  2atm2atN  40421  polval2N  40542  polsubN  40543  pol1N  40546  2polpmapN  40549  2polvalN  40550  poldmj1N  40564  pmapj2N  40565  2polatN  40568  pnonsingN  40569  ispsubcl2N  40583  polsubclN  40588  poml4N  40589  pmapojoinN  40604  pl42lem1N  40615  lhp2lt  40637  lhp0lt  40639  lhpn0  40640  lhpexnle  40642  lhpoc2N  40651  lhpocnle  40652  lhpj1  40658  lhpmod2i2  40674  lhpmod6i1  40675  lhprelat3N  40676  ltrnatb  40773  trlcl  40800  trlle  40820  cdleme3c  40866  cdleme7e  40883  cdleme22b  40977  cdlemg12e  41283  cdlemg12g  41285  tendoid  41409  tendo0tp  41425  cdlemk39s-id  41576  tendoex  41611  dia0eldmN  41676  dia2dimlem2  41701  dia2dimlem3  41702  docaclN  41760  doca2N  41762  djajN  41773  dib0  41800  dih0  41916  dih0bN  41917  dih0rn  41920  dih1  41922  dih1rn  41923  dih1cnv  41924  dihmeetlem18N  41960  dih1dimatlem  41965  dihlspsnssN  41968  dihlspsnat  41969  dihatexv  41974  dihglb2  41978  dochcl  41989  doch0  41994  doch1  41995  dochvalr3  41999  doch2val2  42000  dochss  42001  dochocss  42002  dochoc  42003  dochnoncon  42027  djhlj  42037  dihjatc  42053