Theorem hlop 39355

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

Syntax hints:   → wi 4   ∈ wcel 2109  OPcops 39165  OLcol 39167  HLchlt 39343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-ol 39171  df-oml 39172  df-hlat 39344

This theorem is referenced by:  glbconN  39370  glbconNOLD  39371  glbconxN  39372  hlhgt2  39383  hl0lt1N  39384  hl2at  39399  cvrexch  39414  atcvr0eq  39420  lnnat  39421  atle  39430  cvrat4  39437  athgt  39450  1cvrco  39466  1cvratex  39467  1cvrjat  39469  1cvrat  39470  ps-2  39472  llnn0  39510  lplnn0N  39541  llncvrlpln  39552  lvoln0N  39585  lplncvrlvol  39610  dalemkeop  39619  pmapeq0  39760  pmapglb2N  39765  pmapglb2xN  39766  2atm2atN  39779  polval2N  39900  polsubN  39901  pol1N  39904  2polpmapN  39907  2polvalN  39908  poldmj1N  39922  pmapj2N  39923  2polatN  39926  pnonsingN  39927  ispsubcl2N  39941  polsubclN  39946  poml4N  39947  pmapojoinN  39962  pl42lem1N  39973  lhp2lt  39995  lhp0lt  39997  lhpn0  39998  lhpexnle  40000  lhpoc2N  40009  lhpocnle  40010  lhpj1  40016  lhpmod2i2  40032  lhpmod6i1  40033  lhprelat3N  40034  ltrnatb  40131  trlcl  40158  trlle  40178  cdleme3c  40224  cdleme7e  40241  cdleme22b  40335  cdlemg12e  40641  cdlemg12g  40643  tendoid  40767  tendo0tp  40783  cdlemk39s-id  40934  tendoex  40969  dia0eldmN  41034  dia2dimlem2  41059  dia2dimlem3  41060  docaclN  41118  doca2N  41120  djajN  41131  dib0  41158  dih0  41274  dih0bN  41275  dih0rn  41278  dih1  41280  dih1rn  41281  dih1cnv  41282  dihmeetlem18N  41318  dih1dimatlem  41323  dihlspsnssN  41326  dihlspsnat  41327  dihatexv  41332  dihglb2  41336  dochcl  41347  doch0  41352  doch1  41353  dochvalr3  41357  doch2val2  41358  dochss  41359  dochocss  41360  dochoc  41361  dochnoncon  41385  djhlj  41395  dihjatc  41411