Theorem hlop 39732

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

Syntax hints:   → wi 4   ∈ wcel 2114  OPcops 39542  OLcol 39544  HLchlt 39720

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-ol 39548  df-oml 39549  df-hlat 39721

This theorem is referenced by:  glbconN  39747  glbconxN  39748  hlhgt2  39759  hl0lt1N  39760  hl2at  39775  cvrexch  39790  atcvr0eq  39796  lnnat  39797  atle  39806  cvrat4  39813  athgt  39826  1cvrco  39842  1cvratex  39843  1cvrjat  39845  1cvrat  39846  ps-2  39848  llnn0  39886  lplnn0N  39917  llncvrlpln  39928  lvoln0N  39961  lplncvrlvol  39986  dalemkeop  39995  pmapeq0  40136  pmapglb2N  40141  pmapglb2xN  40142  2atm2atN  40155  polval2N  40276  polsubN  40277  pol1N  40280  2polpmapN  40283  2polvalN  40284  poldmj1N  40298  pmapj2N  40299  2polatN  40302  pnonsingN  40303  ispsubcl2N  40317  polsubclN  40322  poml4N  40323  pmapojoinN  40338  pl42lem1N  40349  lhp2lt  40371  lhp0lt  40373  lhpn0  40374  lhpexnle  40376  lhpoc2N  40385  lhpocnle  40386  lhpj1  40392  lhpmod2i2  40408  lhpmod6i1  40409  lhprelat3N  40410  ltrnatb  40507  trlcl  40534  trlle  40554  cdleme3c  40600  cdleme7e  40617  cdleme22b  40711  cdlemg12e  41017  cdlemg12g  41019  tendoid  41143  tendo0tp  41159  cdlemk39s-id  41310  tendoex  41345  dia0eldmN  41410  dia2dimlem2  41435  dia2dimlem3  41436  docaclN  41494  doca2N  41496  djajN  41507  dib0  41534  dih0  41650  dih0bN  41651  dih0rn  41654  dih1  41656  dih1rn  41657  dih1cnv  41658  dihmeetlem18N  41694  dih1dimatlem  41699  dihlspsnssN  41702  dihlspsnat  41703  dihatexv  41708  dihglb2  41712  dochcl  41723  doch0  41728  doch1  41729  dochvalr3  41733  doch2val2  41734  dochss  41735  dochocss  41736  dochoc  41737  dochnoncon  41761  djhlj  41771  dihjatc  41787