Theorem hlatl 35169

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

Syntax hints:   → wi 4   ∈ wcel 2140  AtLatcal 35073  CvLatclc 35074  HLchlt 35159

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3343  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-br 4806  df-iota 6013  df-fv 6058  df-ov 6818  df-cvlat 35131  df-hlat 35160

This theorem is referenced by:  hllat  35172  hlomcmat  35173  intnatN  35215  cvratlem  35229  atcvrj0  35236  atcvrneN  35238  atcvrj1  35239  atcvrj2b  35240  atltcvr  35243  cvrat4  35251  2atjm  35253  atbtwn  35254  3dim2  35276  2dim  35278  1cvrjat  35283  ps-2  35286  ps-2b  35290  islln3  35318  llnnleat  35321  llnexatN  35329  2llnmat  35332  2atm  35335  2llnm3N  35377  2llnm4  35378  2llnmeqat  35379  dalem21  35502  dalem24  35505  dalem25  35506  dalem54  35534  dalem55  35535  dalem57  35537  pmapat  35571  pmapeq0  35574  isline4N  35585  2lnat  35592  2llnma1b  35594  cdlema2N  35600  cdlemblem  35601  pmapjat1  35661  llnexchb2lem  35676  pol1N  35718  pnonsingN  35741  pclfinclN  35758  lhpocnle  35824  lhpmat  35838  lhpmatb  35839  lhp2at0  35840  lhp2atnle  35841  lhp2at0nle  35843  lhpat3  35854  4atexlemcnd  35880  ltrnmwOLD  35960  trlatn0  35981  ltrnnidn  35983  trlnidatb  35986  trlnle  35995  trlval3  35996  trlval4  35997  cdlemc5  36004  cdleme0e  36026  cdleme3  36046  cdleme7c  36054  cdleme7ga  36057  cdleme7  36058  cdleme11k  36077  cdleme15b  36084  cdleme16b  36088  cdleme16e  36091  cdleme16f  36092  cdlemednpq  36108  cdleme20zN  36110  cdleme20j  36127  cdleme22aa  36148  cdleme22cN  36151  cdleme22d  36152  cdlemf2  36371  cdlemb3  36415  cdlemg12e  36456  cdlemg17dALTN  36473  cdlemg19a  36492  cdlemg27b  36505  cdlemg31d  36509  cdlemg33c  36517  cdlemg33e  36519  trlcone  36537  cdlemi  36629  tendotr  36639  cdlemk17  36667  cdlemk52  36763  cdleml1N  36785  dian0  36849  dia0  36862  dia2dimlem1  36874  dia2dimlem2  36875  dia2dimlem3  36876  dih0cnv  37093  dihmeetlem4preN  37116  dihmeetlem7N  37120  dihmeetlem17N  37133  dihlspsnat  37143  dihatexv  37148