Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hllat Structured version   Visualization version   GIF version

Theorem hllat 35153
Description: A Hilbert lattice is a lattice. (Contributed by NM, 20-Oct-2011.)
Assertion
Ref Expression
hllat (𝐾 ∈ HL → 𝐾 ∈ Lat)

Proof of Theorem hllat
StepHypRef Expression
1 hlatl 35150 . 2 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
2 atllat 35090 . 2 (𝐾 ∈ AtLat → 𝐾 ∈ Lat)
31, 2syl 17 1 (𝐾 ∈ HL → 𝐾 ∈ Lat)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  Latclat 17246  AtLatcal 35054  HLchlt 35140
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-dm 5276  df-iota 6012  df-fv 6057  df-ov 6816  df-atl 35088  df-cvlat 35112  df-hlat 35141
This theorem is referenced by:  hlpos  35155  hlatjcl  35156  hlatjcom  35157  hlatjidm  35158  hlatjass  35159  hlatj32  35161  hlatj4  35163  hlatlej1  35164  atnlej1  35168  atnlej2  35169  hlateq  35188  hlrelat5N  35190  hlrelat  35191  hlrelat2  35192  exatleN  35193  intnatN  35196  cvr2N  35200  hlrelat3  35201  cvrval3  35202  cvrval5  35204  cvrexchlem  35208  cvrexch  35209  cvratlem  35210  cvrat  35211  lnnat  35216  cvrat2  35218  atcvrj2b  35221  atltcvr  35224  atlelt  35227  2atlt  35228  atexchcvrN  35229  cvrat3  35231  cvrat4  35232  cvrat42  35233  2atjm  35234  atbtwn  35235  3noncolr2  35238  4noncolr3  35242  athgt  35245  3dim0  35246  3dimlem3a  35249  3dimlem3OLDN  35251  3dimlem4a  35252  3dimlem4OLDN  35254  3dim3  35258  1cvratex  35262  1cvrjat  35264  1cvrat  35265  ps-1  35266  ps-2  35267  hlatexch3N  35269  hlatexch4  35270  ps-2b  35271  3atlem1  35272  3atlem2  35273  3atlem4  35275  3atlem5  35276  3atlem6  35277  3at  35279  llnneat  35303  2llnmat  35313  2at0mat0  35314  2atm  35316  ps-2c  35317  lplni2  35326  llnmlplnN  35328  lplnle  35329  2atnelpln  35333  lplnneat  35334  lplnnelln  35335  islpln2a  35337  2lplnmN  35348  2llnmj  35349  2atmat  35350  lplnexllnN  35353  2llnjaN  35355  2llnm2N  35357  2llnm3N  35358  2llnm4  35359  2llnmeqat  35360  lvoli3  35366  islvol5  35368  lvoli2  35370  lvolnle3at  35371  3atnelvolN  35375  lvolneatN  35377  lvolnelln  35378  lvolnelpln  35379  islvol2aN  35381  4atlem3  35385  4atlem3a  35386  4atlem3b  35387  4atlem4a  35388  4atlem4b  35389  4atlem4c  35390  4atlem4d  35391  4atlem9  35392  4atlem10a  35393  4atlem10  35395  4atlem11a  35396  4atlem11b  35397  4atlem11  35398  4atlem12a  35399  4atlem12b  35400  4atlem12  35401  4at  35402  4at2  35403  lplncvrlvol2  35404  lplncvrlvol  35405  2lplnja  35408  2lplnm2N  35410  2lplnmj  35411  dalemkelat  35413  pmap11  35551  isline3  35565  lneq2at  35567  lncvrelatN  35570  lncmp  35572  2lnat  35573  2atm2atN  35574  2llnma1b  35575  2llnma3r  35577  cdlema1N  35580  cdlemblem  35582  cdlemb  35583  paddasslem2  35610  paddasslem5  35613  paddasslem8  35616  paddasslem12  35620  paddasslem13  35621  paddasslem15  35623  paddasslem16  35624  paddass  35627  padd12N  35628  pmodlem1  35635  pmodlem2  35636  pmod2iN  35638  pmodN  35639  pmapjat1  35642  pmapjat2  35643  pmapjlln1  35644  hlmod1i  35645  atmod1i1m  35647  llnmod1i2  35649  atmod2i1  35650  atmod2i2  35651  llnmod2i2  35652  atmod3i1  35653  atmod3i2  35654  atmod4i1  35655  atmod4i2  35656  llnexchb2lem  35657  llnexchb2  35658  llnexch2N  35659  dalawlem1  35660  dalawlem2  35661  dalawlem3  35662  dalawlem4  35663  dalawlem5  35664  dalawlem6  35665  dalawlem7  35666  dalawlem8  35667  dalawlem9  35668  dalawlem11  35670  dalawlem12  35671  dalawlem15  35674  polsubN  35696  paddunN  35716  pmapj2N  35718  pmapocjN  35719  psubclinN  35737  paddatclN  35738  pclfinclN  35739  linepsubclN  35740  poml4N  35742  osumcllem5N  35749  osumcllem7N  35751  pexmidlem2N  35760  pexmidlem4N  35762  pl42lem1N  35768  pl42lem2N  35769  pl42lem4N  35771  pl42N  35772  lhp2lt  35790  lhpexle2lem  35798  lhpexle3lem  35800  lhpocnle  35805  lhpjat2  35810  lhpj1  35811  lhpmcvr  35812  lhpmcvr3  35814  lhpmcvr4N  35815  lhpmcvr5N  35816  lhpmcvr6N  35817  lhpm0atN  35818  lhpmatb  35820  lhp2at0  35821  lhp2atnle  35822  lhpelim  35826  lhpmod2i2  35827  lhpmod6i1  35828  lhprelat3N  35829  lhple  35831  lhpat3  35835  4atexlemkl  35846  ltrnm  35920  ltrnj  35921  ltrnel  35928  ltrncnvel  35931  ltrnmwOLD  35941  trlval2  35953  trlcl  35954  trljat1  35956  trljat2  35957  trlle  35974  trlval3  35977  arglem1N  35980  cdlemc1  35981  cdlemc2  35982  cdlemc4  35984  cdlemc5  35985  cdlemc6  35986  cdlemd1  35988  cdlemd2  35989  cdlemd3  35990  cdlemd4  35991  cdlemd7  35994  cdleme0aa  36000  cdleme0b  36002  cdleme0c  36003  cdleme0cp  36004  cdleme0cq  36005  cdleme0e  36007  cdleme0fN  36008  cdlemeulpq  36010  cdleme01N  36011  cdleme0ex1N  36013  cdleme1b  36016  cdleme1  36017  cdleme2  36018  cdleme3b  36019  cdleme3c  36020  cdleme3e  36022  cdleme3g  36024  cdleme3h  36025  cdleme3  36027  cdleme4a  36029  cdleme5  36030  cdleme7aa  36032  cdleme7c  36035  cdleme7d  36036  cdleme7e  36037  cdleme7ga  36038  cdleme7  36039  cdleme8  36040  cdleme9b  36042  cdleme9  36043  cdleme10  36044  cdleme11c  36051  cdleme11e  36053  cdleme11fN  36054  cdleme11g  36055  cdleme11k  36058  cdleme11  36060  cdleme13  36062  cdleme15b  36065  cdleme15d  36067  cdleme15  36068  cdleme16b  36069  cdleme16e  36072  cdleme16f  36073  cdleme17b  36077  cdleme17c  36078  cdleme22gb  36084  cdlemedb  36087  cdlemednpq  36089  cdleme20zN  36091  cdleme19a  36093  cdleme19b  36094  cdleme19c  36095  cdleme19e  36097  cdleme20aN  36099  cdleme20bN  36100  cdleme20c  36101  cdleme20d  36102  cdleme20e  36103  cdleme20j  36108  cdleme20k  36109  cdleme20l2  36111  cdleme20l  36112  cdleme20m  36113  cdleme21c  36117  cdleme21ct  36119  cdleme22aa  36129  cdleme22b  36131  cdleme22cN  36132  cdleme22d  36133  cdleme22e  36134  cdleme22eALTN  36135  cdleme22f  36136  cdleme22g  36138  cdleme23a  36139  cdleme23b  36140  cdleme23c  36141  cdleme27N  36159  cdleme28a  36160  cdleme28b  36161  cdleme29ex  36164  cdleme30a  36168  cdlemefr29exN  36192  cdleme32b  36232  cdleme32c  36233  cdleme32e  36235  cdleme35a  36238  cdleme35fnpq  36239  cdleme35b  36240  cdleme35c  36241  cdleme35d  36242  cdleme35f  36244  cdleme42c  36262  cdleme42e  36269  cdleme42h  36272  cdleme42i  36273  cdleme42mgN  36278  cdleme48bw  36292  cdlemeg46frv  36315  cdlemeg46vrg  36317  cdlemeg46rgv  36318  cdlemeg46req  36319  cdleme50eq  36331  cdlemf1  36351  cdlemf2  36352  trlord  36359  cdlemg2fv2  36390  cdlemg2m  36394  cdlemg7fvbwN  36397  cdlemg4c  36402  cdlemg4  36407  cdlemg6c  36410  cdlemg8b  36418  cdlemg10bALTN  36426  cdlemg10c  36429  cdlemg10  36431  cdlemg11b  36432  cdlemg12f  36438  cdlemg12g  36439  cdlemg12  36440  cdlemg13a  36441  cdlemg17a  36451  cdlemg17dALTN  36454  cdlemg17  36467  cdlemg18b  36469  cdlemg19a  36473  cdlemg19  36474  cdlemg27a  36482  cdlemg27b  36486  cdlemg31a  36487  cdlemg31b  36488  cdlemg33b0  36491  cdlemg33a  36496  cdlemg35  36503  trlcolem  36516  cdlemg42  36519  cdlemg44a  36521  cdlemg46  36525  trljco  36530  trljco2  36531  tendoidcl  36559  tendococl  36562  tendopltp  36570  cdlemh1  36605  cdlemh2  36606  cdlemi1  36608  cdlemi  36610  cdlemk3  36623  cdlemk4  36624  cdlemkvcl  36632  cdlemk10  36633  cdlemk7  36638  cdlemk11  36639  cdlemk12  36640  cdlemkole  36643  cdlemk14  36644  cdlemk15  36645  cdlemk1u  36649  cdlemk5u  36651  cdlemk7u  36660  cdlemk11u  36661  cdlemk12u  36662  cdlemk37  36704  cdlemk39  36706  cdlemkid1  36712  cdlemkid2  36714  cdlemk48  36740  cdlemk50  36742  cdlemk51  36743  cdlemk52  36744  cdlemk39u  36758  dia1eldmN  36832  dialss  36837  dia11N  36839  dia1N  36844  diaglbN  36846  diaintclN  36849  dia2dimlem1  36855  dia2dimlem2  36856  dia2dimlem3  36857  dia2dimlem10  36864  dia2dimlem12  36866  cdlemm10N  36909  docaclN  36915  doca2N  36917  djajN  36928  dib11N  36951  dibglbN  36957  dibintclN  36958  diblss  36961  cdlemn2  36986  cdlemn10  36997  dihjustlem  37007  dihord1  37009  dihord2a  37010  dihord2b  37011  dihord2cN  37012  dihord11b  37013  dihord11c  37015  dihord2pre  37016  dihord2pre2  37017  dihlsscpre  37025  dib2dim  37034  dih2dimb  37035  dih2dimbALTN  37036  dihvalcq2  37038  dihopelvalcpre  37039  dihord6apre  37047  dihord5b  37050  dihord6b  37051  dihord5apre  37053  dih11  37056  dih1  37077  dihwN  37080  dihmeetlem1N  37081  dihglblem5apreN  37082  dihglblem5aN  37083  dihglblem2aN  37084  dihglblem2N  37085  dihglblem3N  37086  dihmeetlem2N  37090  dihglbcpreN  37091  dihmeetbclemN  37095  dihmeetlem3N  37096  dihmeetlem4preN  37097  dihmeetlem6  37100  dihmeetlem7N  37101  dihjatc1  37102  dihjatc2N  37103  dihjatc3  37104  dihmeetlem9N  37106  dihmeetlem10N  37107  dihmeetlem11N  37108  dihmeetlem15N  37112  dihmeetlem16N  37113  dihmeetlem17N  37114  dihmeetlem19N  37116  dihmeetlem20N  37117  dihmeetALTN  37118  dihmeetcl  37136  dihmeet2  37137  dochvalr  37148  djhlj  37192  djhljjN  37193  djhj  37195  dihjatcclem1  37209  dihjatcclem2  37210  dihjatcclem4  37212  dihprrnlem1N  37215  dihprrnlem2  37216  dihjat6  37225  dihjat5N  37228  dvh4dimat  37229
  Copyright terms: Public domain W3C validator