Theorem hlatl 39730

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

Syntax hints:   → wi 4   ∈ wcel 2114  AtLatcal 39634  CvLatclc 39635  HLchlt 39720

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-cvlat 39692  df-hlat 39721

This theorem is referenced by:  hllat  39733  hlomcmat  39735  intnatN  39777  cvratlem  39791  atcvrj0  39798  atcvrneN  39800  atcvrj1  39801  atcvrj2b  39802  atltcvr  39805  cvrat4  39813  2atjm  39815  atbtwn  39816  3dim2  39838  2dim  39840  1cvrjat  39845  ps-2  39848  ps-2b  39852  islln3  39880  llnnleat  39883  llnexatN  39891  2llnmat  39894  2atm  39897  2llnm3N  39939  2llnm4  39940  2llnmeqat  39941  dalem21  40064  dalem24  40067  dalem25  40068  dalem54  40096  dalem55  40097  dalem57  40099  pmapat  40133  pmapeq0  40136  isline4N  40147  2lnat  40154  2llnma1b  40156  cdlema2N  40162  cdlemblem  40163  pmapjat1  40223  llnexchb2lem  40238  pol1N  40280  pnonsingN  40303  pclfinclN  40320  lhpocnle  40386  lhpmat  40400  lhpmatb  40401  lhp2at0  40402  lhp2atnle  40403  lhp2at0nle  40405  lhpat3  40416  4atexlemcnd  40442  trlatn0  40542  ltrnnidn  40544  trlnidatb  40547  trlnle  40556  trlval3  40557  trlval4  40558  cdlemc5  40565  cdleme0e  40587  cdleme3  40607  cdleme7c  40615  cdleme7ga  40618  cdleme7  40619  cdleme11k  40638  cdleme15b  40645  cdleme16b  40649  cdleme16e  40652  cdleme16f  40653  cdlemednpq  40669  cdleme20zN  40671  cdleme20j  40688  cdleme22aa  40709  cdleme22cN  40712  cdleme22d  40713  cdlemf2  40932  cdlemb3  40976  cdlemg12e  41017  cdlemg17dALTN  41034  cdlemg19a  41053  cdlemg27b  41066  cdlemg31d  41070  cdlemg33c  41078  cdlemg33e  41080  trlcone  41098  cdlemi  41190  tendotr  41200  cdlemk17  41228  cdlemk52  41324  cdleml1N  41346  dian0  41409  dia0  41422  dia2dimlem1  41434  dia2dimlem2  41435  dia2dimlem3  41436  dih0cnv  41653  dihmeetlem4preN  41676  dihmeetlem7N  41680  dihmeetlem17N  41693  dihlspsnat  41703  dihatexv  41708