Theorem hlatl 39398

Description: A Hilbert lattice is atomic. (Contributed by NM, 20-Oct-2011.)

Assertion

Ref	Expression
hlatl	⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)

Proof of Theorem hlatl

Step	Hyp	Ref	Expression
1		hlcvl 39397	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat)
2		cvlatl 39363	. 2 ⊢ (𝐾 ∈ CvLat → 𝐾 ∈ AtLat)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)

Syntax hints:   → wi 4   ∈ wcel 2111  AtLatcal 39302  CvLatclc 39303  HLchlt 39388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349  df-cvlat 39360  df-hlat 39389

This theorem is referenced by:  hllat  39401  hlomcmat  39403  intnatN  39445  cvratlem  39459  atcvrj0  39466  atcvrneN  39468  atcvrj1  39469  atcvrj2b  39470  atltcvr  39473  cvrat4  39481  2atjm  39483  atbtwn  39484  3dim2  39506  2dim  39508  1cvrjat  39513  ps-2  39516  ps-2b  39520  islln3  39548  llnnleat  39551  llnexatN  39559  2llnmat  39562  2atm  39565  2llnm3N  39607  2llnm4  39608  2llnmeqat  39609  dalem21  39732  dalem24  39735  dalem25  39736  dalem54  39764  dalem55  39765  dalem57  39767  pmapat  39801  pmapeq0  39804  isline4N  39815  2lnat  39822  2llnma1b  39824  cdlema2N  39830  cdlemblem  39831  pmapjat1  39891  llnexchb2lem  39906  pol1N  39948  pnonsingN  39971  pclfinclN  39988  lhpocnle  40054  lhpmat  40068  lhpmatb  40069  lhp2at0  40070  lhp2atnle  40071  lhp2at0nle  40073  lhpat3  40084  4atexlemcnd  40110  trlatn0  40210  ltrnnidn  40212  trlnidatb  40215  trlnle  40224  trlval3  40225  trlval4  40226  cdlemc5  40233  cdleme0e  40255  cdleme3  40275  cdleme7c  40283  cdleme7ga  40286  cdleme7  40287  cdleme11k  40306  cdleme15b  40313  cdleme16b  40317  cdleme16e  40320  cdleme16f  40321  cdlemednpq  40337  cdleme20zN  40339  cdleme20j  40356  cdleme22aa  40377  cdleme22cN  40380  cdleme22d  40381  cdlemf2  40600  cdlemb3  40644  cdlemg12e  40685  cdlemg17dALTN  40702  cdlemg19a  40721  cdlemg27b  40734  cdlemg31d  40738  cdlemg33c  40746  cdlemg33e  40748  trlcone  40766  cdlemi  40858  tendotr  40868  cdlemk17  40896  cdlemk52  40992  cdleml1N  41014  dian0  41077  dia0  41090  dia2dimlem1  41102  dia2dimlem2  41103  dia2dimlem3  41104  dih0cnv  41321  dihmeetlem4preN  41344  dihmeetlem7N  41348  dihmeetlem17N  41361  dihlspsnat  41371  dihatexv  41376