Theorem hlop 36658

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

Syntax hints:   → wi 4   ∈ wcel 2111  OPcops 36468  OLcol 36470  HLchlt 36646

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-ol 36474  df-oml 36475  df-hlat 36647

This theorem is referenced by:  glbconN  36673  glbconxN  36674  hlhgt2  36685  hl0lt1N  36686  hl2at  36701  cvrexch  36716  atcvr0eq  36722  lnnat  36723  atle  36732  cvrat4  36739  athgt  36752  1cvrco  36768  1cvratex  36769  1cvrjat  36771  1cvrat  36772  ps-2  36774  llnn0  36812  lplnn0N  36843  llncvrlpln  36854  lvoln0N  36887  lplncvrlvol  36912  dalemkeop  36921  pmapeq0  37062  pmapglb2N  37067  pmapglb2xN  37068  2atm2atN  37081  polval2N  37202  polsubN  37203  pol1N  37206  2polpmapN  37209  2polvalN  37210  poldmj1N  37224  pmapj2N  37225  2polatN  37228  pnonsingN  37229  ispsubcl2N  37243  polsubclN  37248  poml4N  37249  pmapojoinN  37264  pl42lem1N  37275  lhp2lt  37297  lhp0lt  37299  lhpn0  37300  lhpexnle  37302  lhpoc2N  37311  lhpocnle  37312  lhpj1  37318  lhpmod2i2  37334  lhpmod6i1  37335  lhprelat3N  37336  ltrnatb  37433  trlcl  37460  trlle  37480  cdleme3c  37526  cdleme7e  37543  cdleme22b  37637  cdlemg12e  37943  cdlemg12g  37945  tendoid  38069  tendo0tp  38085  cdlemk39s-id  38236  tendoex  38271  dia0eldmN  38336  dia2dimlem2  38361  dia2dimlem3  38362  docaclN  38420  doca2N  38422  djajN  38433  dib0  38460  dih0  38576  dih0bN  38577  dih0rn  38580  dih1  38582  dih1rn  38583  dih1cnv  38584  dihmeetlem18N  38620  dih1dimatlem  38625  dihlspsnssN  38628  dihlspsnat  38629  dihatexv  38634  dihglb2  38638  dochcl  38649  doch0  38654  doch1  38655  dochvalr3  38659  doch2val2  38660  dochss  38661  dochocss  38662  dochoc  38663  dochnoncon  38687  djhlj  38697  dihjatc  38713