Theorem hlop 40177

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  OPcops 39987  OLcol 39989  HLchlt 40165

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426  df-ol 39993  df-oml 39994  df-hlat 40166

This theorem is used by:  glbconN  40192  glbconxN  40193  hlhgt2  40204  hl0lt1N  40205  hl2at  40220  cvrexch  40235  atcvr0eq  40241  lnnat  40242  atle  40251  cvrat4  40258  athgt  40271  1cvrco  40287  1cvratex  40288  1cvrjat  40290  1cvrat  40291  ps-2  40293  llnn0  40331  lplnn0N  40362  llncvrlpln  40373  lvoln0N  40406  lplncvrlvol  40431  dalemkeop  40440  pmapeq0  40581  pmapglb2N  40586  pmapglb2xN  40587  2atm2atN  40600  polval2N  40721  polsubN  40722  pol1N  40725  2polpmapN  40728  2polvalN  40729  poldmj1N  40743  pmapj2N  40744  2polatN  40747  pnonsingN  40748  ispsubcl2N  40762  polsubclN  40767  poml4N  40768  pmapojoinN  40783  pl42lem1N  40794  lhp2lt  40816  lhp0lt  40818  lhpn0  40819  lhpexnle  40821  lhpoc2N  40830  lhpocnle  40831  lhpj1  40837  lhpmod2i2  40853  lhpmod6i1  40854  lhprelat3N  40855  ltrnatb  40952  trlcl  40979  trlle  40999  cdleme3c  41045  cdleme7e  41062  cdleme22b  41156  cdlemg12e  41462  cdlemg12g  41464  tendoid  41588  tendo0tp  41604  cdlemk39s-id  41755  tendoex  41790  dia0eldmN  41855  dia2dimlem2  41880  dia2dimlem3  41881  docaclN  41939  doca2N  41941  djajN  41952  dib0  41979  dih0  42095  dih0bN  42096  dih0rn  42099  dih1  42101  dih1rn  42102  dih1cnv  42103  dihmeetlem18N  42139  dih1dimatlem  42144  dihlspsnssN  42147  dihlspsnat  42148  dihatexv  42153  dihglb2  42157  dochcl  42168  doch0  42173  doch1  42174  dochvalr3  42178  doch2val2  42179  dochss  42180  dochocss  42181  dochoc  42182  dochnoncon  42206  djhlj  42216  dihjatc  42232