Theorem hlop 40387

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  OPcops 40197  OLcol 40199  HLchlt 40375

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-ov 7415  df-ol 40203  df-oml 40204  df-hlat 40376

This theorem is used by:  glbconN  40402  glbconxN  40403  hlhgt2  40414  hl0lt1N  40415  hl2at  40430  cvrexch  40445  atcvr0eq  40451  lnnat  40452  atle  40461  cvrat4  40468  athgt  40481  1cvrco  40497  1cvratex  40498  1cvrjat  40500  1cvrat  40501  ps-2  40503  llnn0  40541  lplnn0N  40572  llncvrlpln  40583  lvoln0N  40616  lplncvrlvol  40641  dalemkeop  40650  pmapeq0  40791  pmapglb2N  40796  pmapglb2xN  40797  2atm2atN  40810  polval2N  40931  polsubN  40932  pol1N  40935  2polpmapN  40938  2polvalN  40939  poldmj1N  40953  pmapj2N  40954  2polatN  40957  pnonsingN  40958  ispsubcl2N  40972  polsubclN  40977  poml4N  40978  pmapojoinN  40993  pl42lem1N  41004  lhp2lt  41026  lhp0lt  41028  lhpn0  41029  lhpexnle  41031  lhpoc2N  41040  lhpocnle  41041  lhpj1  41047  lhpmod2i2  41063  lhpmod6i1  41064  lhprelat3N  41065  ltrnatb  41162  trlcl  41189  trlle  41209  cdleme3c  41255  cdleme7e  41272  cdleme22b  41366  cdlemg12e  41672  cdlemg12g  41674  tendoid  41798  tendo0tp  41814  cdlemk39s-id  41965  tendoex  42000  dia0eldmN  42065  dia2dimlem2  42090  dia2dimlem3  42091  docaclN  42149  doca2N  42151  djajN  42162  dib0  42189  dih0  42305  dih0bN  42306  dih0rn  42309  dih1  42311  dih1rn  42312  dih1cnv  42313  dihmeetlem18N  42349  dih1dimatlem  42354  dihlspsnssN  42357  dihlspsnat  42358  dihatexv  42363  dihglb2  42367  dochcl  42378  doch0  42383  doch1  42384  dochvalr3  42388  doch2val2  42389  dochss  42390  dochocss  42391  dochoc  42392  dochnoncon  42416  djhlj  42426  dihjatc  42442