Theorem hlop 37303

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

Syntax hints:   → wi 4   ∈ wcel 2108  OPcops 37113  OLcol 37115  HLchlt 37291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-ol 37119  df-oml 37120  df-hlat 37292

This theorem is referenced by:  glbconN  37318  glbconxN  37319  hlhgt2  37330  hl0lt1N  37331  hl2at  37346  cvrexch  37361  atcvr0eq  37367  lnnat  37368  atle  37377  cvrat4  37384  athgt  37397  1cvrco  37413  1cvratex  37414  1cvrjat  37416  1cvrat  37417  ps-2  37419  llnn0  37457  lplnn0N  37488  llncvrlpln  37499  lvoln0N  37532  lplncvrlvol  37557  dalemkeop  37566  pmapeq0  37707  pmapglb2N  37712  pmapglb2xN  37713  2atm2atN  37726  polval2N  37847  polsubN  37848  pol1N  37851  2polpmapN  37854  2polvalN  37855  poldmj1N  37869  pmapj2N  37870  2polatN  37873  pnonsingN  37874  ispsubcl2N  37888  polsubclN  37893  poml4N  37894  pmapojoinN  37909  pl42lem1N  37920  lhp2lt  37942  lhp0lt  37944  lhpn0  37945  lhpexnle  37947  lhpoc2N  37956  lhpocnle  37957  lhpj1  37963  lhpmod2i2  37979  lhpmod6i1  37980  lhprelat3N  37981  ltrnatb  38078  trlcl  38105  trlle  38125  cdleme3c  38171  cdleme7e  38188  cdleme22b  38282  cdlemg12e  38588  cdlemg12g  38590  tendoid  38714  tendo0tp  38730  cdlemk39s-id  38881  tendoex  38916  dia0eldmN  38981  dia2dimlem2  39006  dia2dimlem3  39007  docaclN  39065  doca2N  39067  djajN  39078  dib0  39105  dih0  39221  dih0bN  39222  dih0rn  39225  dih1  39227  dih1rn  39228  dih1cnv  39229  dihmeetlem18N  39265  dih1dimatlem  39270  dihlspsnssN  39273  dihlspsnat  39274  dihatexv  39279  dihglb2  39283  dochcl  39294  doch0  39299  doch1  39300  dochvalr3  39304  doch2val2  39305  dochss  39306  dochocss  39307  dochoc  39308  dochnoncon  39332  djhlj  39342  dihjatc  39358