Theorem hlatl 39996

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 39995	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat)
2		cvlatl 39961	. 2 ⊢ (𝐾 ∈ CvLat → 𝐾 ∈ AtLat)
3	1, 2	syl 18	1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)

Syntax hints:   → wi 4   ∈ wcel 2145  AtLatcal 39900  CvLatclc 39901  HLchlt 39986

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-ov 7403  df-cvlat 39958  df-hlat 39987

This theorem is referenced by:  hllat  39999  hlomcmat  40001  intnatN  40043  cvratlem  40057  atcvrj0  40064  atcvrneN  40066  atcvrj1  40067  atcvrj2b  40068  atltcvr  40071  cvrat4  40079  2atjm  40081  atbtwn  40082  3dim2  40104  2dim  40106  1cvrjat  40111  ps-2  40114  ps-2b  40118  islln3  40146  llnnleat  40149  llnexatN  40157  2llnmat  40160  2atm  40163  2llnm3N  40205  2llnm4  40206  2llnmeqat  40207  dalem21  40330  dalem24  40333  dalem25  40334  dalem54  40362  dalem55  40363  dalem57  40365  pmapat  40399  pmapeq0  40402  isline4N  40413  2lnat  40420  2llnma1b  40422  cdlema2N  40428  cdlemblem  40429  pmapjat1  40489  llnexchb2lem  40504  pol1N  40546  pnonsingN  40569  pclfinclN  40586  lhpocnle  40652  lhpmat  40666  lhpmatb  40667  lhp2at0  40668  lhp2atnle  40669  lhp2at0nle  40671  lhpat3  40682  4atexlemcnd  40708  trlatn0  40808  ltrnnidn  40810  trlnidatb  40813  trlnle  40822  trlval3  40823  trlval4  40824  cdlemc5  40831  cdleme0e  40853  cdleme3  40873  cdleme7c  40881  cdleme7ga  40884  cdleme7  40885  cdleme11k  40904  cdleme15b  40911  cdleme16b  40915  cdleme16e  40918  cdleme16f  40919  cdlemednpq  40935  cdleme20zN  40937  cdleme20j  40954  cdleme22aa  40975  cdleme22cN  40978  cdleme22d  40979  cdlemf2  41198  cdlemb3  41242  cdlemg12e  41283  cdlemg17dALTN  41300  cdlemg19a  41319  cdlemg27b  41332  cdlemg31d  41336  cdlemg33c  41344  cdlemg33e  41346  trlcone  41364  cdlemi  41456  tendotr  41466  cdlemk17  41494  cdlemk52  41590  cdleml1N  41612  dian0  41675  dia0  41688  dia2dimlem1  41700  dia2dimlem2  41701  dia2dimlem3  41702  dih0cnv  41919  dihmeetlem4preN  41942  dihmeetlem7N  41946  dihmeetlem17N  41959  dihlspsnat  41969  dihatexv  41974