Theorem hlop 39343

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

Syntax hints:   → wi 4   ∈ wcel 2105  OPcops 39153  OLcol 39155  HLchlt 39331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-ol 39159  df-oml 39160  df-hlat 39332

This theorem is referenced by:  glbconN  39358  glbconNOLD  39359  glbconxN  39360  hlhgt2  39371  hl0lt1N  39372  hl2at  39387  cvrexch  39402  atcvr0eq  39408  lnnat  39409  atle  39418  cvrat4  39425  athgt  39438  1cvrco  39454  1cvratex  39455  1cvrjat  39457  1cvrat  39458  ps-2  39460  llnn0  39498  lplnn0N  39529  llncvrlpln  39540  lvoln0N  39573  lplncvrlvol  39598  dalemkeop  39607  pmapeq0  39748  pmapglb2N  39753  pmapglb2xN  39754  2atm2atN  39767  polval2N  39888  polsubN  39889  pol1N  39892  2polpmapN  39895  2polvalN  39896  poldmj1N  39910  pmapj2N  39911  2polatN  39914  pnonsingN  39915  ispsubcl2N  39929  polsubclN  39934  poml4N  39935  pmapojoinN  39950  pl42lem1N  39961  lhp2lt  39983  lhp0lt  39985  lhpn0  39986  lhpexnle  39988  lhpoc2N  39997  lhpocnle  39998  lhpj1  40004  lhpmod2i2  40020  lhpmod6i1  40021  lhprelat3N  40022  ltrnatb  40119  trlcl  40146  trlle  40166  cdleme3c  40212  cdleme7e  40229  cdleme22b  40323  cdlemg12e  40629  cdlemg12g  40631  tendoid  40755  tendo0tp  40771  cdlemk39s-id  40922  tendoex  40957  dia0eldmN  41022  dia2dimlem2  41047  dia2dimlem3  41048  docaclN  41106  doca2N  41108  djajN  41119  dib0  41146  dih0  41262  dih0bN  41263  dih0rn  41266  dih1  41268  dih1rn  41269  dih1cnv  41270  dihmeetlem18N  41306  dih1dimatlem  41311  dihlspsnssN  41314  dihlspsnat  41315  dihatexv  41320  dihglb2  41324  dochcl  41335  doch0  41340  doch1  41341  dochvalr3  41345  doch2val2  41346  dochss  41347  dochocss  41348  dochoc  41349  dochnoncon  41373  djhlj  41383  dihjatc  41399