Theorem hlop 38232

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

Syntax hints:   → wi 4   ∈ wcel 2107  OPcops 38042  OLcol 38044  HLchlt 38220

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-ol 38048  df-oml 38049  df-hlat 38221

This theorem is referenced by:  glbconN  38247  glbconNOLD  38248  glbconxN  38249  hlhgt2  38260  hl0lt1N  38261  hl2at  38276  cvrexch  38291  atcvr0eq  38297  lnnat  38298  atle  38307  cvrat4  38314  athgt  38327  1cvrco  38343  1cvratex  38344  1cvrjat  38346  1cvrat  38347  ps-2  38349  llnn0  38387  lplnn0N  38418  llncvrlpln  38429  lvoln0N  38462  lplncvrlvol  38487  dalemkeop  38496  pmapeq0  38637  pmapglb2N  38642  pmapglb2xN  38643  2atm2atN  38656  polval2N  38777  polsubN  38778  pol1N  38781  2polpmapN  38784  2polvalN  38785  poldmj1N  38799  pmapj2N  38800  2polatN  38803  pnonsingN  38804  ispsubcl2N  38818  polsubclN  38823  poml4N  38824  pmapojoinN  38839  pl42lem1N  38850  lhp2lt  38872  lhp0lt  38874  lhpn0  38875  lhpexnle  38877  lhpoc2N  38886  lhpocnle  38887  lhpj1  38893  lhpmod2i2  38909  lhpmod6i1  38910  lhprelat3N  38911  ltrnatb  39008  trlcl  39035  trlle  39055  cdleme3c  39101  cdleme7e  39118  cdleme22b  39212  cdlemg12e  39518  cdlemg12g  39520  tendoid  39644  tendo0tp  39660  cdlemk39s-id  39811  tendoex  39846  dia0eldmN  39911  dia2dimlem2  39936  dia2dimlem3  39937  docaclN  39995  doca2N  39997  djajN  40008  dib0  40035  dih0  40151  dih0bN  40152  dih0rn  40155  dih1  40157  dih1rn  40158  dih1cnv  40159  dihmeetlem18N  40195  dih1dimatlem  40200  dihlspsnssN  40203  dihlspsnat  40204  dihatexv  40209  dihglb2  40213  dochcl  40224  doch0  40229  doch1  40230  dochvalr3  40234  doch2val2  40235  dochss  40236  dochocss  40237  dochoc  40238  dochnoncon  40262  djhlj  40272  dihjatc  40288