Theorem hlop 35170

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

Syntax hints:   → wi 4   ∈ wcel 2139  OPcops 34980  OLcol 34982  HLchlt 35158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6817  df-ol 34986  df-oml 34987  df-hlat 35159

This theorem is referenced by:  glbconN  35184  glbconxN  35185  hlhgt2  35196  hl0lt1N  35197  hl2at  35212  cvrexch  35227  atcvr0eq  35233  lnnat  35234  atle  35243  cvrat4  35250  athgt  35263  1cvrco  35279  1cvratex  35280  1cvrjat  35282  1cvrat  35283  ps-2  35285  llnn0  35323  lplnn0N  35354  llncvrlpln  35365  lvoln0N  35398  lplncvrlvol  35423  dalemkeop  35432  pmapeq0  35573  pmapglb2N  35578  pmapglb2xN  35579  2atm2atN  35592  polval2N  35713  polsubN  35714  pol1N  35717  2polpmapN  35720  2polvalN  35721  poldmj1N  35735  pmapj2N  35736  2polatN  35739  pnonsingN  35740  ispsubcl2N  35754  polsubclN  35759  poml4N  35760  pmapojoinN  35775  pl42lem1N  35786  lhp2lt  35808  lhp0lt  35810  lhpn0  35811  lhpexnle  35813  lhpoc2N  35822  lhpocnle  35823  lhpj1  35829  lhpmod2i2  35845  lhpmod6i1  35846  lhprelat3N  35847  ltrnatb  35944  ltrnmwOLD  35959  trlcl  35972  trlle  35992  cdleme3c  36038  cdleme7e  36055  cdleme22b  36149  cdlemg12e  36455  cdlemg12g  36457  tendoid  36581  tendo0tp  36597  cdlemk39s-id  36748  tendoex  36783  dia0eldmN  36849  dia2dimlem2  36874  dia2dimlem3  36875  docaclN  36933  doca2N  36935  djajN  36946  dib0  36973  dih0  37089  dih0bN  37090  dih0rn  37093  dih1  37095  dih1rn  37096  dih1cnv  37097  dihmeetlem18N  37133  dih1dimatlem  37138  dihlspsnssN  37141  dihlspsnat  37142  dihatexv  37147  dihglb2  37151  dochcl  37162  doch0  37167  doch1  37168  dochvalr3  37172  doch2val2  37173  dochss  37174  dochocss  37175  dochoc  37176  dochnoncon  37200  djhlj  37210  dihjatc  37226