Theorem hlop 40622

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  OPcops 40432  OLcol 40434  HLchlt 40610

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6515  df-fv 6569  df-ov 7449  df-ol 40438  df-oml 40439  df-hlat 40611

This theorem is used by:  glbconN  40637  glbconxN  40638  hlhgt2  40649  hl0lt1N  40650  hl2at  40665  cvrexch  40680  atcvr0eq  40686  lnnat  40687  atle  40696  cvrat4  40703  athgt  40716  1cvrco  40732  1cvratex  40733  1cvrjat  40735  1cvrat  40736  ps-2  40738  llnn0  40776  lplnn0N  40807  llncvrlpln  40818  lvoln0N  40851  lplncvrlvol  40876  dalemkeop  40885  pmapeq0  41026  pmapglb2N  41031  pmapglb2xN  41032  2atm2atN  41045  polval2N  41166  polsubN  41167  pol1N  41170  2polpmapN  41173  2polvalN  41174  poldmj1N  41188  pmapj2N  41189  2polatN  41192  pnonsingN  41193  ispsubcl2N  41207  polsubclN  41212  poml4N  41213  pmapojoinN  41228  pl42lem1N  41239  lhp2lt  41261  lhp0lt  41263  lhpn0  41264  lhpexnle  41266  lhpoc2N  41275  lhpocnle  41276  lhpj1  41282  lhpmod2i2  41298  lhpmod6i1  41299  lhprelat3N  41300  ltrnatb  41397  trlcl  41424  trlle  41444  cdleme3c  41490  cdleme7e  41507  cdleme22b  41601  cdlemg12e  41907  cdlemg12g  41909  tendoid  42033  tendo0tp  42049  cdlemk39s-id  42200  tendoex  42235  dia0eldmN  42300  dia2dimlem2  42325  dia2dimlem3  42326  docaclN  42384  doca2N  42386  djajN  42397  dib0  42424  dih0  42540  dih0bN  42541  dih0rn  42544  dih1  42546  dih1rn  42547  dih1cnv  42548  dihmeetlem18N  42584  dih1dimatlem  42589  dihlspsnssN  42592  dihlspsnat  42593  dihatexv  42598  dihglb2  42602  dochcl  42613  doch0  42618  doch1  42619  dochvalr3  42623  doch2val2  42624  dochss  42625  dochocss  42626  dochoc  42627  dochnoncon  42651  djhlj  42661  dihjatc  42677