Theorem hlatl 39361

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

Syntax hints:   → wi 4   ∈ wcel 2108  AtLatcal 39265  CvLatclc 39266  HLchlt 39351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-cvlat 39323  df-hlat 39352

This theorem is referenced by:  hllat  39364  hlomcmat  39366  intnatN  39409  cvratlem  39423  atcvrj0  39430  atcvrneN  39432  atcvrj1  39433  atcvrj2b  39434  atltcvr  39437  cvrat4  39445  2atjm  39447  atbtwn  39448  3dim2  39470  2dim  39472  1cvrjat  39477  ps-2  39480  ps-2b  39484  islln3  39512  llnnleat  39515  llnexatN  39523  2llnmat  39526  2atm  39529  2llnm3N  39571  2llnm4  39572  2llnmeqat  39573  dalem21  39696  dalem24  39699  dalem25  39700  dalem54  39728  dalem55  39729  dalem57  39731  pmapat  39765  pmapeq0  39768  isline4N  39779  2lnat  39786  2llnma1b  39788  cdlema2N  39794  cdlemblem  39795  pmapjat1  39855  llnexchb2lem  39870  pol1N  39912  pnonsingN  39935  pclfinclN  39952  lhpocnle  40018  lhpmat  40032  lhpmatb  40033  lhp2at0  40034  lhp2atnle  40035  lhp2at0nle  40037  lhpat3  40048  4atexlemcnd  40074  trlatn0  40174  ltrnnidn  40176  trlnidatb  40179  trlnle  40188  trlval3  40189  trlval4  40190  cdlemc5  40197  cdleme0e  40219  cdleme3  40239  cdleme7c  40247  cdleme7ga  40250  cdleme7  40251  cdleme11k  40270  cdleme15b  40277  cdleme16b  40281  cdleme16e  40284  cdleme16f  40285  cdlemednpq  40301  cdleme20zN  40303  cdleme20j  40320  cdleme22aa  40341  cdleme22cN  40344  cdleme22d  40345  cdlemf2  40564  cdlemb3  40608  cdlemg12e  40649  cdlemg17dALTN  40666  cdlemg19a  40685  cdlemg27b  40698  cdlemg31d  40702  cdlemg33c  40710  cdlemg33e  40712  trlcone  40730  cdlemi  40822  tendotr  40832  cdlemk17  40860  cdlemk52  40956  cdleml1N  40978  dian0  41041  dia0  41054  dia2dimlem1  41066  dia2dimlem2  41067  dia2dimlem3  41068  dih0cnv  41285  dihmeetlem4preN  41308  dihmeetlem7N  41312  dihmeetlem17N  41325  dihlspsnat  41335  dihatexv  41340