Theorem hlatl 37301

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

Syntax hints:   → wi 4   ∈ wcel 2108  AtLatcal 37205  CvLatclc 37206  HLchlt 37291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-cvlat 37263  df-hlat 37292

This theorem is referenced by:  hllat  37304  hlomcmat  37306  intnatN  37348  cvratlem  37362  atcvrj0  37369  atcvrneN  37371  atcvrj1  37372  atcvrj2b  37373  atltcvr  37376  cvrat4  37384  2atjm  37386  atbtwn  37387  3dim2  37409  2dim  37411  1cvrjat  37416  ps-2  37419  ps-2b  37423  islln3  37451  llnnleat  37454  llnexatN  37462  2llnmat  37465  2atm  37468  2llnm3N  37510  2llnm4  37511  2llnmeqat  37512  dalem21  37635  dalem24  37638  dalem25  37639  dalem54  37667  dalem55  37668  dalem57  37670  pmapat  37704  pmapeq0  37707  isline4N  37718  2lnat  37725  2llnma1b  37727  cdlema2N  37733  cdlemblem  37734  pmapjat1  37794  llnexchb2lem  37809  pol1N  37851  pnonsingN  37874  pclfinclN  37891  lhpocnle  37957  lhpmat  37971  lhpmatb  37972  lhp2at0  37973  lhp2atnle  37974  lhp2at0nle  37976  lhpat3  37987  4atexlemcnd  38013  trlatn0  38113  ltrnnidn  38115  trlnidatb  38118  trlnle  38127  trlval3  38128  trlval4  38129  cdlemc5  38136  cdleme0e  38158  cdleme3  38178  cdleme7c  38186  cdleme7ga  38189  cdleme7  38190  cdleme11k  38209  cdleme15b  38216  cdleme16b  38220  cdleme16e  38223  cdleme16f  38224  cdlemednpq  38240  cdleme20zN  38242  cdleme20j  38259  cdleme22aa  38280  cdleme22cN  38283  cdleme22d  38284  cdlemf2  38503  cdlemb3  38547  cdlemg12e  38588  cdlemg17dALTN  38605  cdlemg19a  38624  cdlemg27b  38637  cdlemg31d  38641  cdlemg33c  38649  cdlemg33e  38651  trlcone  38669  cdlemi  38761  tendotr  38771  cdlemk17  38799  cdlemk52  38895  cdleml1N  38917  dian0  38980  dia0  38993  dia2dimlem1  39005  dia2dimlem2  39006  dia2dimlem3  39007  dih0cnv  39224  dihmeetlem4preN  39247  dihmeetlem7N  39251  dihmeetlem17N  39264  dihlspsnat  39274  dihatexv  39279