Theorem hlol 35139

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

Assertion

Ref	Expression
hlol	⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)

Proof of Theorem hlol

Step	Hyp	Ref	Expression
1		hloml 35135	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OML)
2		omlol 35018	. 2 ⊢ (𝐾 ∈ OML → 𝐾 ∈ OL)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)

Syntax hints:   → wi 4   ∈ wcel 2156  OLcol 34952  OMLcoml 34953  HLchlt 35128

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-iota 6060  df-fv 6105  df-ov 6873  df-oml 34957  df-hlat 35129

This theorem is referenced by:  hlop  35140  cvrexch  35198  atle  35214  athgt  35234  2at0mat0  35303  dalem24  35475  pmapjat1  35631  atmod1i1m  35636  llnexchb2lem  35646  dalawlem2  35650  dalawlem6  35654  dalawlem7  35655  dalawlem11  35659  dalawlem12  35660  poldmj1N  35706  pmapj2N  35707  2polatN  35710  lhpmcvr3  35803  lhp2at0  35810  lhp2at0nle  35813  lhpelim  35815  lhpmod2i2  35816  lhpmod6i1  35817  lhprelat3N  35818  lhple  35820  4atex2-0aOLDN  35856  trljat1  35944  trljat2  35945  cdlemc1  35969  cdlemc6  35974  cdleme0cp  35992  cdleme0cq  35993  cdleme0e  35995  cdleme1  36005  cdleme2  36006  cdleme3c  36008  cdleme4  36016  cdleme5  36018  cdleme7c  36023  cdleme7e  36025  cdleme8  36028  cdleme9  36031  cdleme10  36032  cdleme15b  36053  cdlemednpq  36077  cdleme20c  36089  cdleme20d  36090  cdleme20j  36096  cdleme22cN  36120  cdleme22d  36121  cdleme22e  36122  cdleme22eALTN  36123  cdleme23b  36128  cdleme30a  36156  cdlemefrs29pre00  36173  cdlemefrs29bpre0  36174  cdlemefrs29cpre1  36176  cdleme32fva  36215  cdleme35b  36228  cdleme35d  36230  cdleme35e  36231  cdleme42a  36249  cdleme42ke  36263  cdlemeg46frv  36303  cdlemg2fv2  36378  cdlemg2m  36382  cdlemg10bALTN  36414  cdlemg12e  36425  cdlemg31d  36478  trlcoabs2N  36500  trlcolem  36504  trljco  36518  cdlemh2  36594  cdlemh  36595  cdlemi1  36596  cdlemk4  36612  cdlemk9  36617  cdlemk9bN  36618  cdlemkid2  36702  dia2dimlem1  36842  dia2dimlem2  36843  dia2dimlem3  36844  doca2N  36904  djajN  36915  cdlemn10  36984  dihvalcqat  37017  dih1  37064  dihglbcpreN  37078  dihmeetbclemN  37082  dihmeetlem7N  37088  dihjatc1  37089  djhlj  37179  djh01  37190  dihjatc  37195