Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hlop Structured version   Visualization version   GIF version

Theorem hlop 36616
Description: A Hilbert lattice is an orthoposet. (Contributed by NM, 20-Oct-2011.)
Assertion
Ref Expression
hlop (𝐾 ∈ HL → 𝐾 ∈ OP)

Proof of Theorem hlop
StepHypRef Expression
1 hlol 36615 . 2 (𝐾 ∈ HL → 𝐾 ∈ OL)
2 olop 36468 . 2 (𝐾 ∈ OL → 𝐾 ∈ OP)
31, 2syl 17 1 (𝐾 ∈ HL → 𝐾 ∈ OP)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  OPcops 36426  OLcol 36428  HLchlt 36604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ral 3135  df-rex 3136  df-rab 3139  df-v 3471  df-un 3913  df-in 3915  df-ss 3925  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-iota 6293  df-fv 6342  df-ov 7143  df-ol 36432  df-oml 36433  df-hlat 36605
This theorem is referenced by:  glbconN  36631  glbconxN  36632  hlhgt2  36643  hl0lt1N  36644  hl2at  36659  cvrexch  36674  atcvr0eq  36680  lnnat  36681  atle  36690  cvrat4  36697  athgt  36710  1cvrco  36726  1cvratex  36727  1cvrjat  36729  1cvrat  36730  ps-2  36732  llnn0  36770  lplnn0N  36801  llncvrlpln  36812  lvoln0N  36845  lplncvrlvol  36870  dalemkeop  36879  pmapeq0  37020  pmapglb2N  37025  pmapglb2xN  37026  2atm2atN  37039  polval2N  37160  polsubN  37161  pol1N  37164  2polpmapN  37167  2polvalN  37168  poldmj1N  37182  pmapj2N  37183  2polatN  37186  pnonsingN  37187  ispsubcl2N  37201  polsubclN  37206  poml4N  37207  pmapojoinN  37222  pl42lem1N  37233  lhp2lt  37255  lhp0lt  37257  lhpn0  37258  lhpexnle  37260  lhpoc2N  37269  lhpocnle  37270  lhpj1  37276  lhpmod2i2  37292  lhpmod6i1  37293  lhprelat3N  37294  ltrnatb  37391  trlcl  37418  trlle  37438  cdleme3c  37484  cdleme7e  37501  cdleme22b  37595  cdlemg12e  37901  cdlemg12g  37903  tendoid  38027  tendo0tp  38043  cdlemk39s-id  38194  tendoex  38229  dia0eldmN  38294  dia2dimlem2  38319  dia2dimlem3  38320  docaclN  38378  doca2N  38380  djajN  38391  dib0  38418  dih0  38534  dih0bN  38535  dih0rn  38538  dih1  38540  dih1rn  38541  dih1cnv  38542  dihmeetlem18N  38578  dih1dimatlem  38583  dihlspsnssN  38586  dihlspsnat  38587  dihatexv  38592  dihglb2  38596  dochcl  38607  doch0  38612  doch1  38613  dochvalr3  38617  doch2val2  38618  dochss  38619  dochocss  38620  dochoc  38621  dochnoncon  38645  djhlj  38655  dihjatc  38671
  Copyright terms: Public domain W3C validator