Theorem hlop 33667

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

Syntax hints:   → wi 4   ∈ wcel 1977  OPcops 33477  OLcol 33479  HLchlt 33655

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-ol 33483  df-oml 33484  df-hlat 33656

This theorem is referenced by:  glbconN  33681  glbconxN  33682  hlhgt2  33693  hl0lt1N  33694  hl2at  33709  cvrexch  33724  atcvr0eq  33730  lnnat  33731  atle  33740  cvrat4  33747  athgt  33760  1cvrco  33776  1cvratex  33777  1cvrjat  33779  1cvrat  33780  ps-2  33782  llnn0  33820  lplnn0N  33851  llncvrlpln  33862  lvoln0N  33895  lplncvrlvol  33920  dalemkeop  33929  pmapeq0  34070  pmapglb2N  34075  pmapglb2xN  34076  2atm2atN  34089  polval2N  34210  polsubN  34211  pol1N  34214  2polpmapN  34217  2polvalN  34218  poldmj1N  34232  pmapj2N  34233  2polatN  34236  pnonsingN  34237  ispsubcl2N  34251  polsubclN  34256  poml4N  34257  pmapojoinN  34272  pl42lem1N  34283  lhp2lt  34305  lhp0lt  34307  lhpn0  34308  lhpexnle  34310  lhpoc2N  34319  lhpocnle  34320  lhpj1  34326  lhpmod2i2  34342  lhpmod6i1  34343  lhprelat3N  34344  ltrnatb  34441  ltrnmwOLD  34456  trlcl  34469  trlle  34489  cdleme3c  34535  cdleme7e  34552  cdleme22b  34647  cdlemg12e  34953  cdlemg12g  34955  tendoid  35079  tendo0tp  35095  cdlemk39s-id  35246  tendoex  35281  dia0eldmN  35347  dia2dimlem2  35372  dia2dimlem3  35373  docaclN  35431  doca2N  35433  djajN  35444  dib0  35471  dih0  35587  dih0bN  35588  dih0rn  35591  dih1  35593  dih1rn  35594  dih1cnv  35595  dihmeetlem18N  35631  dih1dimatlem  35636  dihlspsnssN  35639  dihlspsnat  35640  dihatexv  35645  dihglb2  35649  dochcl  35660  doch0  35665  doch1  35666  dochvalr3  35670  doch2val2  35671  dochss  35672  dochocss  35673  dochoc  35674  dochnoncon  35698  djhlj  35708  dihjatc  35724