Theorem hlop 35160

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

Syntax hints:   → wi 4   ∈ wcel 2157  OPcops 34970  OLcol 34972  HLchlt 35148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-iota 6073  df-fv 6118  df-ov 6886  df-ol 34976  df-oml 34977  df-hlat 35149

This theorem is referenced by:  glbconN  35175  glbconxN  35176  hlhgt2  35187  hl0lt1N  35188  hl2at  35203  cvrexch  35218  atcvr0eq  35224  lnnat  35225  atle  35234  cvrat4  35241  athgt  35254  1cvrco  35270  1cvratex  35271  1cvrjat  35273  1cvrat  35274  ps-2  35276  llnn0  35314  lplnn0N  35345  llncvrlpln  35356  lvoln0N  35389  lplncvrlvol  35414  dalemkeop  35423  pmapeq0  35564  pmapglb2N  35569  pmapglb2xN  35570  2atm2atN  35583  polval2N  35704  polsubN  35705  pol1N  35708  2polpmapN  35711  2polvalN  35712  poldmj1N  35726  pmapj2N  35727  2polatN  35730  pnonsingN  35731  ispsubcl2N  35745  polsubclN  35750  poml4N  35751  pmapojoinN  35766  pl42lem1N  35777  lhp2lt  35799  lhp0lt  35801  lhpn0  35802  lhpexnle  35804  lhpoc2N  35813  lhpocnle  35814  lhpj1  35820  lhpmod2i2  35836  lhpmod6i1  35837  lhprelat3N  35838  ltrnatb  35935  trlcl  35962  trlle  35982  cdleme3c  36028  cdleme7e  36045  cdleme22b  36139  cdlemg12e  36445  cdlemg12g  36447  tendoid  36571  tendo0tp  36587  cdlemk39s-id  36738  tendoex  36773  dia0eldmN  36838  dia2dimlem2  36863  dia2dimlem3  36864  docaclN  36922  doca2N  36924  djajN  36935  dib0  36962  dih0  37078  dih0bN  37079  dih0rn  37082  dih1  37084  dih1rn  37085  dih1cnv  37086  dihmeetlem18N  37122  dih1dimatlem  37127  dihlspsnssN  37130  dihlspsnat  37131  dihatexv  37136  dihglb2  37140  dochcl  37151  doch0  37156  doch1  37157  dochvalr3  37161  doch2val2  37162  dochss  37163  dochocss  37164  dochoc  37165  dochnoncon  37189  djhlj  37199  dihjatc  37215