Theorem hllat 34650

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 34647	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
2		atllat 34587	. 2 ⊢ (𝐾 ∈ AtLat → 𝐾 ∈ Lat)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)

Syntax hints:   → wi 4   ∈ wcel 1990  Latclat 17045  AtLatcal 34551  HLchlt 34637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-dm 5124  df-iota 5851  df-fv 5896  df-ov 6653  df-atl 34585  df-cvlat 34609  df-hlat 34638

This theorem is referenced by:  hlpos  34652  hlatjcl  34653  hlatjcom  34654  hlatjidm  34655  hlatjass  34656  hlatj32  34658  hlatj4  34660  hlatlej1  34661  atnlej1  34665  atnlej2  34666  hlateq  34685  hlrelat5N  34687  hlrelat  34688  hlrelat2  34689  exatleN  34690  intnatN  34693  cvr2N  34697  hlrelat3  34698  cvrval3  34699  cvrval5  34701  cvrexchlem  34705  cvrexch  34706  cvratlem  34707  cvrat  34708  lnnat  34713  cvrat2  34715  atcvrj2b  34718  atltcvr  34721  atlelt  34724  2atlt  34725  atexchcvrN  34726  cvrat3  34728  cvrat4  34729  cvrat42  34730  2atjm  34731  atbtwn  34732  3noncolr2  34735  4noncolr3  34739  athgt  34742  3dim0  34743  3dimlem3a  34746  3dimlem3OLDN  34748  3dimlem4a  34749  3dimlem4OLDN  34751  3dim3  34755  1cvratex  34759  1cvrjat  34761  1cvrat  34762  ps-1  34763  ps-2  34764  hlatexch3N  34766  hlatexch4  34767  ps-2b  34768  3atlem1  34769  3atlem2  34770  3atlem4  34772  3atlem5  34773  3atlem6  34774  3at  34776  llnneat  34800  2llnmat  34810  2at0mat0  34811  2atm  34813  ps-2c  34814  lplni2  34823  llnmlplnN  34825  lplnle  34826  2atnelpln  34830  lplnneat  34831  lplnnelln  34832  islpln2a  34834  2lplnmN  34845  2llnmj  34846  2atmat  34847  lplnexllnN  34850  2llnjaN  34852  2llnm2N  34854  2llnm3N  34855  2llnm4  34856  2llnmeqat  34857  lvoli3  34863  islvol5  34865  lvoli2  34867  lvolnle3at  34868  3atnelvolN  34872  lvolneatN  34874  lvolnelln  34875  lvolnelpln  34876  islvol2aN  34878  4atlem3  34882  4atlem3a  34883  4atlem3b  34884  4atlem4a  34885  4atlem4b  34886  4atlem4c  34887  4atlem4d  34888  4atlem9  34889  4atlem10a  34890  4atlem10  34892  4atlem11a  34893  4atlem11b  34894  4atlem11  34895  4atlem12a  34896  4atlem12b  34897  4atlem12  34898  4at  34899  4at2  34900  lplncvrlvol2  34901  lplncvrlvol  34902  2lplnja  34905  2lplnm2N  34907  2lplnmj  34908  dalemkelat  34910  pmap11  35048  isline3  35062  lneq2at  35064  lncvrelatN  35067  lncmp  35069  2lnat  35070  2atm2atN  35071  2llnma1b  35072  2llnma3r  35074  cdlema1N  35077  cdlemblem  35079  cdlemb  35080  paddasslem2  35107  paddasslem5  35110  paddasslem8  35113  paddasslem12  35117  paddasslem13  35118  paddasslem15  35120  paddasslem16  35121  paddass  35124  padd12N  35125  pmodlem1  35132  pmodlem2  35133  pmod2iN  35135  pmodN  35136  pmapjat1  35139  pmapjat2  35140  pmapjlln1  35141  hlmod1i  35142  atmod1i1m  35144  llnmod1i2  35146  atmod2i1  35147  atmod2i2  35148  llnmod2i2  35149  atmod3i1  35150  atmod3i2  35151  atmod4i1  35152  atmod4i2  35153  llnexchb2lem  35154  llnexchb2  35155  llnexch2N  35156  dalawlem1  35157  dalawlem2  35158  dalawlem3  35159  dalawlem4  35160  dalawlem5  35161  dalawlem6  35162  dalawlem7  35163  dalawlem8  35164  dalawlem9  35165  dalawlem11  35167  dalawlem12  35168  dalawlem15  35171  polsubN  35193  paddunN  35213  pmapj2N  35215  pmapocjN  35216  psubclinN  35234  paddatclN  35235  pclfinclN  35236  linepsubclN  35237  poml4N  35239  osumcllem5N  35246  osumcllem7N  35248  pexmidlem2N  35257  pexmidlem4N  35259  pl42lem1N  35265  pl42lem2N  35266  pl42lem4N  35268  pl42N  35269  lhp2lt  35287  lhpexle2lem  35295  lhpexle3lem  35297  lhpocnle  35302  lhpjat2  35307  lhpj1  35308  lhpmcvr  35309  lhpmcvr3  35311  lhpmcvr4N  35312  lhpmcvr5N  35313  lhpmcvr6N  35314  lhpm0atN  35315  lhpmatb  35317  lhp2at0  35318  lhp2atnle  35319  lhpelim  35323  lhpmod2i2  35324  lhpmod6i1  35325  lhprelat3N  35326  lhple  35328  lhpat3  35332  4atexlemkl  35343  ltrnm  35417  ltrnj  35418  ltrnel  35425  ltrncnvel  35428  ltrnmwOLD  35438  trlval2  35450  trlcl  35451  trljat1  35453  trljat2  35454  trlle  35471  trlval3  35474  arglem1N  35477  cdlemc1  35478  cdlemc2  35479  cdlemc4  35481  cdlemc5  35482  cdlemc6  35483  cdlemd1  35485  cdlemd2  35486  cdlemd3  35487  cdlemd4  35488  cdlemd7  35491  cdleme0aa  35497  cdleme0b  35499  cdleme0c  35500  cdleme0cp  35501  cdleme0cq  35502  cdleme0e  35504  cdleme0fN  35505  cdlemeulpq  35507  cdleme01N  35508  cdleme0ex1N  35510  cdleme1b  35513  cdleme1  35514  cdleme2  35515  cdleme3b  35516  cdleme3c  35517  cdleme3e  35519  cdleme3g  35521  cdleme3h  35522  cdleme3  35524  cdleme4a  35526  cdleme5  35527  cdleme7aa  35529  cdleme7c  35532  cdleme7d  35533  cdleme7e  35534  cdleme7ga  35535  cdleme7  35536  cdleme8  35537  cdleme9b  35539  cdleme9  35540  cdleme10  35541  cdleme11c  35548  cdleme11e  35550  cdleme11fN  35551  cdleme11g  35552  cdleme11k  35555  cdleme11  35557  cdleme13  35559  cdleme15b  35562  cdleme15d  35564  cdleme15  35565  cdleme16b  35566  cdleme16e  35569  cdleme16f  35570  cdleme17b  35574  cdleme17c  35575  cdleme22gb  35581  cdlemedb  35584  cdlemednpq  35586  cdleme20zN  35588  cdleme19a  35591  cdleme19b  35592  cdleme19c  35593  cdleme19e  35595  cdleme20aN  35597  cdleme20bN  35598  cdleme20c  35599  cdleme20d  35600  cdleme20e  35601  cdleme20j  35606  cdleme20k  35607  cdleme20l2  35609  cdleme20l  35610  cdleme20m  35611  cdleme21c  35615  cdleme21ct  35617  cdleme22aa  35627  cdleme22b  35629  cdleme22cN  35630  cdleme22d  35631  cdleme22e  35632  cdleme22eALTN  35633  cdleme22f  35634  cdleme22g  35636  cdleme23a  35637  cdleme23b  35638  cdleme23c  35639  cdleme27N  35657  cdleme28a  35658  cdleme28b  35659  cdleme29ex  35662  cdleme30a  35666  cdlemefr29exN  35690  cdleme32b  35730  cdleme32c  35731  cdleme32e  35733  cdleme35a  35736  cdleme35fnpq  35737  cdleme35b  35738  cdleme35c  35739  cdleme35d  35740  cdleme35f  35742  cdleme42c  35760  cdleme42e  35767  cdleme42h  35770  cdleme42i  35771  cdleme42mgN  35776  cdleme48bw  35790  cdlemeg46frv  35813  cdlemeg46vrg  35815  cdlemeg46rgv  35816  cdlemeg46req  35817  cdleme50eq  35829  cdlemf1  35849  cdlemf2  35850  trlord  35857  cdlemg2fv2  35888  cdlemg2m  35892  cdlemg7fvbwN  35895  cdlemg4c  35900  cdlemg4  35905  cdlemg6c  35908  cdlemg8b  35916  cdlemg10bALTN  35924  cdlemg10c  35927  cdlemg10  35929  cdlemg11b  35930  cdlemg12f  35936  cdlemg12g  35937  cdlemg12  35938  cdlemg13a  35939  cdlemg17a  35949  cdlemg17dALTN  35952  cdlemg17  35965  cdlemg18b  35967  cdlemg19a  35971  cdlemg19  35972  cdlemg27a  35980  cdlemg27b  35984  cdlemg31a  35985  cdlemg31b  35986  cdlemg33b0  35989  cdlemg33a  35994  cdlemg35  36001  trlcolem  36014  cdlemg42  36017  cdlemg44a  36019  cdlemg46  36023  trljco  36028  trljco2  36029  tendoidcl  36057  tendococl  36060  tendopltp  36068  cdlemh1  36103  cdlemh2  36104  cdlemi1  36106  cdlemi  36108  cdlemk3  36121  cdlemk4  36122  cdlemkvcl  36130  cdlemk10  36131  cdlemk7  36136  cdlemk11  36137  cdlemk12  36138  cdlemkole  36141  cdlemk14  36142  cdlemk15  36143  cdlemk1u  36147  cdlemk5u  36149  cdlemk7u  36158  cdlemk11u  36159  cdlemk12u  36160  cdlemk37  36202  cdlemk39  36204  cdlemkid1  36210  cdlemkid2  36212  cdlemk48  36238  cdlemk50  36240  cdlemk51  36241  cdlemk52  36242  cdlemk39u  36256  dia1eldmN  36330  dialss  36335  dia11N  36337  dia1N  36342  diaglbN  36344  diaintclN  36347  dia2dimlem1  36353  dia2dimlem2  36354  dia2dimlem3  36355  dia2dimlem10  36362  dia2dimlem12  36364  cdlemm10N  36407  docaclN  36413  doca2N  36415  djajN  36426  dib11N  36449  dibglbN  36455  dibintclN  36456  diblss  36459  cdlemn2  36484  cdlemn10  36495  dihjustlem  36505  dihord1  36507  dihord2a  36508  dihord2b  36509  dihord2cN  36510  dihord11b  36511  dihord11c  36513  dihord2pre  36514  dihord2pre2  36515  dihlsscpre  36523  dib2dim  36532  dih2dimb  36533  dih2dimbALTN  36534  dihvalcq2  36536  dihopelvalcpre  36537  dihord6apre  36545  dihord5b  36548  dihord6b  36549  dihord5apre  36551  dih11  36554  dih1  36575  dihwN  36578  dihmeetlem1N  36579  dihglblem5apreN  36580  dihglblem5aN  36581  dihglblem2aN  36582  dihglblem2N  36583  dihglblem3N  36584  dihmeetlem2N  36588  dihglbcpreN  36589  dihmeetbclemN  36593  dihmeetlem3N  36594  dihmeetlem4preN  36595  dihmeetlem6  36598  dihmeetlem7N  36599  dihjatc1  36600  dihjatc2N  36601  dihjatc3  36602  dihmeetlem9N  36604  dihmeetlem10N  36605  dihmeetlem11N  36606  dihmeetlem15N  36610  dihmeetlem16N  36611  dihmeetlem17N  36612  dihmeetlem19N  36614  dihmeetlem20N  36615  dihmeetALTN  36616  dihmeetcl  36634  dihmeet2  36635  dochvalr  36646  djhlj  36690  djhljjN  36691  djhj  36693  dihjatcclem1  36707  dihjatcclem2  36708  dihjatcclem4  36710  dihprrnlem1N  36713  dihprrnlem2  36714  dihjat6  36723  dihjat5N  36726  dvh4dimat  36727