Theorem hllat 33668

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

Assertion

Ref	Expression
hllat	⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)

Proof of Theorem hllat

Step	Hyp	Ref	Expression
1		hlatl 33665	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
2		atllat 33605	. 2 ⊢ (𝐾 ∈ AtLat → 𝐾 ∈ Lat)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)

Syntax hints:   → wi 4   ∈ wcel 1977  Latclat 16868  AtLatcal 33569  HLchlt 33655

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-dm 5048  df-iota 5768  df-fv 5812  df-ov 6552  df-atl 33603  df-cvlat 33627  df-hlat 33656

This theorem is referenced by:  hlpos  33670  hlatjcl  33671  hlatjcom  33672  hlatjidm  33673  hlatjass  33674  hlatj32  33676  hlatj4  33678  hlatlej1  33679  atnlej1  33683  atnlej2  33684  hlateq  33703  hlrelat5N  33705  hlrelat  33706  hlrelat2  33707  exatleN  33708  intnatN  33711  cvr2N  33715  hlrelat3  33716  cvrval3  33717  cvrval5  33719  cvrexchlem  33723  cvrexch  33724  cvratlem  33725  cvrat  33726  lnnat  33731  cvrat2  33733  atcvrj2b  33736  atltcvr  33739  atlelt  33742  2atlt  33743  atexchcvrN  33744  cvrat3  33746  cvrat4  33747  cvrat42  33748  2atjm  33749  atbtwn  33750  3noncolr2  33753  4noncolr3  33757  athgt  33760  3dim0  33761  3dimlem3a  33764  3dimlem3OLDN  33766  3dimlem4a  33767  3dimlem4OLDN  33769  3dim3  33773  1cvratex  33777  1cvrjat  33779  1cvrat  33780  ps-1  33781  ps-2  33782  hlatexch3N  33784  hlatexch4  33785  ps-2b  33786  3atlem1  33787  3atlem2  33788  3atlem4  33790  3atlem5  33791  3atlem6  33792  3at  33794  llnneat  33818  2llnmat  33828  2at0mat0  33829  2atm  33831  ps-2c  33832  lplni2  33841  llnmlplnN  33843  lplnle  33844  2atnelpln  33848  lplnneat  33849  lplnnelln  33850  islpln2a  33852  2lplnmN  33863  2llnmj  33864  2atmat  33865  lplnexllnN  33868  2llnjaN  33870  2llnm2N  33872  2llnm3N  33873  2llnm4  33874  2llnmeqat  33875  lvoli3  33881  islvol5  33883  lvoli2  33885  lvolnle3at  33886  3atnelvolN  33890  lvolneatN  33892  lvolnelln  33893  lvolnelpln  33894  islvol2aN  33896  4atlem3  33900  4atlem3a  33901  4atlem3b  33902  4atlem4a  33903  4atlem4b  33904  4atlem4c  33905  4atlem4d  33906  4atlem9  33907  4atlem10a  33908  4atlem10  33910  4atlem11a  33911  4atlem11b  33912  4atlem11  33913  4atlem12a  33914  4atlem12b  33915  4atlem12  33916  4at  33917  4at2  33918  lplncvrlvol2  33919  lplncvrlvol  33920  2lplnja  33923  2lplnm2N  33925  2lplnmj  33926  dalemkelat  33928  pmap11  34066  isline3  34080  lneq2at  34082  lncvrelatN  34085  lncmp  34087  2lnat  34088  2atm2atN  34089  2llnma1b  34090  2llnma3r  34092  cdlema1N  34095  cdlemblem  34097  cdlemb  34098  paddasslem2  34125  paddasslem5  34128  paddasslem8  34131  paddasslem12  34135  paddasslem13  34136  paddasslem15  34138  paddasslem16  34139  paddass  34142  padd12N  34143  pmodlem1  34150  pmodlem2  34151  pmod2iN  34153  pmodN  34154  pmapjat1  34157  pmapjat2  34158  pmapjlln1  34159  hlmod1i  34160  atmod1i1m  34162  llnmod1i2  34164  atmod2i1  34165  atmod2i2  34166  llnmod2i2  34167  atmod3i1  34168  atmod3i2  34169  atmod4i1  34170  atmod4i2  34171  llnexchb2lem  34172  llnexchb2  34173  llnexch2N  34174  dalawlem1  34175  dalawlem2  34176  dalawlem3  34177  dalawlem4  34178  dalawlem5  34179  dalawlem6  34180  dalawlem7  34181  dalawlem8  34182  dalawlem9  34183  dalawlem11  34185  dalawlem12  34186  dalawlem15  34189  polsubN  34211  paddunN  34231  pmapj2N  34233  pmapocjN  34234  psubclinN  34252  paddatclN  34253  pclfinclN  34254  linepsubclN  34255  poml4N  34257  osumcllem5N  34264  osumcllem7N  34266  pexmidlem2N  34275  pexmidlem4N  34277  pl42lem1N  34283  pl42lem2N  34284  pl42lem4N  34286  pl42N  34287  lhp2lt  34305  lhpexle2lem  34313  lhpexle3lem  34315  lhpocnle  34320  lhpjat2  34325  lhpj1  34326  lhpmcvr  34327  lhpmcvr3  34329  lhpmcvr4N  34330  lhpmcvr5N  34331  lhpmcvr6N  34332  lhpm0atN  34333  lhpmatb  34335  lhp2at0  34336  lhp2atnle  34337  lhpelim  34341  lhpmod2i2  34342  lhpmod6i1  34343  lhprelat3N  34344  lhple  34346  lhpat3  34350  4atexlemkl  34361  ltrnm  34435  ltrnj  34436  ltrnel  34443  ltrncnvel  34446  ltrnmwOLD  34456  trlval2  34468  trlcl  34469  trljat1  34471  trljat2  34472  trlle  34489  trlval3  34492  arglem1N  34495  cdlemc1  34496  cdlemc2  34497  cdlemc4  34499  cdlemc5  34500  cdlemc6  34501  cdlemd1  34503  cdlemd2  34504  cdlemd3  34505  cdlemd4  34506  cdlemd7  34509  cdleme0aa  34515  cdleme0b  34517  cdleme0c  34518  cdleme0cp  34519  cdleme0cq  34520  cdleme0e  34522  cdleme0fN  34523  cdlemeulpq  34525  cdleme01N  34526  cdleme0ex1N  34528  cdleme1b  34531  cdleme1  34532  cdleme2  34533  cdleme3b  34534  cdleme3c  34535  cdleme3e  34537  cdleme3g  34539  cdleme3h  34540  cdleme3  34542  cdleme4a  34544  cdleme5  34545  cdleme7aa  34547  cdleme7c  34550  cdleme7d  34551  cdleme7e  34552  cdleme7ga  34553  cdleme7  34554  cdleme8  34555  cdleme9b  34557  cdleme9  34558  cdleme10  34559  cdleme11c  34566  cdleme11e  34568  cdleme11fN  34569  cdleme11g  34570  cdleme11k  34573  cdleme11  34575  cdleme13  34577  cdleme15b  34580  cdleme15d  34582  cdleme15  34583  cdleme16b  34584  cdleme16e  34587  cdleme16f  34588  cdleme17b  34592  cdleme17c  34593  cdleme22gb  34599  cdlemedb  34602  cdlemednpq  34604  cdleme20zN  34606  cdleme19a  34609  cdleme19b  34610  cdleme19c  34611  cdleme19e  34613  cdleme20aN  34615  cdleme20bN  34616  cdleme20c  34617  cdleme20d  34618  cdleme20e  34619  cdleme20j  34624  cdleme20k  34625  cdleme20l2  34627  cdleme20l  34628  cdleme20m  34629  cdleme21c  34633  cdleme21ct  34635  cdleme22aa  34645  cdleme22b  34647  cdleme22cN  34648  cdleme22d  34649  cdleme22e  34650  cdleme22eALTN  34651  cdleme22f  34652  cdleme22g  34654  cdleme23a  34655  cdleme23b  34656  cdleme23c  34657  cdleme27N  34675  cdleme28a  34676  cdleme28b  34677  cdleme29ex  34680  cdleme30a  34684  cdlemefr29exN  34708  cdleme32b  34748  cdleme32c  34749  cdleme32e  34751  cdleme35a  34754  cdleme35fnpq  34755  cdleme35b  34756  cdleme35c  34757  cdleme35d  34758  cdleme35f  34760  cdleme42c  34778  cdleme42e  34785  cdleme42h  34788  cdleme42i  34789  cdleme42mgN  34794  cdleme48bw  34808  cdlemeg46frv  34831  cdlemeg46vrg  34833  cdlemeg46rgv  34834  cdlemeg46req  34835  cdleme50eq  34847  cdlemf1  34867  cdlemf2  34868  trlord  34875  cdlemg2fv2  34906  cdlemg2m  34910  cdlemg7fvbwN  34913  cdlemg4c  34918  cdlemg4  34923  cdlemg6c  34926  cdlemg8b  34934  cdlemg10bALTN  34942  cdlemg10c  34945  cdlemg10  34947  cdlemg11b  34948  cdlemg12f  34954  cdlemg12g  34955  cdlemg12  34956  cdlemg13a  34957  cdlemg17a  34967  cdlemg17dALTN  34970  cdlemg17  34983  cdlemg18b  34985  cdlemg19a  34989  cdlemg19  34990  cdlemg27a  34998  cdlemg27b  35002  cdlemg31a  35003  cdlemg31b  35004  cdlemg33b0  35007  cdlemg33a  35012  cdlemg35  35019  trlcolem  35032  cdlemg42  35035  cdlemg44a  35037  cdlemg46  35041  trljco  35046  trljco2  35047  tendoidcl  35075  tendococl  35078  tendopltp  35086  cdlemh1  35121  cdlemh2  35122  cdlemi1  35124  cdlemi  35126  cdlemk3  35139  cdlemk4  35140  cdlemkvcl  35148  cdlemk10  35149  cdlemk7  35154  cdlemk11  35155  cdlemk12  35156  cdlemkole  35159  cdlemk14  35160  cdlemk15  35161  cdlemk1u  35165  cdlemk5u  35167  cdlemk7u  35176  cdlemk11u  35177  cdlemk12u  35178  cdlemk37  35220  cdlemk39  35222  cdlemkid1  35228  cdlemkid2  35230  cdlemk48  35256  cdlemk50  35258  cdlemk51  35259  cdlemk52  35260  cdlemk39u  35274  dia1eldmN  35348  dialss  35353  dia11N  35355  dia1N  35360  diaglbN  35362  diaintclN  35365  dia2dimlem1  35371  dia2dimlem2  35372  dia2dimlem3  35373  dia2dimlem10  35380  dia2dimlem12  35382  cdlemm10N  35425  docaclN  35431  doca2N  35433  djajN  35444  dib11N  35467  dibglbN  35473  dibintclN  35474  diblss  35477  cdlemn2  35502  cdlemn10  35513  dihjustlem  35523  dihord1  35525  dihord2a  35526  dihord2b  35527  dihord2cN  35528  dihord11b  35529  dihord11c  35531  dihord2pre  35532  dihord2pre2  35533  dihlsscpre  35541  dib2dim  35550  dih2dimb  35551  dih2dimbALTN  35552  dihvalcq2  35554  dihopelvalcpre  35555  dihord6apre  35563  dihord5b  35566  dihord6b  35567  dihord5apre  35569  dih11  35572  dih1  35593  dihwN  35596  dihmeetlem1N  35597  dihglblem5apreN  35598  dihglblem5aN  35599  dihglblem2aN  35600  dihglblem2N  35601  dihglblem3N  35602  dihmeetlem2N  35606  dihglbcpreN  35607  dihmeetbclemN  35611  dihmeetlem3N  35612  dihmeetlem4preN  35613  dihmeetlem6  35616  dihmeetlem7N  35617  dihjatc1  35618  dihjatc2N  35619  dihjatc3  35620  dihmeetlem9N  35622  dihmeetlem10N  35623  dihmeetlem11N  35624  dihmeetlem15N  35628  dihmeetlem16N  35629  dihmeetlem17N  35630  dihmeetlem19N  35632  dihmeetlem20N  35633  dihmeetALTN  35634  dihmeetcl  35652  dihmeet2  35653  dochvalr  35664  djhlj  35708  djhljjN  35709  djhj  35711  dihjatcclem1  35725  dihjatcclem2  35726  dihjatcclem4  35728  dihprrnlem1N  35731  dihprrnlem2  35732  dihjat6  35741  dihjat5N  35744  dvh4dimat  35745