Theorem hlatl 39338

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

Syntax hints:   → wi 4   ∈ wcel 2109  AtLatcal 39242  CvLatclc 39243  HLchlt 39328

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-cvlat 39300  df-hlat 39329

This theorem is referenced by:  hllat  39341  hlomcmat  39343  intnatN  39386  cvratlem  39400  atcvrj0  39407  atcvrneN  39409  atcvrj1  39410  atcvrj2b  39411  atltcvr  39414  cvrat4  39422  2atjm  39424  atbtwn  39425  3dim2  39447  2dim  39449  1cvrjat  39454  ps-2  39457  ps-2b  39461  islln3  39489  llnnleat  39492  llnexatN  39500  2llnmat  39503  2atm  39506  2llnm3N  39548  2llnm4  39549  2llnmeqat  39550  dalem21  39673  dalem24  39676  dalem25  39677  dalem54  39705  dalem55  39706  dalem57  39708  pmapat  39742  pmapeq0  39745  isline4N  39756  2lnat  39763  2llnma1b  39765  cdlema2N  39771  cdlemblem  39772  pmapjat1  39832  llnexchb2lem  39847  pol1N  39889  pnonsingN  39912  pclfinclN  39929  lhpocnle  39995  lhpmat  40009  lhpmatb  40010  lhp2at0  40011  lhp2atnle  40012  lhp2at0nle  40014  lhpat3  40025  4atexlemcnd  40051  trlatn0  40151  ltrnnidn  40153  trlnidatb  40156  trlnle  40165  trlval3  40166  trlval4  40167  cdlemc5  40174  cdleme0e  40196  cdleme3  40216  cdleme7c  40224  cdleme7ga  40227  cdleme7  40228  cdleme11k  40247  cdleme15b  40254  cdleme16b  40258  cdleme16e  40261  cdleme16f  40262  cdlemednpq  40278  cdleme20zN  40280  cdleme20j  40297  cdleme22aa  40318  cdleme22cN  40321  cdleme22d  40322  cdlemf2  40541  cdlemb3  40585  cdlemg12e  40626  cdlemg17dALTN  40643  cdlemg19a  40662  cdlemg27b  40675  cdlemg31d  40679  cdlemg33c  40687  cdlemg33e  40689  trlcone  40707  cdlemi  40799  tendotr  40809  cdlemk17  40837  cdlemk52  40933  cdleml1N  40955  dian0  41018  dia0  41031  dia2dimlem1  41043  dia2dimlem2  41044  dia2dimlem3  41045  dih0cnv  41262  dihmeetlem4preN  41285  dihmeetlem7N  41289  dihmeetlem17N  41302  dihlspsnat  41312  dihatexv  41317