Theorem hlop 39808

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

Syntax hints:   → wi 4   ∈ wcel 2114  OPcops 39618  OLcol 39620  HLchlt 39796

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-ol 39624  df-oml 39625  df-hlat 39797

This theorem is referenced by:  glbconN  39823  glbconxN  39824  hlhgt2  39835  hl0lt1N  39836  hl2at  39851  cvrexch  39866  atcvr0eq  39872  lnnat  39873  atle  39882  cvrat4  39889  athgt  39902  1cvrco  39918  1cvratex  39919  1cvrjat  39921  1cvrat  39922  ps-2  39924  llnn0  39962  lplnn0N  39993  llncvrlpln  40004  lvoln0N  40037  lplncvrlvol  40062  dalemkeop  40071  pmapeq0  40212  pmapglb2N  40217  pmapglb2xN  40218  2atm2atN  40231  polval2N  40352  polsubN  40353  pol1N  40356  2polpmapN  40359  2polvalN  40360  poldmj1N  40374  pmapj2N  40375  2polatN  40378  pnonsingN  40379  ispsubcl2N  40393  polsubclN  40398  poml4N  40399  pmapojoinN  40414  pl42lem1N  40425  lhp2lt  40447  lhp0lt  40449  lhpn0  40450  lhpexnle  40452  lhpoc2N  40461  lhpocnle  40462  lhpj1  40468  lhpmod2i2  40484  lhpmod6i1  40485  lhprelat3N  40486  ltrnatb  40583  trlcl  40610  trlle  40630  cdleme3c  40676  cdleme7e  40693  cdleme22b  40787  cdlemg12e  41093  cdlemg12g  41095  tendoid  41219  tendo0tp  41235  cdlemk39s-id  41386  tendoex  41421  dia0eldmN  41486  dia2dimlem2  41511  dia2dimlem3  41512  docaclN  41570  doca2N  41572  djajN  41583  dib0  41610  dih0  41726  dih0bN  41727  dih0rn  41730  dih1  41732  dih1rn  41733  dih1cnv  41734  dihmeetlem18N  41770  dih1dimatlem  41775  dihlspsnssN  41778  dihlspsnat  41779  dihatexv  41784  dihglb2  41788  dochcl  41799  doch0  41804  doch1  41805  dochvalr3  41809  doch2val2  41810  dochss  41811  dochocss  41812  dochoc  41813  dochnoncon  41837  djhlj  41847  dihjatc  41863