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

Theorem hlatl 29843
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 29842 . 2  |-  ( K  e.  HL  ->  K  e.  CvLat )
2 cvlatl 29808 . 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 1721   AtLatcal 29747   CvLatclc 29748   HLchlt 29833
This theorem is referenced by:  hllat  29846  hlomcmat  29847  intnatN  29889  cvratlem  29903  atcvrj0  29910  atcvrneN  29912  atcvrj1  29913  atcvrj2b  29914  atltcvr  29917  cvrat4  29925  2atjm  29927  atbtwn  29928  3dim2  29950  2dim  29952  1cvrjat  29957  ps-2  29960  ps-2b  29964  islln3  29992  llnnleat  29995  llnexatN  30003  2llnmat  30006  2atm  30009  2llnm3N  30051  2llnm4  30052  2llnmeqat  30053  dalem21  30176  dalem24  30179  dalem25  30180  dalem54  30208  dalem55  30209  dalem57  30211  pmapat  30245  pmapeq0  30248  isline4N  30259  2lnat  30266  2llnma1b  30268  cdlema2N  30274  cdlemblem  30275  pmapjat1  30335  llnexchb2lem  30350  pol1N  30392  pnonsingN  30415  pclfinclN  30432  lhpocnle  30498  lhpmat  30512  lhpmatb  30513  lhp2at0  30514  lhp2atnle  30515  lhp2at0nle  30517  lhpat3  30528  4atexlemcnd  30554  ltrnmw  30633  trlatn0  30654  ltrnnidn  30656  trlnidatb  30659  trlnle  30668  trlval3  30669  trlval4  30670  cdlemc5  30677  cdleme0e  30699  cdleme3  30719  cdleme7c  30727  cdleme7ga  30730  cdleme7  30731  cdleme11k  30750  cdleme15b  30757  cdleme16b  30761  cdleme16e  30764  cdleme16f  30765  cdlemednpq  30781  cdleme20zN  30783  cdleme20y  30784  cdleme20j  30800  cdleme22aa  30821  cdleme22cN  30824  cdleme22d  30825  cdlemf2  31044  cdlemb3  31088  cdlemg12e  31129  cdlemg17dALTN  31146  cdlemg19a  31165  cdlemg27b  31178  cdlemg31d  31182  cdlemg33c  31190  cdlemg33e  31192  trlcone  31210  cdlemi  31302  tendotr  31312  cdlemk17  31340  cdlemk52  31436  cdleml1N  31458  dian0  31522  dia0  31535  dia2dimlem1  31547  dia2dimlem2  31548  dia2dimlem3  31549  dih0cnv  31766  dihmeetlem4preN  31789  dihmeetlem7N  31793  dihmeetlem17N  31806  dihlspsnat  31816  dihatexv  31821
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-cvlat 29805  df-hlat 29834
  Copyright terms: Public domain W3C validator