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

Theorem hllat 29626
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
StepHypRef Expression
1 hlatl 29623 . 2  |-  ( K  e.  HL  ->  K  e.  AtLat )
2 atllat 29563 . 2  |-  ( K  e.  AtLat  ->  K  e.  Lat )
31, 2syl 15 1  |-  ( K  e.  HL  ->  K  e.  Lat )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1686   Latclat 14153   AtLatcal 29527   HLchlt 29613
This theorem is referenced by:  hlpos  29628  hlatjcl  29629  hlatjcom  29630  hlatjidm  29631  hlatjass  29632  hlatj32  29634  hlatj4  29636  hlatlej1  29637  atnlej1  29641  atnlej2  29642  hlateq  29661  hlrelat5N  29663  hlrelat  29664  hlrelat2  29665  exatleN  29666  intnatN  29669  cvr2N  29673  hlrelat3  29674  cvrval3  29675  cvrval5  29677  cvrexchlem  29681  cvrexch  29682  cvratlem  29683  cvrat  29684  lnnat  29689  cvrat2  29691  atcvrj2b  29694  atltcvr  29697  atlelt  29700  2atlt  29701  atexchcvrN  29702  cvrat3  29704  cvrat4  29705  cvrat42  29706  2atjm  29707  atbtwn  29708  3noncolr2  29711  4noncolr3  29715  athgt  29718  3dim0  29719  3dimlem3a  29722  3dimlem3OLDN  29724  3dimlem4a  29725  3dimlem4OLDN  29727  3dim3  29731  1cvratex  29735  1cvrjat  29737  1cvrat  29738  ps-1  29739  ps-2  29740  hlatexch3N  29742  hlatexch4  29743  ps-2b  29744  3atlem1  29745  3atlem2  29746  3atlem4  29748  3atlem5  29749  3atlem6  29750  3at  29752  llnneat  29776  2llnmat  29786  2at0mat0  29787  2atm  29789  ps-2c  29790  lplni2  29799  llnmlplnN  29801  lplnle  29802  2atnelpln  29806  lplnneat  29807  lplnnelln  29808  islpln2a  29810  2lplnmN  29821  2llnmj  29822  2atmat  29823  lplnexllnN  29826  2llnjaN  29828  2llnm2N  29830  2llnm3N  29831  2llnm4  29832  2llnmeqat  29833  lvoli3  29839  islvol5  29841  lvoli2  29843  lvolnle3at  29844  3atnelvolN  29848  lvolneatN  29850  lvolnelln  29851  lvolnelpln  29852  islvol2aN  29854  4atlem3  29858  4atlem3a  29859  4atlem3b  29860  4atlem4a  29861  4atlem4b  29862  4atlem4c  29863  4atlem4d  29864  4atlem9  29865  4atlem10a  29866  4atlem10  29868  4atlem11a  29869  4atlem11b  29870  4atlem11  29871  4atlem12a  29872  4atlem12b  29873  4atlem12  29874  4at  29875  4at2  29876  lplncvrlvol2  29877  lplncvrlvol  29878  2lplnja  29881  2lplnm2N  29883  2lplnmj  29884  dalemkelat  29886  pmap11  30024  isline3  30038  lneq2at  30040  lncvrelatN  30043  lncmp  30045  2lnat  30046  2atm2atN  30047  2llnma1b  30048  2llnma3r  30050  cdlema1N  30053  cdlemblem  30055  cdlemb  30056  paddasslem2  30083  paddasslem5  30086  paddasslem8  30089  paddasslem12  30093  paddasslem13  30094  paddasslem15  30096  paddasslem16  30097  paddass  30100  padd12N  30101  pmodlem1  30108  pmodlem2  30109  pmod2iN  30111  pmodN  30112  pmapjat1  30115  pmapjat2  30116  pmapjlln1  30117  hlmod1i  30118  atmod1i1m  30120  llnmod1i2  30122  atmod2i1  30123  atmod2i2  30124  llnmod2i2  30125  atmod3i1  30126  atmod3i2  30127  atmod4i1  30128  atmod4i2  30129  llnexchb2lem  30130  llnexchb2  30131  llnexch2N  30132  dalawlem1  30133  dalawlem2  30134  dalawlem3  30135  dalawlem4  30136  dalawlem5  30137  dalawlem6  30138  dalawlem7  30139  dalawlem8  30140  dalawlem9  30141  dalawlem11  30143  dalawlem12  30144  dalawlem15  30147  polsubN  30169  paddunN  30189  pmapj2N  30191  pmapocjN  30192  psubclinN  30210  paddatclN  30211  pclfinclN  30212  linepsubclN  30213  poml4N  30215  osumcllem5N  30222  osumcllem7N  30224  pexmidlem2N  30233  pexmidlem4N  30235  pl42lem1N  30241  pl42lem2N  30242  pl42lem4N  30244  pl42N  30245  lhp2lt  30263  lhpexle2lem  30271  lhpexle3lem  30273  lhpocnle  30278  lhpjat2  30283  lhpj1  30284  lhpmcvr  30285  lhpmcvr3  30287  lhpmcvr4N  30288  lhpmcvr5N  30289  lhpmcvr6N  30290  lhpm0atN  30291  lhpmatb  30293  lhp2at0  30294  lhp2atnle  30295  lhpelim  30299  lhpmod2i2  30300  lhpmod6i1  30301  lhprelat3N  30302  lhple  30304  lhpat3  30308  4atexlemkl  30319  ltrnm  30393  ltrnj  30394  ltrnel  30401  ltrncnvel  30404  ltrnmw  30413  trlval2  30425  trlcl  30426  trljat1  30428  trljat2  30429  trlle  30446  trlval3  30449  arglem1N  30452  cdlemc1  30453  cdlemc2  30454  cdlemc4  30456  cdlemc5  30457  cdlemc6  30458  cdlemd1  30460  cdlemd2  30461  cdlemd3  30462  cdlemd4  30463  cdlemd7  30466  cdleme0aa  30472  cdleme0b  30474  cdleme0c  30475  cdleme0cp  30476  cdleme0cq  30477  cdleme0e  30479  cdleme0fN  30480  cdlemeulpq  30482  cdleme01N  30483  cdleme0ex1N  30485  cdleme1b  30488  cdleme1  30489  cdleme2  30490  cdleme3b  30491  cdleme3c  30492  cdleme3e  30494  cdleme3g  30496  cdleme3h  30497  cdleme3  30499  cdleme4a  30501  cdleme5  30502  cdleme7aa  30504  cdleme7c  30507  cdleme7d  30508  cdleme7e  30509  cdleme7ga  30510  cdleme7  30511  cdleme8  30512  cdleme9b  30514  cdleme9  30515  cdleme10  30516  cdleme11c  30523  cdleme11e  30525  cdleme11fN  30526  cdleme11g  30527  cdleme11k  30530  cdleme11  30532  cdleme13  30534  cdleme15b  30537  cdleme15d  30539  cdleme15  30540  cdleme16b  30541  cdleme16e  30544  cdleme16f  30545  cdleme17b  30549  cdleme17c  30550  cdleme22gb  30556  cdlemedb  30559  cdlemednpq  30561  cdleme20zN  30563  cdleme19a  30565  cdleme19b  30566  cdleme19c  30567  cdleme19e  30569  cdleme20aN  30571  cdleme20bN  30572  cdleme20c  30573  cdleme20d  30574  cdleme20e  30575  cdleme20j  30580  cdleme20k  30581  cdleme20l2  30583  cdleme20l  30584  cdleme20m  30585  cdleme21c  30589  cdleme21ct  30591  cdleme22aa  30601  cdleme22b  30603  cdleme22cN  30604  cdleme22d  30605  cdleme22e  30606  cdleme22eALTN  30607  cdleme22f  30608  cdleme22g  30610  cdleme23a  30611  cdleme23b  30612  cdleme23c  30613  cdleme27N  30631  cdleme28a  30632  cdleme28b  30633  cdleme29ex  30636  cdleme30a  30640  cdlemefr29exN  30664  cdleme32b  30704  cdleme32c  30705  cdleme32e  30707  cdleme35a  30710  cdleme35fnpq  30711  cdleme35b  30712  cdleme35c  30713  cdleme35d  30714  cdleme35f  30716  cdleme42c  30734  cdleme42e  30741  cdleme42h  30744  cdleme42i  30745  cdleme42mgN  30750  cdleme48bw  30764  cdlemeg46frv  30787  cdlemeg46vrg  30789  cdlemeg46rgv  30790  cdlemeg46req  30791  cdleme50eq  30803  cdlemf1  30823  cdlemf2  30824  trlord  30831  cdlemg2fv2  30862  cdlemg2m  30866  cdlemg7fvbwN  30869  cdlemg4c  30874  cdlemg4  30879  cdlemg6c  30882  cdlemg8b  30890  cdlemg10bALTN  30898  cdlemg10c  30901  cdlemg10  30903  cdlemg11b  30904  cdlemg12f  30910  cdlemg12g  30911  cdlemg12  30912  cdlemg13a  30913  cdlemg17a  30923  cdlemg17dALTN  30926  cdlemg17  30939  cdlemg18b  30941  cdlemg19a  30945  cdlemg19  30946  cdlemg27a  30954  cdlemg27b  30958  cdlemg31a  30959  cdlemg31b  30960  cdlemg33b0  30963  cdlemg33a  30968  cdlemg35  30975  trlcolem  30988  cdlemg42  30991  cdlemg44a  30993  cdlemg46  30997  trljco  31002  trljco2  31003  tendoidcl  31031  tendococl  31034  tendopltp  31042  cdlemh1  31077  cdlemh2  31078  cdlemi1  31080  cdlemi  31082  cdlemk3  31095  cdlemk4  31096  cdlemkvcl  31104  cdlemk10  31105  cdlemk7  31110  cdlemk11  31111  cdlemk12  31112  cdlemkole  31115  cdlemk14  31116  cdlemk15  31117  cdlemk1u  31121  cdlemk5u  31123  cdlemk7u  31132  cdlemk11u  31133  cdlemk12u  31134  cdlemk37  31176  cdlemk39  31178  cdlemkid1  31184  cdlemkid2  31186  cdlemk48  31212  cdlemk50  31214  cdlemk51  31215  cdlemk52  31216  cdlemk39u  31230  dia1eldmN  31304  dialss  31309  dia11N  31311  dia1N  31316  diaglbN  31318  diaintclN  31321  dia2dimlem1  31327  dia2dimlem2  31328  dia2dimlem3  31329  dia2dimlem10  31336  dia2dimlem12  31338  cdlemm10N  31381  docaclN  31387  doca2N  31389  djajN  31400  dib11N  31423  dibglbN  31429  dibintclN  31430  diblss  31433  cdlemn2  31458  cdlemn10  31469  dihjustlem  31479  dihord1  31481  dihord2a  31482  dihord2b  31483  dihord2cN  31484  dihord11b  31485  dihord11c  31487  dihord2pre  31488  dihord2pre2  31489  dihlsscpre  31497  dib2dim  31506  dih2dimb  31507  dih2dimbALTN  31508  dihvalcq2  31510  dihopelvalcpre  31511  dihord6apre  31519  dihord5b  31522  dihord6b  31523  dihord5apre  31525  dih11  31528  dih1  31549  dihwN  31552  dihmeetlem1N  31553  dihglblem5apreN  31554  dihglblem5aN  31555  dihglblem2aN  31556  dihglblem2N  31557  dihglblem3N  31558  dihmeetlem2N  31562  dihglbcpreN  31563  dihmeetbclemN  31567  dihmeetlem3N  31568  dihmeetlem4preN  31569  dihmeetlem6  31572  dihmeetlem7N  31573  dihjatc1  31574  dihjatc2N  31575  dihjatc3  31576  dihmeetlem9N  31578  dihmeetlem10N  31579  dihmeetlem11N  31580  dihmeetlem15N  31584  dihmeetlem16N  31585  dihmeetlem17N  31586  dihmeetlem19N  31588  dihmeetlem20N  31589  dihmeetALTN  31590  dihmeetcl  31608  dihmeet2  31609  dochvalr  31620  djhlj  31664  djhljjN  31665  djhj  31667  dihjatcclem1  31681  dihjatcclem2  31682  dihjatcclem4  31684  dihprrnlem1N  31687  dihprrnlem2  31688  dihjat6  31697  dihjat5N  31700  dvh4dimat  31701
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-iota 5221  df-fv 5265  df-ov 5863  df-atl 29561  df-cvlat 29585  df-hlat 29614
  Copyright terms: Public domain W3C validator