Theorem hllat 34963

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

Assertion

Ref	Expression
hllat	|- ( K e. HL -> K e. Lat )

Proof of Theorem hllat

Step	Hyp	Ref	Expression
1		hlatl 34960	. 2 |- ( K e. HL -> K e. AtLat )
2		atllat 34900	. 2 |- ( K e. AtLat -> K e. Lat )
3	1, 2	syl 16	1 |- ( K e. HL -> K e. Lat )

Syntax hints:   -> wi 4   e. wcel 1804   Latclat 15654   AtLatcal 34864   HLchlt 34950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-dm 4999  df-iota 5541  df-fv 5586  df-ov 6284  df-atl 34898  df-cvlat 34922  df-hlat 34951

This theorem is referenced by:  hlpos  34965  hlatjcl  34966  hlatjcom  34967  hlatjidm  34968  hlatjass  34969  hlatj32  34971  hlatj4  34973  hlatlej1  34974  atnlej1  34978  atnlej2  34979  hlateq  34998  hlrelat5N  35000  hlrelat  35001  hlrelat2  35002  exatleN  35003  intnatN  35006  cvr2N  35010  hlrelat3  35011  cvrval3  35012  cvrval5  35014  cvrexchlem  35018  cvrexch  35019  cvratlem  35020  cvrat  35021  lnnat  35026  cvrat2  35028  atcvrj2b  35031  atltcvr  35034  atlelt  35037  2atlt  35038  atexchcvrN  35039  cvrat3  35041  cvrat4  35042  cvrat42  35043  2atjm  35044  atbtwn  35045  3noncolr2  35048  4noncolr3  35052  athgt  35055  3dim0  35056  3dimlem3a  35059  3dimlem3OLDN  35061  3dimlem4a  35062  3dimlem4OLDN  35064  3dim3  35068  1cvratex  35072  1cvrjat  35074  1cvrat  35075  ps-1  35076  ps-2  35077  hlatexch3N  35079  hlatexch4  35080  ps-2b  35081  3atlem1  35082  3atlem2  35083  3atlem4  35085  3atlem5  35086  3atlem6  35087  3at  35089  llnneat  35113  2llnmat  35123  2at0mat0  35124  2atm  35126  ps-2c  35127  lplni2  35136  llnmlplnN  35138  lplnle  35139  2atnelpln  35143  lplnneat  35144  lplnnelln  35145  islpln2a  35147  2lplnmN  35158  2llnmj  35159  2atmat  35160  lplnexllnN  35163  2llnjaN  35165  2llnm2N  35167  2llnm3N  35168  2llnm4  35169  2llnmeqat  35170  lvoli3  35176  islvol5  35178  lvoli2  35180  lvolnle3at  35181  3atnelvolN  35185  lvolneatN  35187  lvolnelln  35188  lvolnelpln  35189  islvol2aN  35191  4atlem3  35195  4atlem3a  35196  4atlem3b  35197  4atlem4a  35198  4atlem4b  35199  4atlem4c  35200  4atlem4d  35201  4atlem9  35202  4atlem10a  35203  4atlem10  35205  4atlem11a  35206  4atlem11b  35207  4atlem11  35208  4atlem12a  35209  4atlem12b  35210  4atlem12  35211  4at  35212  4at2  35213  lplncvrlvol2  35214  lplncvrlvol  35215  2lplnja  35218  2lplnm2N  35220  2lplnmj  35221  dalemkelat  35223  pmap11  35361  isline3  35375  lneq2at  35377  lncvrelatN  35380  lncmp  35382  2lnat  35383  2atm2atN  35384  2llnma1b  35385  2llnma3r  35387  cdlema1N  35390  cdlemblem  35392  cdlemb  35393  paddasslem2  35420  paddasslem5  35423  paddasslem8  35426  paddasslem12  35430  paddasslem13  35431  paddasslem15  35433  paddasslem16  35434  paddass  35437  padd12N  35438  pmodlem1  35445  pmodlem2  35446  pmod2iN  35448  pmodN  35449  pmapjat1  35452  pmapjat2  35453  pmapjlln1  35454  hlmod1i  35455  atmod1i1m  35457  llnmod1i2  35459  atmod2i1  35460  atmod2i2  35461  llnmod2i2  35462  atmod3i1  35463  atmod3i2  35464  atmod4i1  35465  atmod4i2  35466  llnexchb2lem  35467  llnexchb2  35468  llnexch2N  35469  dalawlem1  35470  dalawlem2  35471  dalawlem3  35472  dalawlem4  35473  dalawlem5  35474  dalawlem6  35475  dalawlem7  35476  dalawlem8  35477  dalawlem9  35478  dalawlem11  35480  dalawlem12  35481  dalawlem15  35484  polsubN  35506  paddunN  35526  pmapj2N  35528  pmapocjN  35529  psubclinN  35547  paddatclN  35548  pclfinclN  35549  linepsubclN  35550  poml4N  35552  osumcllem5N  35559  osumcllem7N  35561  pexmidlem2N  35570  pexmidlem4N  35572  pl42lem1N  35578  pl42lem2N  35579  pl42lem4N  35581  pl42N  35582  lhp2lt  35600  lhpexle2lem  35608  lhpexle3lem  35610  lhpocnle  35615  lhpjat2  35620  lhpj1  35621  lhpmcvr  35622  lhpmcvr3  35624  lhpmcvr4N  35625  lhpmcvr5N  35626  lhpmcvr6N  35627  lhpm0atN  35628  lhpmatb  35630  lhp2at0  35631  lhp2atnle  35632  lhpelim  35636  lhpmod2i2  35637  lhpmod6i1  35638  lhprelat3N  35639  lhple  35641  lhpat3  35645  4atexlemkl  35656  ltrnm  35730  ltrnj  35731  ltrnel  35738  ltrncnvel  35741  ltrnmwOLD  35751  trlval2  35763  trlcl  35764  trljat1  35766  trljat2  35767  trlle  35784  trlval3  35787  arglem1N  35790  cdlemc1  35791  cdlemc2  35792  cdlemc4  35794  cdlemc5  35795  cdlemc6  35796  cdlemd1  35798  cdlemd2  35799  cdlemd3  35800  cdlemd4  35801  cdlemd7  35804  cdleme0aa  35810  cdleme0b  35812  cdleme0c  35813  cdleme0cp  35814  cdleme0cq  35815  cdleme0e  35817  cdleme0fN  35818  cdlemeulpq  35820  cdleme01N  35821  cdleme0ex1N  35823  cdleme1b  35826  cdleme1  35827  cdleme2  35828  cdleme3b  35829  cdleme3c  35830  cdleme3e  35832  cdleme3g  35834  cdleme3h  35835  cdleme3  35837  cdleme4a  35839  cdleme5  35840  cdleme7aa  35842  cdleme7c  35845  cdleme7d  35846  cdleme7e  35847  cdleme7ga  35848  cdleme7  35849  cdleme8  35850  cdleme9b  35852  cdleme9  35853  cdleme10  35854  cdleme11c  35861  cdleme11e  35863  cdleme11fN  35864  cdleme11g  35865  cdleme11k  35868  cdleme11  35870  cdleme13  35872  cdleme15b  35875  cdleme15d  35877  cdleme15  35878  cdleme16b  35879  cdleme16e  35882  cdleme16f  35883  cdleme17b  35887  cdleme17c  35888  cdleme22gb  35894  cdlemedb  35897  cdlemednpq  35899  cdleme20zN  35901  cdleme19a  35904  cdleme19b  35905  cdleme19c  35906  cdleme19e  35908  cdleme20aN  35910  cdleme20bN  35911  cdleme20c  35912  cdleme20d  35913  cdleme20e  35914  cdleme20j  35919  cdleme20k  35920  cdleme20l2  35922  cdleme20l  35923  cdleme20m  35924  cdleme21c  35928  cdleme21ct  35930  cdleme22aa  35940  cdleme22b  35942  cdleme22cN  35943  cdleme22d  35944  cdleme22e  35945  cdleme22eALTN  35946  cdleme22f  35947  cdleme22g  35949  cdleme23a  35950  cdleme23b  35951  cdleme23c  35952  cdleme27N  35970  cdleme28a  35971  cdleme28b  35972  cdleme29ex  35975  cdleme30a  35979  cdlemefr29exN  36003  cdleme32b  36043  cdleme32c  36044  cdleme32e  36046  cdleme35a  36049  cdleme35fnpq  36050  cdleme35b  36051  cdleme35c  36052  cdleme35d  36053  cdleme35f  36055  cdleme42c  36073  cdleme42e  36080  cdleme42h  36083  cdleme42i  36084  cdleme42mgN  36089  cdleme48bw  36103  cdlemeg46frv  36126  cdlemeg46vrg  36128  cdlemeg46rgv  36129  cdlemeg46req  36130  cdleme50eq  36142  cdlemf1  36162  cdlemf2  36163  trlord  36170  cdlemg2fv2  36201  cdlemg2m  36205  cdlemg7fvbwN  36208  cdlemg4c  36213  cdlemg4  36218  cdlemg6c  36221  cdlemg8b  36229  cdlemg10bALTN  36237  cdlemg10c  36240  cdlemg10  36242  cdlemg11b  36243  cdlemg12f  36249  cdlemg12g  36250  cdlemg12  36251  cdlemg13a  36252  cdlemg17a  36262  cdlemg17dALTN  36265  cdlemg17  36278  cdlemg18b  36280  cdlemg19a  36284  cdlemg19  36285  cdlemg27a  36293  cdlemg27b  36297  cdlemg31a  36298  cdlemg31b  36299  cdlemg33b0  36302  cdlemg33a  36307  cdlemg35  36314  trlcolem  36327  cdlemg42  36330  cdlemg44a  36332  cdlemg46  36336  trljco  36341  trljco2  36342  tendoidcl  36370  tendococl  36373  tendopltp  36381  cdlemh1  36416  cdlemh2  36417  cdlemi1  36419  cdlemi  36421  cdlemk3  36434  cdlemk4  36435  cdlemkvcl  36443  cdlemk10  36444  cdlemk7  36449  cdlemk11  36450  cdlemk12  36451  cdlemkole  36454  cdlemk14  36455  cdlemk15  36456  cdlemk1u  36460  cdlemk5u  36462  cdlemk7u  36471  cdlemk11u  36472  cdlemk12u  36473  cdlemk37  36515  cdlemk39  36517  cdlemkid1  36523  cdlemkid2  36525  cdlemk48  36551  cdlemk50  36553  cdlemk51  36554  cdlemk52  36555  cdlemk39u  36569  dia1eldmN  36643  dialss  36648  dia11N  36650  dia1N  36655  diaglbN  36657  diaintclN  36660  dia2dimlem1  36666  dia2dimlem2  36667  dia2dimlem3  36668  dia2dimlem10  36675  dia2dimlem12  36677  cdlemm10N  36720  docaclN  36726  doca2N  36728  djajN  36739  dib11N  36762  dibglbN  36768  dibintclN  36769  diblss  36772  cdlemn2  36797  cdlemn10  36808  dihjustlem  36818  dihord1  36820  dihord2a  36821  dihord2b  36822  dihord2cN  36823  dihord11b  36824  dihord11c  36826  dihord2pre  36827  dihord2pre2  36828  dihlsscpre  36836  dib2dim  36845  dih2dimb  36846  dih2dimbALTN  36847  dihvalcq2  36849  dihopelvalcpre  36850  dihord6apre  36858  dihord5b  36861  dihord6b  36862  dihord5apre  36864  dih11  36867  dih1  36888  dihwN  36891  dihmeetlem1N  36892  dihglblem5apreN  36893  dihglblem5aN  36894  dihglblem2aN  36895  dihglblem2N  36896  dihglblem3N  36897  dihmeetlem2N  36901  dihglbcpreN  36902  dihmeetbclemN  36906  dihmeetlem3N  36907  dihmeetlem4preN  36908  dihmeetlem6  36911  dihmeetlem7N  36912  dihjatc1  36913  dihjatc2N  36914  dihjatc3  36915  dihmeetlem9N  36917  dihmeetlem10N  36918  dihmeetlem11N  36919  dihmeetlem15N  36923  dihmeetlem16N  36924  dihmeetlem17N  36925  dihmeetlem19N  36927  dihmeetlem20N  36928  dihmeetALTN  36929  dihmeetcl  36947  dihmeet2  36948  dochvalr  36959  djhlj  37003  djhljjN  37004  djhj  37006  dihjatcclem1  37020  dihjatcclem2  37021  dihjatcclem4  37023  dihprrnlem1N  37026  dihprrnlem2  37027  dihjat6  37036  dihjat5N  37039  dvh4dimat  37040