Theorem hlatl 40511

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  AtLatcal 40415  CvLatclc 40416  HLchlt 40501

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6547  df-ov 7424  df-cvlat 40473  df-hlat 40502

This theorem is used by:  hllat  40514  hlomcmat  40516  intnatN  40558  cvratlem  40572  atcvrj0  40579  atcvrneN  40581  atcvrj1  40582  atcvrj2b  40583  atltcvr  40586  cvrat4  40594  2atjm  40596  atbtwn  40597  3dim2  40619  2dim  40621  1cvrjat  40626  ps-2  40629  ps-2b  40633  islln3  40661  llnnleat  40664  llnexatN  40672  2llnmat  40675  2atm  40678  2llnm3N  40720  2llnm4  40721  2llnmeqat  40722  dalem21  40845  dalem24  40848  dalem25  40849  dalem54  40877  dalem55  40878  dalem57  40880  pmapat  40914  pmapeq0  40917  isline4N  40928  2lnat  40935  2llnma1b  40937  cdlema2N  40943  cdlemblem  40944  pmapjat1  41004  llnexchb2lem  41019  pol1N  41061  pnonsingN  41084  pclfinclN  41101  lhpocnle  41167  lhpmat  41181  lhpmatb  41182  lhp2at0  41183  lhp2atnle  41184  lhp2at0nle  41186  lhpat3  41197  4atexlemcnd  41223  trlatn0  41323  ltrnnidn  41325  trlnidatb  41328  trlnle  41337  trlval3  41338  trlval4  41339  cdlemc5  41346  cdleme0e  41368  cdleme3  41388  cdleme7c  41396  cdleme7ga  41399  cdleme7  41400  cdleme11k  41419  cdleme15b  41426  cdleme16b  41430  cdleme16e  41433  cdleme16f  41434  cdlemednpq  41450  cdleme20zN  41452  cdleme20j  41469  cdleme22aa  41490  cdleme22cN  41493  cdleme22d  41494  cdlemf2  41713  cdlemb3  41757  cdlemg12e  41798  cdlemg17dALTN  41815  cdlemg19a  41834  cdlemg27b  41847  cdlemg31d  41851  cdlemg33c  41859  cdlemg33e  41861  trlcone  41879  cdlemi  41971  tendotr  41981  cdlemk17  42009  cdlemk52  42105  cdleml1N  42127  dian0  42190  dia0  42203  dia2dimlem1  42215  dia2dimlem2  42216  dia2dimlem3  42217  dih0cnv  42434  dihmeetlem4preN  42457  dihmeetlem7N  42461  dihmeetlem17N  42474  dihlspsnat  42484  dihatexv  42489