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

Theorem hlatl 34960
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 34959 . 2  |-  ( K  e.  HL  ->  K  e.  CvLat )
2 cvlatl 34925 . 2  |-  ( K  e.  CvLat  ->  K  e.  AtLat
)
31, 2syl 16 1  |-  ( K  e.  HL  ->  K  e.  AtLat )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   AtLatcal 34864   CvLatclc 34865   HLchlt 34950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586  df-ov 6284  df-cvlat 34922  df-hlat 34951
This theorem is referenced by:  hllat  34963  hlomcmat  34964  intnatN  35006  cvratlem  35020  atcvrj0  35027  atcvrneN  35029  atcvrj1  35030  atcvrj2b  35031  atltcvr  35034  cvrat4  35042  2atjm  35044  atbtwn  35045  3dim2  35067  2dim  35069  1cvrjat  35074  ps-2  35077  ps-2b  35081  islln3  35109  llnnleat  35112  llnexatN  35120  2llnmat  35123  2atm  35126  2llnm3N  35168  2llnm4  35169  2llnmeqat  35170  dalem21  35293  dalem24  35296  dalem25  35297  dalem54  35325  dalem55  35326  dalem57  35328  pmapat  35362  pmapeq0  35365  isline4N  35376  2lnat  35383  2llnma1b  35385  cdlema2N  35391  cdlemblem  35392  pmapjat1  35452  llnexchb2lem  35467  pol1N  35509  pnonsingN  35532  pclfinclN  35549  lhpocnle  35615  lhpmat  35629  lhpmatb  35630  lhp2at0  35631  lhp2atnle  35632  lhp2at0nle  35634  lhpat3  35645  4atexlemcnd  35671  ltrnmwOLD  35751  trlatn0  35772  ltrnnidn  35774  trlnidatb  35777  trlnle  35786  trlval3  35787  trlval4  35788  cdlemc5  35795  cdleme0e  35817  cdleme3  35837  cdleme7c  35845  cdleme7ga  35848  cdleme7  35849  cdleme11k  35868  cdleme15b  35875  cdleme16b  35879  cdleme16e  35882  cdleme16f  35883  cdlemednpq  35899  cdleme20zN  35901  cdleme20yOLD  35903  cdleme20j  35919  cdleme22aa  35940  cdleme22cN  35943  cdleme22d  35944  cdlemf2  36163  cdlemb3  36207  cdlemg12e  36248  cdlemg17dALTN  36265  cdlemg19a  36284  cdlemg27b  36297  cdlemg31d  36301  cdlemg33c  36309  cdlemg33e  36311  trlcone  36329  cdlemi  36421  tendotr  36431  cdlemk17  36459  cdlemk52  36555  cdleml1N  36577  dian0  36641  dia0  36654  dia2dimlem1  36666  dia2dimlem2  36667  dia2dimlem3  36668  dih0cnv  36885  dihmeetlem4preN  36908  dihmeetlem7N  36912  dihmeetlem17N  36925  dihlspsnat  36935  dihatexv  36940
  Copyright terms: Public domain W3C validator