Theorem hllat 32974

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 32971	. 2 |- ( K e. HL -> K e. AtLat )
2		atllat 32911	. 2 |- ( K e. AtLat -> K e. Lat )
3	1, 2	syl 17	1 |- ( K e. HL -> K e. Lat )

Syntax hints:   -> wi 4   e. wcel 1898   Latclat 16340   AtLatcal 32875   HLchlt 32961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-dm 4863  df-iota 5565  df-fv 5609  df-ov 6318  df-atl 32909  df-cvlat 32933  df-hlat 32962

This theorem is referenced by:  hlpos  32976  hlatjcl  32977  hlatjcom  32978  hlatjidm  32979  hlatjass  32980  hlatj32  32982  hlatj4  32984  hlatlej1  32985  atnlej1  32989  atnlej2  32990  hlateq  33009  hlrelat5N  33011  hlrelat  33012  hlrelat2  33013  exatleN  33014  intnatN  33017  cvr2N  33021  hlrelat3  33022  cvrval3  33023  cvrval5  33025  cvrexchlem  33029  cvrexch  33030  cvratlem  33031  cvrat  33032  lnnat  33037  cvrat2  33039  atcvrj2b  33042  atltcvr  33045  atlelt  33048  2atlt  33049  atexchcvrN  33050  cvrat3  33052  cvrat4  33053  cvrat42  33054  2atjm  33055  atbtwn  33056  3noncolr2  33059  4noncolr3  33063  athgt  33066  3dim0  33067  3dimlem3a  33070  3dimlem3OLDN  33072  3dimlem4a  33073  3dimlem4OLDN  33075  3dim3  33079  1cvratex  33083  1cvrjat  33085  1cvrat  33086  ps-1  33087  ps-2  33088  hlatexch3N  33090  hlatexch4  33091  ps-2b  33092  3atlem1  33093  3atlem2  33094  3atlem4  33096  3atlem5  33097  3atlem6  33098  3at  33100  llnneat  33124  2llnmat  33134  2at0mat0  33135  2atm  33137  ps-2c  33138  lplni2  33147  llnmlplnN  33149  lplnle  33150  2atnelpln  33154  lplnneat  33155  lplnnelln  33156  islpln2a  33158  2lplnmN  33169  2llnmj  33170  2atmat  33171  lplnexllnN  33174  2llnjaN  33176  2llnm2N  33178  2llnm3N  33179  2llnm4  33180  2llnmeqat  33181  lvoli3  33187  islvol5  33189  lvoli2  33191  lvolnle3at  33192  3atnelvolN  33196  lvolneatN  33198  lvolnelln  33199  lvolnelpln  33200  islvol2aN  33202  4atlem3  33206  4atlem3a  33207  4atlem3b  33208  4atlem4a  33209  4atlem4b  33210  4atlem4c  33211  4atlem4d  33212  4atlem9  33213  4atlem10a  33214  4atlem10  33216  4atlem11a  33217  4atlem11b  33218  4atlem11  33219  4atlem12a  33220  4atlem12b  33221  4atlem12  33222  4at  33223  4at2  33224  lplncvrlvol2  33225  lplncvrlvol  33226  2lplnja  33229  2lplnm2N  33231  2lplnmj  33232  dalemkelat  33234  pmap11  33372  isline3  33386  lneq2at  33388  lncvrelatN  33391  lncmp  33393  2lnat  33394  2atm2atN  33395  2llnma1b  33396  2llnma3r  33398  cdlema1N  33401  cdlemblem  33403  cdlemb  33404  paddasslem2  33431  paddasslem5  33434  paddasslem8  33437  paddasslem12  33441  paddasslem13  33442  paddasslem15  33444  paddasslem16  33445  paddass  33448  padd12N  33449  pmodlem1  33456  pmodlem2  33457  pmod2iN  33459  pmodN  33460  pmapjat1  33463  pmapjat2  33464  pmapjlln1  33465  hlmod1i  33466  atmod1i1m  33468  llnmod1i2  33470  atmod2i1  33471  atmod2i2  33472  llnmod2i2  33473  atmod3i1  33474  atmod3i2  33475  atmod4i1  33476  atmod4i2  33477  llnexchb2lem  33478  llnexchb2  33479  llnexch2N  33480  dalawlem1  33481  dalawlem2  33482  dalawlem3  33483  dalawlem4  33484  dalawlem5  33485  dalawlem6  33486  dalawlem7  33487  dalawlem8  33488  dalawlem9  33489  dalawlem11  33491  dalawlem12  33492  dalawlem15  33495  polsubN  33517  paddunN  33537  pmapj2N  33539  pmapocjN  33540  psubclinN  33558  paddatclN  33559  pclfinclN  33560  linepsubclN  33561  poml4N  33563  osumcllem5N  33570  osumcllem7N  33572  pexmidlem2N  33581  pexmidlem4N  33583  pl42lem1N  33589  pl42lem2N  33590  pl42lem4N  33592  pl42N  33593  lhp2lt  33611  lhpexle2lem  33619  lhpexle3lem  33621  lhpocnle  33626  lhpjat2  33631  lhpj1  33632  lhpmcvr  33633  lhpmcvr3  33635  lhpmcvr4N  33636  lhpmcvr5N  33637  lhpmcvr6N  33638  lhpm0atN  33639  lhpmatb  33641  lhp2at0  33642  lhp2atnle  33643  lhpelim  33647  lhpmod2i2  33648  lhpmod6i1  33649  lhprelat3N  33650  lhple  33652  lhpat3  33656  4atexlemkl  33667  ltrnm  33741  ltrnj  33742  ltrnel  33749  ltrncnvel  33752  ltrnmwOLD  33762  trlval2  33774  trlcl  33775  trljat1  33777  trljat2  33778  trlle  33795  trlval3  33798  arglem1N  33801  cdlemc1  33802  cdlemc2  33803  cdlemc4  33805  cdlemc5  33806  cdlemc6  33807  cdlemd1  33809  cdlemd2  33810  cdlemd3  33811  cdlemd4  33812  cdlemd7  33815  cdleme0aa  33821  cdleme0b  33823  cdleme0c  33824  cdleme0cp  33825  cdleme0cq  33826  cdleme0e  33828  cdleme0fN  33829  cdlemeulpq  33831  cdleme01N  33832  cdleme0ex1N  33834  cdleme1b  33837  cdleme1  33838  cdleme2  33839  cdleme3b  33840  cdleme3c  33841  cdleme3e  33843  cdleme3g  33845  cdleme3h  33846  cdleme3  33848  cdleme4a  33850  cdleme5  33851  cdleme7aa  33853  cdleme7c  33856  cdleme7d  33857  cdleme7e  33858  cdleme7ga  33859  cdleme7  33860  cdleme8  33861  cdleme9b  33863  cdleme9  33864  cdleme10  33865  cdleme11c  33872  cdleme11e  33874  cdleme11fN  33875  cdleme11g  33876  cdleme11k  33879  cdleme11  33881  cdleme13  33883  cdleme15b  33886  cdleme15d  33888  cdleme15  33889  cdleme16b  33890  cdleme16e  33893  cdleme16f  33894  cdleme17b  33898  cdleme17c  33899  cdleme22gb  33905  cdlemedb  33908  cdlemednpq  33910  cdleme20zN  33912  cdleme19a  33915  cdleme19b  33916  cdleme19c  33917  cdleme19e  33919  cdleme20aN  33921  cdleme20bN  33922  cdleme20c  33923  cdleme20d  33924  cdleme20e  33925  cdleme20j  33930  cdleme20k  33931  cdleme20l2  33933  cdleme20l  33934  cdleme20m  33935  cdleme21c  33939  cdleme21ct  33941  cdleme22aa  33951  cdleme22b  33953  cdleme22cN  33954  cdleme22d  33955  cdleme22e  33956  cdleme22eALTN  33957  cdleme22f  33958  cdleme22g  33960  cdleme23a  33961  cdleme23b  33962  cdleme23c  33963  cdleme27N  33981  cdleme28a  33982  cdleme28b  33983  cdleme29ex  33986  cdleme30a  33990  cdlemefr29exN  34014  cdleme32b  34054  cdleme32c  34055  cdleme32e  34057  cdleme35a  34060  cdleme35fnpq  34061  cdleme35b  34062  cdleme35c  34063  cdleme35d  34064  cdleme35f  34066  cdleme42c  34084  cdleme42e  34091  cdleme42h  34094  cdleme42i  34095  cdleme42mgN  34100  cdleme48bw  34114  cdlemeg46frv  34137  cdlemeg46vrg  34139  cdlemeg46rgv  34140  cdlemeg46req  34141  cdleme50eq  34153  cdlemf1  34173  cdlemf2  34174  trlord  34181  cdlemg2fv2  34212  cdlemg2m  34216  cdlemg7fvbwN  34219  cdlemg4c  34224  cdlemg4  34229  cdlemg6c  34232  cdlemg8b  34240  cdlemg10bALTN  34248  cdlemg10c  34251  cdlemg10  34253  cdlemg11b  34254  cdlemg12f  34260  cdlemg12g  34261  cdlemg12  34262  cdlemg13a  34263  cdlemg17a  34273  cdlemg17dALTN  34276  cdlemg17  34289  cdlemg18b  34291  cdlemg19a  34295  cdlemg19  34296  cdlemg27a  34304  cdlemg27b  34308  cdlemg31a  34309  cdlemg31b  34310  cdlemg33b0  34313  cdlemg33a  34318  cdlemg35  34325  trlcolem  34338  cdlemg42  34341  cdlemg44a  34343  cdlemg46  34347  trljco  34352  trljco2  34353  tendoidcl  34381  tendococl  34384  tendopltp  34392  cdlemh1  34427  cdlemh2  34428  cdlemi1  34430  cdlemi  34432  cdlemk3  34445  cdlemk4  34446  cdlemkvcl  34454  cdlemk10  34455  cdlemk7  34460  cdlemk11  34461  cdlemk12  34462  cdlemkole  34465  cdlemk14  34466  cdlemk15  34467  cdlemk1u  34471  cdlemk5u  34473  cdlemk7u  34482  cdlemk11u  34483  cdlemk12u  34484  cdlemk37  34526  cdlemk39  34528  cdlemkid1  34534  cdlemkid2  34536  cdlemk48  34562  cdlemk50  34564  cdlemk51  34565  cdlemk52  34566  cdlemk39u  34580  dia1eldmN  34654  dialss  34659  dia11N  34661  dia1N  34666  diaglbN  34668  diaintclN  34671  dia2dimlem1  34677  dia2dimlem2  34678  dia2dimlem3  34679  dia2dimlem10  34686  dia2dimlem12  34688  cdlemm10N  34731  docaclN  34737  doca2N  34739  djajN  34750  dib11N  34773  dibglbN  34779  dibintclN  34780  diblss  34783  cdlemn2  34808  cdlemn10  34819  dihjustlem  34829  dihord1  34831  dihord2a  34832  dihord2b  34833  dihord2cN  34834  dihord11b  34835  dihord11c  34837  dihord2pre  34838  dihord2pre2  34839  dihlsscpre  34847  dib2dim  34856  dih2dimb  34857  dih2dimbALTN  34858  dihvalcq2  34860  dihopelvalcpre  34861  dihord6apre  34869  dihord5b  34872  dihord6b  34873  dihord5apre  34875  dih11  34878  dih1  34899  dihwN  34902  dihmeetlem1N  34903  dihglblem5apreN  34904  dihglblem5aN  34905  dihglblem2aN  34906  dihglblem2N  34907  dihglblem3N  34908  dihmeetlem2N  34912  dihglbcpreN  34913  dihmeetbclemN  34917  dihmeetlem3N  34918  dihmeetlem4preN  34919  dihmeetlem6  34922  dihmeetlem7N  34923  dihjatc1  34924  dihjatc2N  34925  dihjatc3  34926  dihmeetlem9N  34928  dihmeetlem10N  34929  dihmeetlem11N  34930  dihmeetlem15N  34934  dihmeetlem16N  34935  dihmeetlem17N  34936  dihmeetlem19N  34938  dihmeetlem20N  34939  dihmeetALTN  34940  dihmeetcl  34958  dihmeet2  34959  dochvalr  34970  djhlj  35014  djhljjN  35015  djhj  35017  dihjatcclem1  35031  dihjatcclem2  35032  dihjatcclem4  35034  dihprrnlem1N  35037  dihprrnlem2  35038  dihjat6  35047  dihjat5N  35050  dvh4dimat  35051