Theorem hlatl 39479

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

Syntax hints:   → wi 4   ∈ wcel 2113  AtLatcal 39383  CvLatclc 39384  HLchlt 39469

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 2115  ax-9 2123  ax-ext 2705

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 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355  df-cvlat 39441  df-hlat 39470

This theorem is referenced by:  hllat  39482  hlomcmat  39484  intnatN  39526  cvratlem  39540  atcvrj0  39547  atcvrneN  39549  atcvrj1  39550  atcvrj2b  39551  atltcvr  39554  cvrat4  39562  2atjm  39564  atbtwn  39565  3dim2  39587  2dim  39589  1cvrjat  39594  ps-2  39597  ps-2b  39601  islln3  39629  llnnleat  39632  llnexatN  39640  2llnmat  39643  2atm  39646  2llnm3N  39688  2llnm4  39689  2llnmeqat  39690  dalem21  39813  dalem24  39816  dalem25  39817  dalem54  39845  dalem55  39846  dalem57  39848  pmapat  39882  pmapeq0  39885  isline4N  39896  2lnat  39903  2llnma1b  39905  cdlema2N  39911  cdlemblem  39912  pmapjat1  39972  llnexchb2lem  39987  pol1N  40029  pnonsingN  40052  pclfinclN  40069  lhpocnle  40135  lhpmat  40149  lhpmatb  40150  lhp2at0  40151  lhp2atnle  40152  lhp2at0nle  40154  lhpat3  40165  4atexlemcnd  40191  trlatn0  40291  ltrnnidn  40293  trlnidatb  40296  trlnle  40305  trlval3  40306  trlval4  40307  cdlemc5  40314  cdleme0e  40336  cdleme3  40356  cdleme7c  40364  cdleme7ga  40367  cdleme7  40368  cdleme11k  40387  cdleme15b  40394  cdleme16b  40398  cdleme16e  40401  cdleme16f  40402  cdlemednpq  40418  cdleme20zN  40420  cdleme20j  40437  cdleme22aa  40458  cdleme22cN  40461  cdleme22d  40462  cdlemf2  40681  cdlemb3  40725  cdlemg12e  40766  cdlemg17dALTN  40783  cdlemg19a  40802  cdlemg27b  40815  cdlemg31d  40819  cdlemg33c  40827  cdlemg33e  40829  trlcone  40847  cdlemi  40939  tendotr  40949  cdlemk17  40977  cdlemk52  41073  cdleml1N  41095  dian0  41158  dia0  41171  dia2dimlem1  41183  dia2dimlem2  41184  dia2dimlem3  41185  dih0cnv  41402  dihmeetlem4preN  41425  dihmeetlem7N  41429  dihmeetlem17N  41442  dihlspsnat  41452  dihatexv  41457