Theorem hlop 40243

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  OPcops 40053  OLcol 40055  HLchlt 40231

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420  df-ol 40059  df-oml 40060  df-hlat 40232

This theorem is used by:  glbconN  40258  glbconxN  40259  hlhgt2  40270  hl0lt1N  40271  hl2at  40286  cvrexch  40301  atcvr0eq  40307  lnnat  40308  atle  40317  cvrat4  40324  athgt  40337  1cvrco  40353  1cvratex  40354  1cvrjat  40356  1cvrat  40357  ps-2  40359  llnn0  40397  lplnn0N  40428  llncvrlpln  40439  lvoln0N  40472  lplncvrlvol  40497  dalemkeop  40506  pmapeq0  40647  pmapglb2N  40652  pmapglb2xN  40653  2atm2atN  40666  polval2N  40787  polsubN  40788  pol1N  40791  2polpmapN  40794  2polvalN  40795  poldmj1N  40809  pmapj2N  40810  2polatN  40813  pnonsingN  40814  ispsubcl2N  40828  polsubclN  40833  poml4N  40834  pmapojoinN  40849  pl42lem1N  40860  lhp2lt  40882  lhp0lt  40884  lhpn0  40885  lhpexnle  40887  lhpoc2N  40896  lhpocnle  40897  lhpj1  40903  lhpmod2i2  40919  lhpmod6i1  40920  lhprelat3N  40921  ltrnatb  41018  trlcl  41045  trlle  41065  cdleme3c  41111  cdleme7e  41128  cdleme22b  41222  cdlemg12e  41528  cdlemg12g  41530  tendoid  41654  tendo0tp  41670  cdlemk39s-id  41821  tendoex  41856  dia0eldmN  41921  dia2dimlem2  41946  dia2dimlem3  41947  docaclN  42005  doca2N  42007  djajN  42018  dib0  42045  dih0  42161  dih0bN  42162  dih0rn  42165  dih1  42167  dih1rn  42168  dih1cnv  42169  dihmeetlem18N  42205  dih1dimatlem  42210  dihlspsnssN  42213  dihlspsnat  42214  dihatexv  42219  dihglb2  42223  dochcl  42234  doch0  42239  doch1  42240  dochvalr3  42244  doch2val2  42245  dochss  42246  dochocss  42247  dochoc  42248  dochnoncon  42272  djhlj  42282  dihjatc  42298