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 35070
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 35067 . 2 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
2 atllat 35007 . 2 (𝐾 ∈ AtLat → 𝐾 ∈ Lat)
31, 2syl 17 1 (𝐾 ∈ HL → 𝐾 ∈ Lat)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2103  Latclat 17167  AtLatcal 34971  HLchlt 35057
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-ral 3019  df-rex 3020  df-rab 3023  df-v 3306  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-br 4761  df-dm 5228  df-iota 5964  df-fv 6009  df-ov 6768  df-atl 35005  df-cvlat 35029  df-hlat 35058
This theorem is referenced by:  hlpos  35072  hlatjcl  35073  hlatjcom  35074  hlatjidm  35075  hlatjass  35076  hlatj32  35078  hlatj4  35080  hlatlej1  35081  atnlej1  35085  atnlej2  35086  hlateq  35105  hlrelat5N  35107  hlrelat  35108  hlrelat2  35109  exatleN  35110  intnatN  35113  cvr2N  35117  hlrelat3  35118  cvrval3  35119  cvrval5  35121  cvrexchlem  35125  cvrexch  35126  cvratlem  35127  cvrat  35128  lnnat  35133  cvrat2  35135  atcvrj2b  35138  atltcvr  35141  atlelt  35144  2atlt  35145  atexchcvrN  35146  cvrat3  35148  cvrat4  35149  cvrat42  35150  2atjm  35151  atbtwn  35152  3noncolr2  35155  4noncolr3  35159  athgt  35162  3dim0  35163  3dimlem3a  35166  3dimlem3OLDN  35168  3dimlem4a  35169  3dimlem4OLDN  35171  3dim3  35175  1cvratex  35179  1cvrjat  35181  1cvrat  35182  ps-1  35183  ps-2  35184  hlatexch3N  35186  hlatexch4  35187  ps-2b  35188  3atlem1  35189  3atlem2  35190  3atlem4  35192  3atlem5  35193  3atlem6  35194  3at  35196  llnneat  35220  2llnmat  35230  2at0mat0  35231  2atm  35233  ps-2c  35234  lplni2  35243  llnmlplnN  35245  lplnle  35246  2atnelpln  35250  lplnneat  35251  lplnnelln  35252  islpln2a  35254  2lplnmN  35265  2llnmj  35266  2atmat  35267  lplnexllnN  35270  2llnjaN  35272  2llnm2N  35274  2llnm3N  35275  2llnm4  35276  2llnmeqat  35277  lvoli3  35283  islvol5  35285  lvoli2  35287  lvolnle3at  35288  3atnelvolN  35292  lvolneatN  35294  lvolnelln  35295  lvolnelpln  35296  islvol2aN  35298  4atlem3  35302  4atlem3a  35303  4atlem3b  35304  4atlem4a  35305  4atlem4b  35306  4atlem4c  35307  4atlem4d  35308  4atlem9  35309  4atlem10a  35310  4atlem10  35312  4atlem11a  35313  4atlem11b  35314  4atlem11  35315  4atlem12a  35316  4atlem12b  35317  4atlem12  35318  4at  35319  4at2  35320  lplncvrlvol2  35321  lplncvrlvol  35322  2lplnja  35325  2lplnm2N  35327  2lplnmj  35328  dalemkelat  35330  pmap11  35468  isline3  35482  lneq2at  35484  lncvrelatN  35487  lncmp  35489  2lnat  35490  2atm2atN  35491  2llnma1b  35492  2llnma3r  35494  cdlema1N  35497  cdlemblem  35499  cdlemb  35500  paddasslem2  35527  paddasslem5  35530  paddasslem8  35533  paddasslem12  35537  paddasslem13  35538  paddasslem15  35540  paddasslem16  35541  paddass  35544  padd12N  35545  pmodlem1  35552  pmodlem2  35553  pmod2iN  35555  pmodN  35556  pmapjat1  35559  pmapjat2  35560  pmapjlln1  35561  hlmod1i  35562  atmod1i1m  35564  llnmod1i2  35566  atmod2i1  35567  atmod2i2  35568  llnmod2i2  35569  atmod3i1  35570  atmod3i2  35571  atmod4i1  35572  atmod4i2  35573  llnexchb2lem  35574  llnexchb2  35575  llnexch2N  35576  dalawlem1  35577  dalawlem2  35578  dalawlem3  35579  dalawlem4  35580  dalawlem5  35581  dalawlem6  35582  dalawlem7  35583  dalawlem8  35584  dalawlem9  35585  dalawlem11  35587  dalawlem12  35588  dalawlem15  35591  polsubN  35613  paddunN  35633  pmapj2N  35635  pmapocjN  35636  psubclinN  35654  paddatclN  35655  pclfinclN  35656  linepsubclN  35657  poml4N  35659  osumcllem5N  35666  osumcllem7N  35668  pexmidlem2N  35677  pexmidlem4N  35679  pl42lem1N  35685  pl42lem2N  35686  pl42lem4N  35688  pl42N  35689  lhp2lt  35707  lhpexle2lem  35715  lhpexle3lem  35717  lhpocnle  35722  lhpjat2  35727  lhpj1  35728  lhpmcvr  35729  lhpmcvr3  35731  lhpmcvr4N  35732  lhpmcvr5N  35733  lhpmcvr6N  35734  lhpm0atN  35735  lhpmatb  35737  lhp2at0  35738  lhp2atnle  35739  lhpelim  35743  lhpmod2i2  35744  lhpmod6i1  35745  lhprelat3N  35746  lhple  35748  lhpat3  35752  4atexlemkl  35763  ltrnm  35837  ltrnj  35838  ltrnel  35845  ltrncnvel  35848  ltrnmwOLD  35858  trlval2  35870  trlcl  35871  trljat1  35873  trljat2  35874  trlle  35891  trlval3  35894  arglem1N  35897  cdlemc1  35898  cdlemc2  35899  cdlemc4  35901  cdlemc5  35902  cdlemc6  35903  cdlemd1  35905  cdlemd2  35906  cdlemd3  35907  cdlemd4  35908  cdlemd7  35911  cdleme0aa  35917  cdleme0b  35919  cdleme0c  35920  cdleme0cp  35921  cdleme0cq  35922  cdleme0e  35924  cdleme0fN  35925  cdlemeulpq  35927  cdleme01N  35928  cdleme0ex1N  35930  cdleme1b  35933  cdleme1  35934  cdleme2  35935  cdleme3b  35936  cdleme3c  35937  cdleme3e  35939  cdleme3g  35941  cdleme3h  35942  cdleme3  35944  cdleme4a  35946  cdleme5  35947  cdleme7aa  35949  cdleme7c  35952  cdleme7d  35953  cdleme7e  35954  cdleme7ga  35955  cdleme7  35956  cdleme8  35957  cdleme9b  35959  cdleme9  35960  cdleme10  35961  cdleme11c  35968  cdleme11e  35970  cdleme11fN  35971  cdleme11g  35972  cdleme11k  35975  cdleme11  35977  cdleme13  35979  cdleme15b  35982  cdleme15d  35984  cdleme15  35985  cdleme16b  35986  cdleme16e  35989  cdleme16f  35990  cdleme17b  35994  cdleme17c  35995  cdleme22gb  36001  cdlemedb  36004  cdlemednpq  36006  cdleme20zN  36008  cdleme19a  36010  cdleme19b  36011  cdleme19c  36012  cdleme19e  36014  cdleme20aN  36016  cdleme20bN  36017  cdleme20c  36018  cdleme20d  36019  cdleme20e  36020  cdleme20j  36025  cdleme20k  36026  cdleme20l2  36028  cdleme20l  36029  cdleme20m  36030  cdleme21c  36034  cdleme21ct  36036  cdleme22aa  36046  cdleme22b  36048  cdleme22cN  36049  cdleme22d  36050  cdleme22e  36051  cdleme22eALTN  36052  cdleme22f  36053  cdleme22g  36055  cdleme23a  36056  cdleme23b  36057  cdleme23c  36058  cdleme27N  36076  cdleme28a  36077  cdleme28b  36078  cdleme29ex  36081  cdleme30a  36085  cdlemefr29exN  36109  cdleme32b  36149  cdleme32c  36150  cdleme32e  36152  cdleme35a  36155  cdleme35fnpq  36156  cdleme35b  36157  cdleme35c  36158  cdleme35d  36159  cdleme35f  36161  cdleme42c  36179  cdleme42e  36186  cdleme42h  36189  cdleme42i  36190  cdleme42mgN  36195  cdleme48bw  36209  cdlemeg46frv  36232  cdlemeg46vrg  36234  cdlemeg46rgv  36235  cdlemeg46req  36236  cdleme50eq  36248  cdlemf1  36268  cdlemf2  36269  trlord  36276  cdlemg2fv2  36307  cdlemg2m  36311  cdlemg7fvbwN  36314  cdlemg4c  36319  cdlemg4  36324  cdlemg6c  36327  cdlemg8b  36335  cdlemg10bALTN  36343  cdlemg10c  36346  cdlemg10  36348  cdlemg11b  36349  cdlemg12f  36355  cdlemg12g  36356  cdlemg12  36357  cdlemg13a  36358  cdlemg17a  36368  cdlemg17dALTN  36371  cdlemg17  36384  cdlemg18b  36386  cdlemg19a  36390  cdlemg19  36391  cdlemg27a  36399  cdlemg27b  36403  cdlemg31a  36404  cdlemg31b  36405  cdlemg33b0  36408  cdlemg33a  36413  cdlemg35  36420  trlcolem  36433  cdlemg42  36436  cdlemg44a  36438  cdlemg46  36442  trljco  36447  trljco2  36448  tendoidcl  36476  tendococl  36479  tendopltp  36487  cdlemh1  36522  cdlemh2  36523  cdlemi1  36525  cdlemi  36527  cdlemk3  36540  cdlemk4  36541  cdlemkvcl  36549  cdlemk10  36550  cdlemk7  36555  cdlemk11  36556  cdlemk12  36557  cdlemkole  36560  cdlemk14  36561  cdlemk15  36562  cdlemk1u  36566  cdlemk5u  36568  cdlemk7u  36577  cdlemk11u  36578  cdlemk12u  36579  cdlemk37  36621  cdlemk39  36623  cdlemkid1  36629  cdlemkid2  36631  cdlemk48  36657  cdlemk50  36659  cdlemk51  36660  cdlemk52  36661  cdlemk39u  36675  dia1eldmN  36749  dialss  36754  dia11N  36756  dia1N  36761  diaglbN  36763  diaintclN  36766  dia2dimlem1  36772  dia2dimlem2  36773  dia2dimlem3  36774  dia2dimlem10  36781  dia2dimlem12  36783  cdlemm10N  36826  docaclN  36832  doca2N  36834  djajN  36845  dib11N  36868  dibglbN  36874  dibintclN  36875  diblss  36878  cdlemn2  36903  cdlemn10  36914  dihjustlem  36924  dihord1  36926  dihord2a  36927  dihord2b  36928  dihord2cN  36929  dihord11b  36930  dihord11c  36932  dihord2pre  36933  dihord2pre2  36934  dihlsscpre  36942  dib2dim  36951  dih2dimb  36952  dih2dimbALTN  36953  dihvalcq2  36955  dihopelvalcpre  36956  dihord6apre  36964  dihord5b  36967  dihord6b  36968  dihord5apre  36970  dih11  36973  dih1  36994  dihwN  36997  dihmeetlem1N  36998  dihglblem5apreN  36999  dihglblem5aN  37000  dihglblem2aN  37001  dihglblem2N  37002  dihglblem3N  37003  dihmeetlem2N  37007  dihglbcpreN  37008  dihmeetbclemN  37012  dihmeetlem3N  37013  dihmeetlem4preN  37014  dihmeetlem6  37017  dihmeetlem7N  37018  dihjatc1  37019  dihjatc2N  37020  dihjatc3  37021  dihmeetlem9N  37023  dihmeetlem10N  37024  dihmeetlem11N  37025  dihmeetlem15N  37029  dihmeetlem16N  37030  dihmeetlem17N  37031  dihmeetlem19N  37033  dihmeetlem20N  37034  dihmeetALTN  37035  dihmeetcl  37053  dihmeet2  37054  dochvalr  37065  djhlj  37109  djhljjN  37110  djhj  37112  dihjatcclem1  37126  dihjatcclem2  37127  dihjatcclem4  37129  dihprrnlem1N  37132  dihprrnlem2  37133  dihjat6  37142  dihjat5N  37145  dvh4dimat  37146
  Copyright terms: Public domain W3C validator