Theorem hlop 39318

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

Syntax hints:   → wi 4   ∈ wcel 2108  OPcops 39128  OLcol 39130  HLchlt 39306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-ol 39134  df-oml 39135  df-hlat 39307

This theorem is referenced by:  glbconN  39333  glbconNOLD  39334  glbconxN  39335  hlhgt2  39346  hl0lt1N  39347  hl2at  39362  cvrexch  39377  atcvr0eq  39383  lnnat  39384  atle  39393  cvrat4  39400  athgt  39413  1cvrco  39429  1cvratex  39430  1cvrjat  39432  1cvrat  39433  ps-2  39435  llnn0  39473  lplnn0N  39504  llncvrlpln  39515  lvoln0N  39548  lplncvrlvol  39573  dalemkeop  39582  pmapeq0  39723  pmapglb2N  39728  pmapglb2xN  39729  2atm2atN  39742  polval2N  39863  polsubN  39864  pol1N  39867  2polpmapN  39870  2polvalN  39871  poldmj1N  39885  pmapj2N  39886  2polatN  39889  pnonsingN  39890  ispsubcl2N  39904  polsubclN  39909  poml4N  39910  pmapojoinN  39925  pl42lem1N  39936  lhp2lt  39958  lhp0lt  39960  lhpn0  39961  lhpexnle  39963  lhpoc2N  39972  lhpocnle  39973  lhpj1  39979  lhpmod2i2  39995  lhpmod6i1  39996  lhprelat3N  39997  ltrnatb  40094  trlcl  40121  trlle  40141  cdleme3c  40187  cdleme7e  40204  cdleme22b  40298  cdlemg12e  40604  cdlemg12g  40606  tendoid  40730  tendo0tp  40746  cdlemk39s-id  40897  tendoex  40932  dia0eldmN  40997  dia2dimlem2  41022  dia2dimlem3  41023  docaclN  41081  doca2N  41083  djajN  41094  dib0  41121  dih0  41237  dih0bN  41238  dih0rn  41241  dih1  41243  dih1rn  41244  dih1cnv  41245  dihmeetlem18N  41281  dih1dimatlem  41286  dihlspsnssN  41289  dihlspsnat  41290  dihatexv  41295  dihglb2  41299  dochcl  41310  doch0  41315  doch1  41316  dochvalr3  41320  doch2val2  41321  dochss  41322  dochocss  41323  dochoc  41324  dochnoncon  41348  djhlj  41358  dihjatc  41374