Theorem hlatl 37586

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

Syntax hints:   → wi 4   ∈ wcel 2105  AtLatcal 37490  CvLatclc 37491  HLchlt 37576

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4849  df-br 5086  df-iota 6415  df-fv 6471  df-ov 7316  df-cvlat 37548  df-hlat 37577

This theorem is referenced by:  hllat  37589  hlomcmat  37591  intnatN  37633  cvratlem  37647  atcvrj0  37654  atcvrneN  37656  atcvrj1  37657  atcvrj2b  37658  atltcvr  37661  cvrat4  37669  2atjm  37671  atbtwn  37672  3dim2  37694  2dim  37696  1cvrjat  37701  ps-2  37704  ps-2b  37708  islln3  37736  llnnleat  37739  llnexatN  37747  2llnmat  37750  2atm  37753  2llnm3N  37795  2llnm4  37796  2llnmeqat  37797  dalem21  37920  dalem24  37923  dalem25  37924  dalem54  37952  dalem55  37953  dalem57  37955  pmapat  37989  pmapeq0  37992  isline4N  38003  2lnat  38010  2llnma1b  38012  cdlema2N  38018  cdlemblem  38019  pmapjat1  38079  llnexchb2lem  38094  pol1N  38136  pnonsingN  38159  pclfinclN  38176  lhpocnle  38242  lhpmat  38256  lhpmatb  38257  lhp2at0  38258  lhp2atnle  38259  lhp2at0nle  38261  lhpat3  38272  4atexlemcnd  38298  trlatn0  38398  ltrnnidn  38400  trlnidatb  38403  trlnle  38412  trlval3  38413  trlval4  38414  cdlemc5  38421  cdleme0e  38443  cdleme3  38463  cdleme7c  38471  cdleme7ga  38474  cdleme7  38475  cdleme11k  38494  cdleme15b  38501  cdleme16b  38505  cdleme16e  38508  cdleme16f  38509  cdlemednpq  38525  cdleme20zN  38527  cdleme20j  38544  cdleme22aa  38565  cdleme22cN  38568  cdleme22d  38569  cdlemf2  38788  cdlemb3  38832  cdlemg12e  38873  cdlemg17dALTN  38890  cdlemg19a  38909  cdlemg27b  38922  cdlemg31d  38926  cdlemg33c  38934  cdlemg33e  38936  trlcone  38954  cdlemi  39046  tendotr  39056  cdlemk17  39084  cdlemk52  39180  cdleml1N  39202  dian0  39265  dia0  39278  dia2dimlem1  39290  dia2dimlem2  39291  dia2dimlem3  39292  dih0cnv  39509  dihmeetlem4preN  39532  dihmeetlem7N  39536  dihmeetlem17N  39549  dihlspsnat  39559  dihatexv  39564