Theorem hlop 37376

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

Syntax hints:   → wi 4   ∈ wcel 2106  OPcops 37186  OLcol 37188  HLchlt 37364

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-ov 7278  df-ol 37192  df-oml 37193  df-hlat 37365

This theorem is referenced by:  glbconN  37391  glbconxN  37392  hlhgt2  37403  hl0lt1N  37404  hl2at  37419  cvrexch  37434  atcvr0eq  37440  lnnat  37441  atle  37450  cvrat4  37457  athgt  37470  1cvrco  37486  1cvratex  37487  1cvrjat  37489  1cvrat  37490  ps-2  37492  llnn0  37530  lplnn0N  37561  llncvrlpln  37572  lvoln0N  37605  lplncvrlvol  37630  dalemkeop  37639  pmapeq0  37780  pmapglb2N  37785  pmapglb2xN  37786  2atm2atN  37799  polval2N  37920  polsubN  37921  pol1N  37924  2polpmapN  37927  2polvalN  37928  poldmj1N  37942  pmapj2N  37943  2polatN  37946  pnonsingN  37947  ispsubcl2N  37961  polsubclN  37966  poml4N  37967  pmapojoinN  37982  pl42lem1N  37993  lhp2lt  38015  lhp0lt  38017  lhpn0  38018  lhpexnle  38020  lhpoc2N  38029  lhpocnle  38030  lhpj1  38036  lhpmod2i2  38052  lhpmod6i1  38053  lhprelat3N  38054  ltrnatb  38151  trlcl  38178  trlle  38198  cdleme3c  38244  cdleme7e  38261  cdleme22b  38355  cdlemg12e  38661  cdlemg12g  38663  tendoid  38787  tendo0tp  38803  cdlemk39s-id  38954  tendoex  38989  dia0eldmN  39054  dia2dimlem2  39079  dia2dimlem3  39080  docaclN  39138  doca2N  39140  djajN  39151  dib0  39178  dih0  39294  dih0bN  39295  dih0rn  39298  dih1  39300  dih1rn  39301  dih1cnv  39302  dihmeetlem18N  39338  dih1dimatlem  39343  dihlspsnssN  39346  dihlspsnat  39347  dihatexv  39352  dihglb2  39356  dochcl  39367  doch0  39372  doch1  39373  dochvalr3  39377  doch2val2  39378  dochss  39379  dochocss  39380  dochoc  39381  dochnoncon  39405  djhlj  39415  dihjatc  39431