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

Theorem hlatl 30256
Description: A Hilbert lattice is atomic. (Contributed by NM, 20-Oct-2011.)
Assertion
Ref Expression
hlatl  |-  ( K  e.  HL  ->  K  e.  AtLat )

Proof of Theorem hlatl
StepHypRef Expression
1 hlcvl 30255 . 2  |-  ( K  e.  HL  ->  K  e.  CvLat )
2 cvlatl 30221 . 2  |-  ( K  e.  CvLat  ->  K  e.  AtLat
)
31, 2syl 16 1  |-  ( K  e.  HL  ->  K  e.  AtLat )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1727   AtLatcal 30160   CvLatclc 30161   HLchlt 30246
This theorem is referenced by:  hllat  30259  hlomcmat  30260  intnatN  30302  cvratlem  30316  atcvrj0  30323  atcvrneN  30325  atcvrj1  30326  atcvrj2b  30327  atltcvr  30330  cvrat4  30338  2atjm  30340  atbtwn  30341  3dim2  30363  2dim  30365  1cvrjat  30370  ps-2  30373  ps-2b  30377  islln3  30405  llnnleat  30408  llnexatN  30416  2llnmat  30419  2atm  30422  2llnm3N  30464  2llnm4  30465  2llnmeqat  30466  dalem21  30589  dalem24  30592  dalem25  30593  dalem54  30621  dalem55  30622  dalem57  30624  pmapat  30658  pmapeq0  30661  isline4N  30672  2lnat  30679  2llnma1b  30681  cdlema2N  30687  cdlemblem  30688  pmapjat1  30748  llnexchb2lem  30763  pol1N  30805  pnonsingN  30828  pclfinclN  30845  lhpocnle  30911  lhpmat  30925  lhpmatb  30926  lhp2at0  30927  lhp2atnle  30928  lhp2at0nle  30930  lhpat3  30941  4atexlemcnd  30967  ltrnmw  31046  trlatn0  31067  ltrnnidn  31069  trlnidatb  31072  trlnle  31081  trlval3  31082  trlval4  31083  cdlemc5  31090  cdleme0e  31112  cdleme3  31132  cdleme7c  31140  cdleme7ga  31143  cdleme7  31144  cdleme11k  31163  cdleme15b  31170  cdleme16b  31174  cdleme16e  31177  cdleme16f  31178  cdlemednpq  31194  cdleme20zN  31196  cdleme20y  31197  cdleme20j  31213  cdleme22aa  31234  cdleme22cN  31237  cdleme22d  31238  cdlemf2  31457  cdlemb3  31501  cdlemg12e  31542  cdlemg17dALTN  31559  cdlemg19a  31578  cdlemg27b  31591  cdlemg31d  31595  cdlemg33c  31603  cdlemg33e  31605  trlcone  31623  cdlemi  31715  tendotr  31725  cdlemk17  31753  cdlemk52  31849  cdleml1N  31871  dian0  31935  dia0  31948  dia2dimlem1  31960  dia2dimlem2  31961  dia2dimlem3  31962  dih0cnv  32179  dihmeetlem4preN  32202  dihmeetlem7N  32206  dihmeetlem17N  32219  dihlspsnat  32229  dihatexv  32234
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ral 2716  df-rex 2717  df-rab 2720  df-v 2964  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-nul 3614  df-if 3764  df-sn 3844  df-pr 3845  df-op 3847  df-uni 4040  df-br 4238  df-iota 5447  df-fv 5491  df-ov 6113  df-cvlat 30218  df-hlat 30247
  Copyright terms: Public domain W3C validator