Theorem hlatl 40241

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  AtLatcal 40145  CvLatclc 40146  HLchlt 40231

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420  df-cvlat 40203  df-hlat 40232

This theorem is used by:  hllat  40244  hlomcmat  40246  intnatN  40288  cvratlem  40302  atcvrj0  40309  atcvrneN  40311  atcvrj1  40312  atcvrj2b  40313  atltcvr  40316  cvrat4  40324  2atjm  40326  atbtwn  40327  3dim2  40349  2dim  40351  1cvrjat  40356  ps-2  40359  ps-2b  40363  islln3  40391  llnnleat  40394  llnexatN  40402  2llnmat  40405  2atm  40408  2llnm3N  40450  2llnm4  40451  2llnmeqat  40452  dalem21  40575  dalem24  40578  dalem25  40579  dalem54  40607  dalem55  40608  dalem57  40610  pmapat  40644  pmapeq0  40647  isline4N  40658  2lnat  40665  2llnma1b  40667  cdlema2N  40673  cdlemblem  40674  pmapjat1  40734  llnexchb2lem  40749  pol1N  40791  pnonsingN  40814  pclfinclN  40831  lhpocnle  40897  lhpmat  40911  lhpmatb  40912  lhp2at0  40913  lhp2atnle  40914  lhp2at0nle  40916  lhpat3  40927  4atexlemcnd  40953  trlatn0  41053  ltrnnidn  41055  trlnidatb  41058  trlnle  41067  trlval3  41068  trlval4  41069  cdlemc5  41076  cdleme0e  41098  cdleme3  41118  cdleme7c  41126  cdleme7ga  41129  cdleme7  41130  cdleme11k  41149  cdleme15b  41156  cdleme16b  41160  cdleme16e  41163  cdleme16f  41164  cdlemednpq  41180  cdleme20zN  41182  cdleme20j  41199  cdleme22aa  41220  cdleme22cN  41223  cdleme22d  41224  cdlemf2  41443  cdlemb3  41487  cdlemg12e  41528  cdlemg17dALTN  41545  cdlemg19a  41564  cdlemg27b  41577  cdlemg31d  41581  cdlemg33c  41589  cdlemg33e  41591  trlcone  41609  cdlemi  41701  tendotr  41711  cdlemk17  41739  cdlemk52  41835  cdleml1N  41857  dian0  41920  dia0  41933  dia2dimlem1  41945  dia2dimlem2  41946  dia2dimlem3  41947  dih0cnv  42164  dihmeetlem4preN  42187  dihmeetlem7N  42191  dihmeetlem17N  42204  dihlspsnat  42214  dihatexv  42219