Theorem hlol 34648

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

Assertion

Ref	Expression
hlol	|- ( K e. HL -> K e. OL )

Proof of Theorem hlol

Step	Hyp	Ref	Expression
1		hloml 34644	. 2 |- ( K e. HL -> K e. OML )
2		omlol 34527	. 2 |- ( K e. OML -> K e. OL )
3	1, 2	syl 17	1 |- ( K e. HL -> K e. OL )

Syntax hints:   -> wi 4   e. wcel 1990   OLcol 34461   OMLcoml 34462   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-oml 34466  df-hlat 34638

This theorem is referenced by:  hlop  34649  cvrexch  34706  atle  34722  athgt  34742  2at0mat0  34811  dalem24  34983  pmapjat1  35139  atmod1i1m  35144  llnexchb2lem  35154  dalawlem2  35158  dalawlem6  35162  dalawlem7  35163  dalawlem11  35167  dalawlem12  35168  poldmj1N  35214  pmapj2N  35215  2polatN  35218  lhpmcvr3  35311  lhp2at0  35318  lhp2at0nle  35321  lhpelim  35323  lhpmod2i2  35324  lhpmod6i1  35325  lhprelat3N  35326  lhple  35328  4atex2-0aOLDN  35364  trljat1  35453  trljat2  35454  cdlemc1  35478  cdlemc6  35483  cdleme0cp  35501  cdleme0cq  35502  cdleme0e  35504  cdleme1  35514  cdleme2  35515  cdleme3c  35517  cdleme4  35525  cdleme5  35527  cdleme7c  35532  cdleme7e  35534  cdleme8  35537  cdleme9  35540  cdleme10  35541  cdleme15b  35562  cdlemednpq  35586  cdleme20yOLD  35590  cdleme20c  35599  cdleme20d  35600  cdleme20j  35606  cdleme22cN  35630  cdleme22d  35631  cdleme22e  35632  cdleme22eALTN  35633  cdleme23b  35638  cdleme30a  35666  cdlemefrs29pre00  35683  cdlemefrs29bpre0  35684  cdlemefrs29cpre1  35686  cdleme32fva  35725  cdleme35b  35738  cdleme35d  35740  cdleme35e  35741  cdleme42a  35759  cdleme42ke  35773  cdlemeg46frv  35813  cdlemg2fv2  35888  cdlemg2m  35892  cdlemg10bALTN  35924  cdlemg12e  35935  cdlemg31d  35988  trlcoabs2N  36010  trlcolem  36014  trljco  36028  cdlemh2  36104  cdlemh  36105  cdlemi1  36106  cdlemk4  36122  cdlemk9  36127  cdlemk9bN  36128  cdlemkid2  36212  dia2dimlem1  36353  dia2dimlem2  36354  dia2dimlem3  36355  doca2N  36415  djajN  36426  cdlemn10  36495  dihvalcqat  36528  dih1  36575  dihglbcpreN  36589  dihmeetbclemN  36593  dihmeetlem7N  36599  dihjatc1  36600  djhlj  36690  djh01  36701  dihjatc  36706