Theorem hlop 34649

Description: A Hilbert lattice is an orthoposet. (Contributed by NM, 20-Oct-2011.)

Assertion

Ref	Expression
hlop	|- ( K e. HL -> K e. OP )

Proof of Theorem hlop

Step	Hyp	Ref	Expression
1		hlol 34648	. 2 |- ( K e. HL -> K e. OL )
2		olop 34501	. 2 |- ( K e. OL -> K e. OP )
3	1, 2	syl 17	1 |- ( K e. HL -> K e. OP )

Syntax hints:   -> wi 4   e. wcel 1990   OPcops 34459   OLcol 34461   HLchlt 34637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-ol 34465  df-oml 34466  df-hlat 34638

This theorem is referenced by:  glbconN  34663  glbconxN  34664  hlhgt2  34675  hl0lt1N  34676  hl2at  34691  cvrexch  34706  atcvr0eq  34712  lnnat  34713  atle  34722  cvrat4  34729  athgt  34742  1cvrco  34758  1cvratex  34759  1cvrjat  34761  1cvrat  34762  ps-2  34764  llnn0  34802  lplnn0N  34833  llncvrlpln  34844  lvoln0N  34877  lplncvrlvol  34902  dalemkeop  34911  pmapeq0  35052  pmapglb2N  35057  pmapglb2xN  35058  2atm2atN  35071  polval2N  35192  polsubN  35193  pol1N  35196  2polpmapN  35199  2polvalN  35200  poldmj1N  35214  pmapj2N  35215  2polatN  35218  pnonsingN  35219  ispsubcl2N  35233  polsubclN  35238  poml4N  35239  pmapojoinN  35254  pl42lem1N  35265  lhp2lt  35287  lhp0lt  35289  lhpn0  35290  lhpexnle  35292  lhpoc2N  35301  lhpocnle  35302  lhpj1  35308  lhpmod2i2  35324  lhpmod6i1  35325  lhprelat3N  35326  ltrnatb  35423  ltrnmwOLD  35438  trlcl  35451  trlle  35471  cdleme3c  35517  cdleme7e  35534  cdleme22b  35629  cdlemg12e  35935  cdlemg12g  35937  tendoid  36061  tendo0tp  36077  cdlemk39s-id  36228  tendoex  36263  dia0eldmN  36329  dia2dimlem2  36354  dia2dimlem3  36355  docaclN  36413  doca2N  36415  djajN  36426  dib0  36453  dih0  36569  dih0bN  36570  dih0rn  36573  dih1  36575  dih1rn  36576  dih1cnv  36577  dihmeetlem18N  36613  dih1dimatlem  36618  dihlspsnssN  36621  dihlspsnat  36622  dihatexv  36627  dihglb2  36631  dochcl  36642  doch0  36647  doch1  36648  dochvalr3  36652  doch2val2  36653  dochss  36654  dochocss  36655  dochoc  36656  dochnoncon  36680  djhlj  36690  dihjatc  36706