Theorem hlop 40114

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

Syntax hints:   → wi 4   ∈ wcel 2143  OPcops 39924  OLcol 39926  HLchlt 40102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-ol 39930  df-oml 39931  df-hlat 40103

This theorem is referenced by:  glbconN  40129  glbconxN  40130  hlhgt2  40141  hl0lt1N  40142  hl2at  40157  cvrexch  40172  atcvr0eq  40178  lnnat  40179  atle  40188  cvrat4  40195  athgt  40208  1cvrco  40224  1cvratex  40225  1cvrjat  40227  1cvrat  40228  ps-2  40230  llnn0  40268  lplnn0N  40299  llncvrlpln  40310  lvoln0N  40343  lplncvrlvol  40368  dalemkeop  40377  pmapeq0  40518  pmapglb2N  40523  pmapglb2xN  40524  2atm2atN  40537  polval2N  40658  polsubN  40659  pol1N  40662  2polpmapN  40665  2polvalN  40666  poldmj1N  40680  pmapj2N  40681  2polatN  40684  pnonsingN  40685  ispsubcl2N  40699  polsubclN  40704  poml4N  40705  pmapojoinN  40720  pl42lem1N  40731  lhp2lt  40753  lhp0lt  40755  lhpn0  40756  lhpexnle  40758  lhpoc2N  40767  lhpocnle  40768  lhpj1  40774  lhpmod2i2  40790  lhpmod6i1  40791  lhprelat3N  40792  ltrnatb  40889  trlcl  40916  trlle  40936  cdleme3c  40982  cdleme7e  40999  cdleme22b  41093  cdlemg12e  41399  cdlemg12g  41401  tendoid  41525  tendo0tp  41541  cdlemk39s-id  41692  tendoex  41727  dia0eldmN  41792  dia2dimlem2  41817  dia2dimlem3  41818  docaclN  41876  doca2N  41878  djajN  41889  dib0  41916  dih0  42032  dih0bN  42033  dih0rn  42036  dih1  42038  dih1rn  42039  dih1cnv  42040  dihmeetlem18N  42076  dih1dimatlem  42081  dihlspsnssN  42084  dihlspsnat  42085  dihatexv  42090  dihglb2  42094  dochcl  42105  doch0  42110  doch1  42111  dochvalr3  42115  doch2val2  42116  dochss  42117  dochocss  42118  dochoc  42119  dochnoncon  42143  djhlj  42153  dihjatc  42169