Theorem hlop 39618

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

Syntax hints:   → wi 4   ∈ wcel 2113  OPcops 39428  OLcol 39430  HLchlt 39606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-ol 39434  df-oml 39435  df-hlat 39607

This theorem is referenced by:  glbconN  39633  glbconxN  39634  hlhgt2  39645  hl0lt1N  39646  hl2at  39661  cvrexch  39676  atcvr0eq  39682  lnnat  39683  atle  39692  cvrat4  39699  athgt  39712  1cvrco  39728  1cvratex  39729  1cvrjat  39731  1cvrat  39732  ps-2  39734  llnn0  39772  lplnn0N  39803  llncvrlpln  39814  lvoln0N  39847  lplncvrlvol  39872  dalemkeop  39881  pmapeq0  40022  pmapglb2N  40027  pmapglb2xN  40028  2atm2atN  40041  polval2N  40162  polsubN  40163  pol1N  40166  2polpmapN  40169  2polvalN  40170  poldmj1N  40184  pmapj2N  40185  2polatN  40188  pnonsingN  40189  ispsubcl2N  40203  polsubclN  40208  poml4N  40209  pmapojoinN  40224  pl42lem1N  40235  lhp2lt  40257  lhp0lt  40259  lhpn0  40260  lhpexnle  40262  lhpoc2N  40271  lhpocnle  40272  lhpj1  40278  lhpmod2i2  40294  lhpmod6i1  40295  lhprelat3N  40296  ltrnatb  40393  trlcl  40420  trlle  40440  cdleme3c  40486  cdleme7e  40503  cdleme22b  40597  cdlemg12e  40903  cdlemg12g  40905  tendoid  41029  tendo0tp  41045  cdlemk39s-id  41196  tendoex  41231  dia0eldmN  41296  dia2dimlem2  41321  dia2dimlem3  41322  docaclN  41380  doca2N  41382  djajN  41393  dib0  41420  dih0  41536  dih0bN  41537  dih0rn  41540  dih1  41542  dih1rn  41543  dih1cnv  41544  dihmeetlem18N  41580  dih1dimatlem  41585  dihlspsnssN  41588  dihlspsnat  41589  dihatexv  41594  dihglb2  41598  dochcl  41609  doch0  41614  doch1  41615  dochvalr3  41619  doch2val2  41620  dochss  41621  dochocss  41622  dochoc  41623  dochnoncon  41647  djhlj  41657  dihjatc  41673