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 34130
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 34127 . 2 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
2 atllat 34067 . 2 (𝐾 ∈ AtLat → 𝐾 ∈ Lat)
31, 2syl 17 1 (𝐾 ∈ HL → 𝐾 ∈ Lat)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  Latclat 16966  AtLatcal 34031  HLchlt 34117
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-dm 5084  df-iota 5810  df-fv 5855  df-ov 6607  df-atl 34065  df-cvlat 34089  df-hlat 34118
This theorem is referenced by:  hlpos  34132  hlatjcl  34133  hlatjcom  34134  hlatjidm  34135  hlatjass  34136  hlatj32  34138  hlatj4  34140  hlatlej1  34141  atnlej1  34145  atnlej2  34146  hlateq  34165  hlrelat5N  34167  hlrelat  34168  hlrelat2  34169  exatleN  34170  intnatN  34173  cvr2N  34177  hlrelat3  34178  cvrval3  34179  cvrval5  34181  cvrexchlem  34185  cvrexch  34186  cvratlem  34187  cvrat  34188  lnnat  34193  cvrat2  34195  atcvrj2b  34198  atltcvr  34201  atlelt  34204  2atlt  34205  atexchcvrN  34206  cvrat3  34208  cvrat4  34209  cvrat42  34210  2atjm  34211  atbtwn  34212  3noncolr2  34215  4noncolr3  34219  athgt  34222  3dim0  34223  3dimlem3a  34226  3dimlem3OLDN  34228  3dimlem4a  34229  3dimlem4OLDN  34231  3dim3  34235  1cvratex  34239  1cvrjat  34241  1cvrat  34242  ps-1  34243  ps-2  34244  hlatexch3N  34246  hlatexch4  34247  ps-2b  34248  3atlem1  34249  3atlem2  34250  3atlem4  34252  3atlem5  34253  3atlem6  34254  3at  34256  llnneat  34280  2llnmat  34290  2at0mat0  34291  2atm  34293  ps-2c  34294  lplni2  34303  llnmlplnN  34305  lplnle  34306  2atnelpln  34310  lplnneat  34311  lplnnelln  34312  islpln2a  34314  2lplnmN  34325  2llnmj  34326  2atmat  34327  lplnexllnN  34330  2llnjaN  34332  2llnm2N  34334  2llnm3N  34335  2llnm4  34336  2llnmeqat  34337  lvoli3  34343  islvol5  34345  lvoli2  34347  lvolnle3at  34348  3atnelvolN  34352  lvolneatN  34354  lvolnelln  34355  lvolnelpln  34356  islvol2aN  34358  4atlem3  34362  4atlem3a  34363  4atlem3b  34364  4atlem4a  34365  4atlem4b  34366  4atlem4c  34367  4atlem4d  34368  4atlem9  34369  4atlem10a  34370  4atlem10  34372  4atlem11a  34373  4atlem11b  34374  4atlem11  34375  4atlem12a  34376  4atlem12b  34377  4atlem12  34378  4at  34379  4at2  34380  lplncvrlvol2  34381  lplncvrlvol  34382  2lplnja  34385  2lplnm2N  34387  2lplnmj  34388  dalemkelat  34390  pmap11  34528  isline3  34542  lneq2at  34544  lncvrelatN  34547  lncmp  34549  2lnat  34550  2atm2atN  34551  2llnma1b  34552  2llnma3r  34554  cdlema1N  34557  cdlemblem  34559  cdlemb  34560  paddasslem2  34587  paddasslem5  34590  paddasslem8  34593  paddasslem12  34597  paddasslem13  34598  paddasslem15  34600  paddasslem16  34601  paddass  34604  padd12N  34605  pmodlem1  34612  pmodlem2  34613  pmod2iN  34615  pmodN  34616  pmapjat1  34619  pmapjat2  34620  pmapjlln1  34621  hlmod1i  34622  atmod1i1m  34624  llnmod1i2  34626  atmod2i1  34627  atmod2i2  34628  llnmod2i2  34629  atmod3i1  34630  atmod3i2  34631  atmod4i1  34632  atmod4i2  34633  llnexchb2lem  34634  llnexchb2  34635  llnexch2N  34636  dalawlem1  34637  dalawlem2  34638  dalawlem3  34639  dalawlem4  34640  dalawlem5  34641  dalawlem6  34642  dalawlem7  34643  dalawlem8  34644  dalawlem9  34645  dalawlem11  34647  dalawlem12  34648  dalawlem15  34651  polsubN  34673  paddunN  34693  pmapj2N  34695  pmapocjN  34696  psubclinN  34714  paddatclN  34715  pclfinclN  34716  linepsubclN  34717  poml4N  34719  osumcllem5N  34726  osumcllem7N  34728  pexmidlem2N  34737  pexmidlem4N  34739  pl42lem1N  34745  pl42lem2N  34746  pl42lem4N  34748  pl42N  34749  lhp2lt  34767  lhpexle2lem  34775  lhpexle3lem  34777  lhpocnle  34782  lhpjat2  34787  lhpj1  34788  lhpmcvr  34789  lhpmcvr3  34791  lhpmcvr4N  34792  lhpmcvr5N  34793  lhpmcvr6N  34794  lhpm0atN  34795  lhpmatb  34797  lhp2at0  34798  lhp2atnle  34799  lhpelim  34803  lhpmod2i2  34804  lhpmod6i1  34805  lhprelat3N  34806  lhple  34808  lhpat3  34812  4atexlemkl  34823  ltrnm  34897  ltrnj  34898  ltrnel  34905  ltrncnvel  34908  ltrnmwOLD  34918  trlval2  34930  trlcl  34931  trljat1  34933  trljat2  34934  trlle  34951  trlval3  34954  arglem1N  34957  cdlemc1  34958  cdlemc2  34959  cdlemc4  34961  cdlemc5  34962  cdlemc6  34963  cdlemd1  34965  cdlemd2  34966  cdlemd3  34967  cdlemd4  34968  cdlemd7  34971  cdleme0aa  34977  cdleme0b  34979  cdleme0c  34980  cdleme0cp  34981  cdleme0cq  34982  cdleme0e  34984  cdleme0fN  34985  cdlemeulpq  34987  cdleme01N  34988  cdleme0ex1N  34990  cdleme1b  34993  cdleme1  34994  cdleme2  34995  cdleme3b  34996  cdleme3c  34997  cdleme3e  34999  cdleme3g  35001  cdleme3h  35002  cdleme3  35004  cdleme4a  35006  cdleme5  35007  cdleme7aa  35009  cdleme7c  35012  cdleme7d  35013  cdleme7e  35014  cdleme7ga  35015  cdleme7  35016  cdleme8  35017  cdleme9b  35019  cdleme9  35020  cdleme10  35021  cdleme11c  35028  cdleme11e  35030  cdleme11fN  35031  cdleme11g  35032  cdleme11k  35035  cdleme11  35037  cdleme13  35039  cdleme15b  35042  cdleme15d  35044  cdleme15  35045  cdleme16b  35046  cdleme16e  35049  cdleme16f  35050  cdleme17b  35054  cdleme17c  35055  cdleme22gb  35061  cdlemedb  35064  cdlemednpq  35066  cdleme20zN  35068  cdleme19a  35071  cdleme19b  35072  cdleme19c  35073  cdleme19e  35075  cdleme20aN  35077  cdleme20bN  35078  cdleme20c  35079  cdleme20d  35080  cdleme20e  35081  cdleme20j  35086  cdleme20k  35087  cdleme20l2  35089  cdleme20l  35090  cdleme20m  35091  cdleme21c  35095  cdleme21ct  35097  cdleme22aa  35107  cdleme22b  35109  cdleme22cN  35110  cdleme22d  35111  cdleme22e  35112  cdleme22eALTN  35113  cdleme22f  35114  cdleme22g  35116  cdleme23a  35117  cdleme23b  35118  cdleme23c  35119  cdleme27N  35137  cdleme28a  35138  cdleme28b  35139  cdleme29ex  35142  cdleme30a  35146  cdlemefr29exN  35170  cdleme32b  35210  cdleme32c  35211  cdleme32e  35213  cdleme35a  35216  cdleme35fnpq  35217  cdleme35b  35218  cdleme35c  35219  cdleme35d  35220  cdleme35f  35222  cdleme42c  35240  cdleme42e  35247  cdleme42h  35250  cdleme42i  35251  cdleme42mgN  35256  cdleme48bw  35270  cdlemeg46frv  35293  cdlemeg46vrg  35295  cdlemeg46rgv  35296  cdlemeg46req  35297  cdleme50eq  35309  cdlemf1  35329  cdlemf2  35330  trlord  35337  cdlemg2fv2  35368  cdlemg2m  35372  cdlemg7fvbwN  35375  cdlemg4c  35380  cdlemg4  35385  cdlemg6c  35388  cdlemg8b  35396  cdlemg10bALTN  35404  cdlemg10c  35407  cdlemg10  35409  cdlemg11b  35410  cdlemg12f  35416  cdlemg12g  35417  cdlemg12  35418  cdlemg13a  35419  cdlemg17a  35429  cdlemg17dALTN  35432  cdlemg17  35445  cdlemg18b  35447  cdlemg19a  35451  cdlemg19  35452  cdlemg27a  35460  cdlemg27b  35464  cdlemg31a  35465  cdlemg31b  35466  cdlemg33b0  35469  cdlemg33a  35474  cdlemg35  35481  trlcolem  35494  cdlemg42  35497  cdlemg44a  35499  cdlemg46  35503  trljco  35508  trljco2  35509  tendoidcl  35537  tendococl  35540  tendopltp  35548  cdlemh1  35583  cdlemh2  35584  cdlemi1  35586  cdlemi  35588  cdlemk3  35601  cdlemk4  35602  cdlemkvcl  35610  cdlemk10  35611  cdlemk7  35616  cdlemk11  35617  cdlemk12  35618  cdlemkole  35621  cdlemk14  35622  cdlemk15  35623  cdlemk1u  35627  cdlemk5u  35629  cdlemk7u  35638  cdlemk11u  35639  cdlemk12u  35640  cdlemk37  35682  cdlemk39  35684  cdlemkid1  35690  cdlemkid2  35692  cdlemk48  35718  cdlemk50  35720  cdlemk51  35721  cdlemk52  35722  cdlemk39u  35736  dia1eldmN  35810  dialss  35815  dia11N  35817  dia1N  35822  diaglbN  35824  diaintclN  35827  dia2dimlem1  35833  dia2dimlem2  35834  dia2dimlem3  35835  dia2dimlem10  35842  dia2dimlem12  35844  cdlemm10N  35887  docaclN  35893  doca2N  35895  djajN  35906  dib11N  35929  dibglbN  35935  dibintclN  35936  diblss  35939  cdlemn2  35964  cdlemn10  35975  dihjustlem  35985  dihord1  35987  dihord2a  35988  dihord2b  35989  dihord2cN  35990  dihord11b  35991  dihord11c  35993  dihord2pre  35994  dihord2pre2  35995  dihlsscpre  36003  dib2dim  36012  dih2dimb  36013  dih2dimbALTN  36014  dihvalcq2  36016  dihopelvalcpre  36017  dihord6apre  36025  dihord5b  36028  dihord6b  36029  dihord5apre  36031  dih11  36034  dih1  36055  dihwN  36058  dihmeetlem1N  36059  dihglblem5apreN  36060  dihglblem5aN  36061  dihglblem2aN  36062  dihglblem2N  36063  dihglblem3N  36064  dihmeetlem2N  36068  dihglbcpreN  36069  dihmeetbclemN  36073  dihmeetlem3N  36074  dihmeetlem4preN  36075  dihmeetlem6  36078  dihmeetlem7N  36079  dihjatc1  36080  dihjatc2N  36081  dihjatc3  36082  dihmeetlem9N  36084  dihmeetlem10N  36085  dihmeetlem11N  36086  dihmeetlem15N  36090  dihmeetlem16N  36091  dihmeetlem17N  36092  dihmeetlem19N  36094  dihmeetlem20N  36095  dihmeetALTN  36096  dihmeetcl  36114  dihmeet2  36115  dochvalr  36126  djhlj  36170  djhljjN  36171  djhj  36173  dihjatcclem1  36187  dihjatcclem2  36188  dihjatcclem4  36190  dihprrnlem1N  36193  dihprrnlem2  36194  dihjat6  36203  dihjat5N  36206  dvh4dimat  36207
  Copyright terms: Public domain W3C validator