Theorem hlop 36513

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

Syntax hints:   → wi 4   ∈ wcel 2114  OPcops 36323  OLcol 36325  HLchlt 36501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159  df-ol 36329  df-oml 36330  df-hlat 36502

This theorem is referenced by:  glbconN  36528  glbconxN  36529  hlhgt2  36540  hl0lt1N  36541  hl2at  36556  cvrexch  36571  atcvr0eq  36577  lnnat  36578  atle  36587  cvrat4  36594  athgt  36607  1cvrco  36623  1cvratex  36624  1cvrjat  36626  1cvrat  36627  ps-2  36629  llnn0  36667  lplnn0N  36698  llncvrlpln  36709  lvoln0N  36742  lplncvrlvol  36767  dalemkeop  36776  pmapeq0  36917  pmapglb2N  36922  pmapglb2xN  36923  2atm2atN  36936  polval2N  37057  polsubN  37058  pol1N  37061  2polpmapN  37064  2polvalN  37065  poldmj1N  37079  pmapj2N  37080  2polatN  37083  pnonsingN  37084  ispsubcl2N  37098  polsubclN  37103  poml4N  37104  pmapojoinN  37119  pl42lem1N  37130  lhp2lt  37152  lhp0lt  37154  lhpn0  37155  lhpexnle  37157  lhpoc2N  37166  lhpocnle  37167  lhpj1  37173  lhpmod2i2  37189  lhpmod6i1  37190  lhprelat3N  37191  ltrnatb  37288  trlcl  37315  trlle  37335  cdleme3c  37381  cdleme7e  37398  cdleme22b  37492  cdlemg12e  37798  cdlemg12g  37800  tendoid  37924  tendo0tp  37940  cdlemk39s-id  38091  tendoex  38126  dia0eldmN  38191  dia2dimlem2  38216  dia2dimlem3  38217  docaclN  38275  doca2N  38277  djajN  38288  dib0  38315  dih0  38431  dih0bN  38432  dih0rn  38435  dih1  38437  dih1rn  38438  dih1cnv  38439  dihmeetlem18N  38475  dih1dimatlem  38480  dihlspsnssN  38483  dihlspsnat  38484  dihatexv  38489  dihglb2  38493  dochcl  38504  doch0  38509  doch1  38510  dochvalr3  38514  doch2val2  38515  dochss  38516  dochocss  38517  dochoc  38518  dochnoncon  38542  djhlj  38552  dihjatc  38568