Theorem hllat 32841

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 32838	. 2 |- ( K e. HL -> K e. AtLat )
2		atllat 32778	. 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 1872   Latclat 16234   AtLatcal 32742   HLchlt 32828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-br 4367  df-dm 4806  df-iota 5508  df-fv 5552  df-ov 6252  df-atl 32776  df-cvlat 32800  df-hlat 32829

This theorem is referenced by:  hlpos  32843  hlatjcl  32844  hlatjcom  32845  hlatjidm  32846  hlatjass  32847  hlatj32  32849  hlatj4  32851  hlatlej1  32852  atnlej1  32856  atnlej2  32857  hlateq  32876  hlrelat5N  32878  hlrelat  32879  hlrelat2  32880  exatleN  32881  intnatN  32884  cvr2N  32888  hlrelat3  32889  cvrval3  32890  cvrval5  32892  cvrexchlem  32896  cvrexch  32897  cvratlem  32898  cvrat  32899  lnnat  32904  cvrat2  32906  atcvrj2b  32909  atltcvr  32912  atlelt  32915  2atlt  32916  atexchcvrN  32917  cvrat3  32919  cvrat4  32920  cvrat42  32921  2atjm  32922  atbtwn  32923  3noncolr2  32926  4noncolr3  32930  athgt  32933  3dim0  32934  3dimlem3a  32937  3dimlem3OLDN  32939  3dimlem4a  32940  3dimlem4OLDN  32942  3dim3  32946  1cvratex  32950  1cvrjat  32952  1cvrat  32953  ps-1  32954  ps-2  32955  hlatexch3N  32957  hlatexch4  32958  ps-2b  32959  3atlem1  32960  3atlem2  32961  3atlem4  32963  3atlem5  32964  3atlem6  32965  3at  32967  llnneat  32991  2llnmat  33001  2at0mat0  33002  2atm  33004  ps-2c  33005  lplni2  33014  llnmlplnN  33016  lplnle  33017  2atnelpln  33021  lplnneat  33022  lplnnelln  33023  islpln2a  33025  2lplnmN  33036  2llnmj  33037  2atmat  33038  lplnexllnN  33041  2llnjaN  33043  2llnm2N  33045  2llnm3N  33046  2llnm4  33047  2llnmeqat  33048  lvoli3  33054  islvol5  33056  lvoli2  33058  lvolnle3at  33059  3atnelvolN  33063  lvolneatN  33065  lvolnelln  33066  lvolnelpln  33067  islvol2aN  33069  4atlem3  33073  4atlem3a  33074  4atlem3b  33075  4atlem4a  33076  4atlem4b  33077  4atlem4c  33078  4atlem4d  33079  4atlem9  33080  4atlem10a  33081  4atlem10  33083  4atlem11a  33084  4atlem11b  33085  4atlem11  33086  4atlem12a  33087  4atlem12b  33088  4atlem12  33089  4at  33090  4at2  33091  lplncvrlvol2  33092  lplncvrlvol  33093  2lplnja  33096  2lplnm2N  33098  2lplnmj  33099  dalemkelat  33101  pmap11  33239  isline3  33253  lneq2at  33255  lncvrelatN  33258  lncmp  33260  2lnat  33261  2atm2atN  33262  2llnma1b  33263  2llnma3r  33265  cdlema1N  33268  cdlemblem  33270  cdlemb  33271  paddasslem2  33298  paddasslem5  33301  paddasslem8  33304  paddasslem12  33308  paddasslem13  33309  paddasslem15  33311  paddasslem16  33312  paddass  33315  padd12N  33316  pmodlem1  33323  pmodlem2  33324  pmod2iN  33326  pmodN  33327  pmapjat1  33330  pmapjat2  33331  pmapjlln1  33332  hlmod1i  33333  atmod1i1m  33335  llnmod1i2  33337  atmod2i1  33338  atmod2i2  33339  llnmod2i2  33340  atmod3i1  33341  atmod3i2  33342  atmod4i1  33343  atmod4i2  33344  llnexchb2lem  33345  llnexchb2  33346  llnexch2N  33347  dalawlem1  33348  dalawlem2  33349  dalawlem3  33350  dalawlem4  33351  dalawlem5  33352  dalawlem6  33353  dalawlem7  33354  dalawlem8  33355  dalawlem9  33356  dalawlem11  33358  dalawlem12  33359  dalawlem15  33362  polsubN  33384  paddunN  33404  pmapj2N  33406  pmapocjN  33407  psubclinN  33425  paddatclN  33426  pclfinclN  33427  linepsubclN  33428  poml4N  33430  osumcllem5N  33437  osumcllem7N  33439  pexmidlem2N  33448  pexmidlem4N  33450  pl42lem1N  33456  pl42lem2N  33457  pl42lem4N  33459  pl42N  33460  lhp2lt  33478  lhpexle2lem  33486  lhpexle3lem  33488  lhpocnle  33493  lhpjat2  33498  lhpj1  33499  lhpmcvr  33500  lhpmcvr3  33502  lhpmcvr4N  33503  lhpmcvr5N  33504  lhpmcvr6N  33505  lhpm0atN  33506  lhpmatb  33508  lhp2at0  33509  lhp2atnle  33510  lhpelim  33514  lhpmod2i2  33515  lhpmod6i1  33516  lhprelat3N  33517  lhple  33519  lhpat3  33523  4atexlemkl  33534  ltrnm  33608  ltrnj  33609  ltrnel  33616  ltrncnvel  33619  ltrnmwOLD  33629  trlval2  33641  trlcl  33642  trljat1  33644  trljat2  33645  trlle  33662  trlval3  33665  arglem1N  33668  cdlemc1  33669  cdlemc2  33670  cdlemc4  33672  cdlemc5  33673  cdlemc6  33674  cdlemd1  33676  cdlemd2  33677  cdlemd3  33678  cdlemd4  33679  cdlemd7  33682  cdleme0aa  33688  cdleme0b  33690  cdleme0c  33691  cdleme0cp  33692  cdleme0cq  33693  cdleme0e  33695  cdleme0fN  33696  cdlemeulpq  33698  cdleme01N  33699  cdleme0ex1N  33701  cdleme1b  33704  cdleme1  33705  cdleme2  33706  cdleme3b  33707  cdleme3c  33708  cdleme3e  33710  cdleme3g  33712  cdleme3h  33713  cdleme3  33715  cdleme4a  33717  cdleme5  33718  cdleme7aa  33720  cdleme7c  33723  cdleme7d  33724  cdleme7e  33725  cdleme7ga  33726  cdleme7  33727  cdleme8  33728  cdleme9b  33730  cdleme9  33731  cdleme10  33732  cdleme11c  33739  cdleme11e  33741  cdleme11fN  33742  cdleme11g  33743  cdleme11k  33746  cdleme11  33748  cdleme13  33750  cdleme15b  33753  cdleme15d  33755  cdleme15  33756  cdleme16b  33757  cdleme16e  33760  cdleme16f  33761  cdleme17b  33765  cdleme17c  33766  cdleme22gb  33772  cdlemedb  33775  cdlemednpq  33777  cdleme20zN  33779  cdleme19a  33782  cdleme19b  33783  cdleme19c  33784  cdleme19e  33786  cdleme20aN  33788  cdleme20bN  33789  cdleme20c  33790  cdleme20d  33791  cdleme20e  33792  cdleme20j  33797  cdleme20k  33798  cdleme20l2  33800  cdleme20l  33801  cdleme20m  33802  cdleme21c  33806  cdleme21ct  33808  cdleme22aa  33818  cdleme22b  33820  cdleme22cN  33821  cdleme22d  33822  cdleme22e  33823  cdleme22eALTN  33824  cdleme22f  33825  cdleme22g  33827  cdleme23a  33828  cdleme23b  33829  cdleme23c  33830  cdleme27N  33848  cdleme28a  33849  cdleme28b  33850  cdleme29ex  33853  cdleme30a  33857  cdlemefr29exN  33881  cdleme32b  33921  cdleme32c  33922  cdleme32e  33924  cdleme35a  33927  cdleme35fnpq  33928  cdleme35b  33929  cdleme35c  33930  cdleme35d  33931  cdleme35f  33933  cdleme42c  33951  cdleme42e  33958  cdleme42h  33961  cdleme42i  33962  cdleme42mgN  33967  cdleme48bw  33981  cdlemeg46frv  34004  cdlemeg46vrg  34006  cdlemeg46rgv  34007  cdlemeg46req  34008  cdleme50eq  34020  cdlemf1  34040  cdlemf2  34041  trlord  34048  cdlemg2fv2  34079  cdlemg2m  34083  cdlemg7fvbwN  34086  cdlemg4c  34091  cdlemg4  34096  cdlemg6c  34099  cdlemg8b  34107  cdlemg10bALTN  34115  cdlemg10c  34118  cdlemg10  34120  cdlemg11b  34121  cdlemg12f  34127  cdlemg12g  34128  cdlemg12  34129  cdlemg13a  34130  cdlemg17a  34140  cdlemg17dALTN  34143  cdlemg17  34156  cdlemg18b  34158  cdlemg19a  34162  cdlemg19  34163  cdlemg27a  34171  cdlemg27b  34175  cdlemg31a  34176  cdlemg31b  34177  cdlemg33b0  34180  cdlemg33a  34185  cdlemg35  34192  trlcolem  34205  cdlemg42  34208  cdlemg44a  34210  cdlemg46  34214  trljco  34219  trljco2  34220  tendoidcl  34248  tendococl  34251  tendopltp  34259  cdlemh1  34294  cdlemh2  34295  cdlemi1  34297  cdlemi  34299  cdlemk3  34312  cdlemk4  34313  cdlemkvcl  34321  cdlemk10  34322  cdlemk7  34327  cdlemk11  34328  cdlemk12  34329  cdlemkole  34332  cdlemk14  34333  cdlemk15  34334  cdlemk1u  34338  cdlemk5u  34340  cdlemk7u  34349  cdlemk11u  34350  cdlemk12u  34351  cdlemk37  34393  cdlemk39  34395  cdlemkid1  34401  cdlemkid2  34403  cdlemk48  34429  cdlemk50  34431  cdlemk51  34432  cdlemk52  34433  cdlemk39u  34447  dia1eldmN  34521  dialss  34526  dia11N  34528  dia1N  34533  diaglbN  34535  diaintclN  34538  dia2dimlem1  34544  dia2dimlem2  34545  dia2dimlem3  34546  dia2dimlem10  34553  dia2dimlem12  34555  cdlemm10N  34598  docaclN  34604  doca2N  34606  djajN  34617  dib11N  34640  dibglbN  34646  dibintclN  34647  diblss  34650  cdlemn2  34675  cdlemn10  34686  dihjustlem  34696  dihord1  34698  dihord2a  34699  dihord2b  34700  dihord2cN  34701  dihord11b  34702  dihord11c  34704  dihord2pre  34705  dihord2pre2  34706  dihlsscpre  34714  dib2dim  34723  dih2dimb  34724  dih2dimbALTN  34725  dihvalcq2  34727  dihopelvalcpre  34728  dihord6apre  34736  dihord5b  34739  dihord6b  34740  dihord5apre  34742  dih11  34745  dih1  34766  dihwN  34769  dihmeetlem1N  34770  dihglblem5apreN  34771  dihglblem5aN  34772  dihglblem2aN  34773  dihglblem2N  34774  dihglblem3N  34775  dihmeetlem2N  34779  dihglbcpreN  34780  dihmeetbclemN  34784  dihmeetlem3N  34785  dihmeetlem4preN  34786  dihmeetlem6  34789  dihmeetlem7N  34790  dihjatc1  34791  dihjatc2N  34792  dihjatc3  34793  dihmeetlem9N  34795  dihmeetlem10N  34796  dihmeetlem11N  34797  dihmeetlem15N  34801  dihmeetlem16N  34802  dihmeetlem17N  34803  dihmeetlem19N  34805  dihmeetlem20N  34806  dihmeetALTN  34807  dihmeetcl  34825  dihmeet2  34826  dochvalr  34837  djhlj  34881  djhljjN  34882  djhj  34884  dihjatcclem1  34898  dihjatcclem2  34899  dihjatcclem4  34901  dihprrnlem1N  34904  dihprrnlem2  34905  dihjat6  34914  dihjat5N  34917  dvh4dimat  34918