Theorem hlop 40512

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  OPcops 40322  OLcol 40324  HLchlt 40500

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-ol 40328  df-oml 40329  df-hlat 40501

This theorem is used by:  glbconN  40527  glbconxN  40528  hlhgt2  40539  hl0lt1N  40540  hl2at  40555  cvrexch  40570  atcvr0eq  40576  lnnat  40577  atle  40586  cvrat4  40593  athgt  40606  1cvrco  40622  1cvratex  40623  1cvrjat  40625  1cvrat  40626  ps-2  40628  llnn0  40666  lplnn0N  40697  llncvrlpln  40708  lvoln0N  40741  lplncvrlvol  40766  dalemkeop  40775  pmapeq0  40916  pmapglb2N  40921  pmapglb2xN  40922  2atm2atN  40935  polval2N  41056  polsubN  41057  pol1N  41060  2polpmapN  41063  2polvalN  41064  poldmj1N  41078  pmapj2N  41079  2polatN  41082  pnonsingN  41083  ispsubcl2N  41097  polsubclN  41102  poml4N  41103  pmapojoinN  41118  pl42lem1N  41129  lhp2lt  41151  lhp0lt  41153  lhpn0  41154  lhpexnle  41156  lhpoc2N  41165  lhpocnle  41166  lhpj1  41172  lhpmod2i2  41188  lhpmod6i1  41189  lhprelat3N  41190  ltrnatb  41287  trlcl  41314  trlle  41334  cdleme3c  41380  cdleme7e  41397  cdleme22b  41491  cdlemg12e  41797  cdlemg12g  41799  tendoid  41923  tendo0tp  41939  cdlemk39s-id  42090  tendoex  42125  dia0eldmN  42190  dia2dimlem2  42215  dia2dimlem3  42216  docaclN  42274  doca2N  42276  djajN  42287  dib0  42314  dih0  42430  dih0bN  42431  dih0rn  42434  dih1  42436  dih1rn  42437  dih1cnv  42438  dihmeetlem18N  42474  dih1dimatlem  42479  dihlspsnssN  42482  dihlspsnat  42483  dihatexv  42488  dihglb2  42492  dochcl  42503  doch0  42508  doch1  42509  dochvalr3  42513  doch2val2  42514  dochss  42515  dochocss  42516  dochoc  42517  dochnoncon  42541  djhlj  42551  dihjatc  42567