Theorem hlop 37596

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

Syntax hints:   → wi 4   ∈ wcel 2105  OPcops 37406  OLcol 37408  HLchlt 37584

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-br 5088  df-iota 6418  df-fv 6474  df-ov 7320  df-ol 37412  df-oml 37413  df-hlat 37585

This theorem is referenced by:  glbconN  37611  glbconNOLD  37612  glbconxN  37613  hlhgt2  37624  hl0lt1N  37625  hl2at  37640  cvrexch  37655  atcvr0eq  37661  lnnat  37662  atle  37671  cvrat4  37678  athgt  37691  1cvrco  37707  1cvratex  37708  1cvrjat  37710  1cvrat  37711  ps-2  37713  llnn0  37751  lplnn0N  37782  llncvrlpln  37793  lvoln0N  37826  lplncvrlvol  37851  dalemkeop  37860  pmapeq0  38001  pmapglb2N  38006  pmapglb2xN  38007  2atm2atN  38020  polval2N  38141  polsubN  38142  pol1N  38145  2polpmapN  38148  2polvalN  38149  poldmj1N  38163  pmapj2N  38164  2polatN  38167  pnonsingN  38168  ispsubcl2N  38182  polsubclN  38187  poml4N  38188  pmapojoinN  38203  pl42lem1N  38214  lhp2lt  38236  lhp0lt  38238  lhpn0  38239  lhpexnle  38241  lhpoc2N  38250  lhpocnle  38251  lhpj1  38257  lhpmod2i2  38273  lhpmod6i1  38274  lhprelat3N  38275  ltrnatb  38372  trlcl  38399  trlle  38419  cdleme3c  38465  cdleme7e  38482  cdleme22b  38576  cdlemg12e  38882  cdlemg12g  38884  tendoid  39008  tendo0tp  39024  cdlemk39s-id  39175  tendoex  39210  dia0eldmN  39275  dia2dimlem2  39300  dia2dimlem3  39301  docaclN  39359  doca2N  39361  djajN  39372  dib0  39399  dih0  39515  dih0bN  39516  dih0rn  39519  dih1  39521  dih1rn  39522  dih1cnv  39523  dihmeetlem18N  39559  dih1dimatlem  39564  dihlspsnssN  39567  dihlspsnat  39568  dihatexv  39573  dihglb2  39577  dochcl  39588  doch0  39593  doch1  39594  dochvalr3  39598  doch2val2  39599  dochss  39600  dochocss  39601  dochoc  39602  dochnoncon  39626  djhlj  39636  dihjatc  39652