Theorem hlop 38961

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

Syntax hints:   → wi 4   ∈ wcel 2098  OPcops 38771  OLcol 38773  HLchlt 38949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-iota 6501  df-fv 6557  df-ov 7422  df-ol 38777  df-oml 38778  df-hlat 38950

This theorem is referenced by:  glbconN  38976  glbconNOLD  38977  glbconxN  38978  hlhgt2  38989  hl0lt1N  38990  hl2at  39005  cvrexch  39020  atcvr0eq  39026  lnnat  39027  atle  39036  cvrat4  39043  athgt  39056  1cvrco  39072  1cvratex  39073  1cvrjat  39075  1cvrat  39076  ps-2  39078  llnn0  39116  lplnn0N  39147  llncvrlpln  39158  lvoln0N  39191  lplncvrlvol  39216  dalemkeop  39225  pmapeq0  39366  pmapglb2N  39371  pmapglb2xN  39372  2atm2atN  39385  polval2N  39506  polsubN  39507  pol1N  39510  2polpmapN  39513  2polvalN  39514  poldmj1N  39528  pmapj2N  39529  2polatN  39532  pnonsingN  39533  ispsubcl2N  39547  polsubclN  39552  poml4N  39553  pmapojoinN  39568  pl42lem1N  39579  lhp2lt  39601  lhp0lt  39603  lhpn0  39604  lhpexnle  39606  lhpoc2N  39615  lhpocnle  39616  lhpj1  39622  lhpmod2i2  39638  lhpmod6i1  39639  lhprelat3N  39640  ltrnatb  39737  trlcl  39764  trlle  39784  cdleme3c  39830  cdleme7e  39847  cdleme22b  39941  cdlemg12e  40247  cdlemg12g  40249  tendoid  40373  tendo0tp  40389  cdlemk39s-id  40540  tendoex  40575  dia0eldmN  40640  dia2dimlem2  40665  dia2dimlem3  40666  docaclN  40724  doca2N  40726  djajN  40737  dib0  40764  dih0  40880  dih0bN  40881  dih0rn  40884  dih1  40886  dih1rn  40887  dih1cnv  40888  dihmeetlem18N  40924  dih1dimatlem  40929  dihlspsnssN  40932  dihlspsnat  40933  dihatexv  40938  dihglb2  40942  dochcl  40953  doch0  40958  doch1  40959  dochvalr3  40963  doch2val2  40964  dochss  40965  dochocss  40966  dochoc  40967  dochnoncon  40991  djhlj  41001  dihjatc  41017