Theorem hlop 34129

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

Syntax hints:   → wi 4   ∈ wcel 1987  OPcops 33939  OLcol 33941  HLchlt 34117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-iota 5810  df-fv 5855  df-ov 6607  df-ol 33945  df-oml 33946  df-hlat 34118

This theorem is referenced by:  glbconN  34143  glbconxN  34144  hlhgt2  34155  hl0lt1N  34156  hl2at  34171  cvrexch  34186  atcvr0eq  34192  lnnat  34193  atle  34202  cvrat4  34209  athgt  34222  1cvrco  34238  1cvratex  34239  1cvrjat  34241  1cvrat  34242  ps-2  34244  llnn0  34282  lplnn0N  34313  llncvrlpln  34324  lvoln0N  34357  lplncvrlvol  34382  dalemkeop  34391  pmapeq0  34532  pmapglb2N  34537  pmapglb2xN  34538  2atm2atN  34551  polval2N  34672  polsubN  34673  pol1N  34676  2polpmapN  34679  2polvalN  34680  poldmj1N  34694  pmapj2N  34695  2polatN  34698  pnonsingN  34699  ispsubcl2N  34713  polsubclN  34718  poml4N  34719  pmapojoinN  34734  pl42lem1N  34745  lhp2lt  34767  lhp0lt  34769  lhpn0  34770  lhpexnle  34772  lhpoc2N  34781  lhpocnle  34782  lhpj1  34788  lhpmod2i2  34804  lhpmod6i1  34805  lhprelat3N  34806  ltrnatb  34903  ltrnmwOLD  34918  trlcl  34931  trlle  34951  cdleme3c  34997  cdleme7e  35014  cdleme22b  35109  cdlemg12e  35415  cdlemg12g  35417  tendoid  35541  tendo0tp  35557  cdlemk39s-id  35708  tendoex  35743  dia0eldmN  35809  dia2dimlem2  35834  dia2dimlem3  35835  docaclN  35893  doca2N  35895  djajN  35906  dib0  35933  dih0  36049  dih0bN  36050  dih0rn  36053  dih1  36055  dih1rn  36056  dih1cnv  36057  dihmeetlem18N  36093  dih1dimatlem  36098  dihlspsnssN  36101  dihlspsnat  36102  dihatexv  36107  dihglb2  36111  dochcl  36122  doch0  36127  doch1  36128  dochvalr3  36132  doch2val2  36133  dochss  36134  dochocss  36135  dochoc  36136  dochnoncon  36160  djhlj  36170  dihjatc  36186