Theorem hlop 39950

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

Syntax hints:   → wi 4   ∈ wcel 2141  OPcops 39760  OLcol 39762  HLchlt 39938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-ov 7395  df-ol 39766  df-oml 39767  df-hlat 39939

This theorem is referenced by:  glbconN  39965  glbconxN  39966  hlhgt2  39977  hl0lt1N  39978  hl2at  39993  cvrexch  40008  atcvr0eq  40014  lnnat  40015  atle  40024  cvrat4  40031  athgt  40044  1cvrco  40060  1cvratex  40061  1cvrjat  40063  1cvrat  40064  ps-2  40066  llnn0  40104  lplnn0N  40135  llncvrlpln  40146  lvoln0N  40179  lplncvrlvol  40204  dalemkeop  40213  pmapeq0  40354  pmapglb2N  40359  pmapglb2xN  40360  2atm2atN  40373  polval2N  40494  polsubN  40495  pol1N  40498  2polpmapN  40501  2polvalN  40502  poldmj1N  40516  pmapj2N  40517  2polatN  40520  pnonsingN  40521  ispsubcl2N  40535  polsubclN  40540  poml4N  40541  pmapojoinN  40556  pl42lem1N  40567  lhp2lt  40589  lhp0lt  40591  lhpn0  40592  lhpexnle  40594  lhpoc2N  40603  lhpocnle  40604  lhpj1  40610  lhpmod2i2  40626  lhpmod6i1  40627  lhprelat3N  40628  ltrnatb  40725  trlcl  40752  trlle  40772  cdleme3c  40818  cdleme7e  40835  cdleme22b  40929  cdlemg12e  41235  cdlemg12g  41237  tendoid  41361  tendo0tp  41377  cdlemk39s-id  41528  tendoex  41563  dia0eldmN  41628  dia2dimlem2  41653  dia2dimlem3  41654  docaclN  41712  doca2N  41714  djajN  41725  dib0  41752  dih0  41868  dih0bN  41869  dih0rn  41872  dih1  41874  dih1rn  41875  dih1cnv  41876  dihmeetlem18N  41912  dih1dimatlem  41917  dihlspsnssN  41920  dihlspsnat  41921  dihatexv  41926  dihglb2  41930  dochcl  41941  doch0  41946  doch1  41947  dochvalr3  41951  doch2val2  41952  dochss  41953  dochocss  41954  dochoc  41955  dochnoncon  41979  djhlj  41989  dihjatc  42005