Theorem hlatl 39360

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

Syntax hints:   → wi 4   ∈ wcel 2109  AtLatcal 39264  CvLatclc 39265  HLchlt 39350

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-cvlat 39322  df-hlat 39351

This theorem is referenced by:  hllat  39363  hlomcmat  39365  intnatN  39408  cvratlem  39422  atcvrj0  39429  atcvrneN  39431  atcvrj1  39432  atcvrj2b  39433  atltcvr  39436  cvrat4  39444  2atjm  39446  atbtwn  39447  3dim2  39469  2dim  39471  1cvrjat  39476  ps-2  39479  ps-2b  39483  islln3  39511  llnnleat  39514  llnexatN  39522  2llnmat  39525  2atm  39528  2llnm3N  39570  2llnm4  39571  2llnmeqat  39572  dalem21  39695  dalem24  39698  dalem25  39699  dalem54  39727  dalem55  39728  dalem57  39730  pmapat  39764  pmapeq0  39767  isline4N  39778  2lnat  39785  2llnma1b  39787  cdlema2N  39793  cdlemblem  39794  pmapjat1  39854  llnexchb2lem  39869  pol1N  39911  pnonsingN  39934  pclfinclN  39951  lhpocnle  40017  lhpmat  40031  lhpmatb  40032  lhp2at0  40033  lhp2atnle  40034  lhp2at0nle  40036  lhpat3  40047  4atexlemcnd  40073  trlatn0  40173  ltrnnidn  40175  trlnidatb  40178  trlnle  40187  trlval3  40188  trlval4  40189  cdlemc5  40196  cdleme0e  40218  cdleme3  40238  cdleme7c  40246  cdleme7ga  40249  cdleme7  40250  cdleme11k  40269  cdleme15b  40276  cdleme16b  40280  cdleme16e  40283  cdleme16f  40284  cdlemednpq  40300  cdleme20zN  40302  cdleme20j  40319  cdleme22aa  40340  cdleme22cN  40343  cdleme22d  40344  cdlemf2  40563  cdlemb3  40607  cdlemg12e  40648  cdlemg17dALTN  40665  cdlemg19a  40684  cdlemg27b  40697  cdlemg31d  40701  cdlemg33c  40709  cdlemg33e  40711  trlcone  40729  cdlemi  40821  tendotr  40831  cdlemk17  40859  cdlemk52  40955  cdleml1N  40977  dian0  41040  dia0  41053  dia2dimlem1  41065  dia2dimlem2  41066  dia2dimlem3  41067  dih0cnv  41284  dihmeetlem4preN  41307  dihmeetlem7N  41311  dihmeetlem17N  41324  dihlspsnat  41334  dihatexv  41339