Theorem hlatl 40385

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  AtLatcal 40289  CvLatclc 40290  HLchlt 40375

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-ov 7415  df-cvlat 40347  df-hlat 40376

This theorem is used by:  hllat  40388  hlomcmat  40390  intnatN  40432  cvratlem  40446  atcvrj0  40453  atcvrneN  40455  atcvrj1  40456  atcvrj2b  40457  atltcvr  40460  cvrat4  40468  2atjm  40470  atbtwn  40471  3dim2  40493  2dim  40495  1cvrjat  40500  ps-2  40503  ps-2b  40507  islln3  40535  llnnleat  40538  llnexatN  40546  2llnmat  40549  2atm  40552  2llnm3N  40594  2llnm4  40595  2llnmeqat  40596  dalem21  40719  dalem24  40722  dalem25  40723  dalem54  40751  dalem55  40752  dalem57  40754  pmapat  40788  pmapeq0  40791  isline4N  40802  2lnat  40809  2llnma1b  40811  cdlema2N  40817  cdlemblem  40818  pmapjat1  40878  llnexchb2lem  40893  pol1N  40935  pnonsingN  40958  pclfinclN  40975  lhpocnle  41041  lhpmat  41055  lhpmatb  41056  lhp2at0  41057  lhp2atnle  41058  lhp2at0nle  41060  lhpat3  41071  4atexlemcnd  41097  trlatn0  41197  ltrnnidn  41199  trlnidatb  41202  trlnle  41211  trlval3  41212  trlval4  41213  cdlemc5  41220  cdleme0e  41242  cdleme3  41262  cdleme7c  41270  cdleme7ga  41273  cdleme7  41274  cdleme11k  41293  cdleme15b  41300  cdleme16b  41304  cdleme16e  41307  cdleme16f  41308  cdlemednpq  41324  cdleme20zN  41326  cdleme20j  41343  cdleme22aa  41364  cdleme22cN  41367  cdleme22d  41368  cdlemf2  41587  cdlemb3  41631  cdlemg12e  41672  cdlemg17dALTN  41689  cdlemg19a  41708  cdlemg27b  41721  cdlemg31d  41725  cdlemg33c  41733  cdlemg33e  41735  trlcone  41753  cdlemi  41845  tendotr  41855  cdlemk17  41883  cdlemk52  41979  cdleml1N  42001  dian0  42064  dia0  42077  dia2dimlem1  42089  dia2dimlem2  42090  dia2dimlem3  42091  dih0cnv  42308  dihmeetlem4preN  42331  dihmeetlem7N  42335  dihmeetlem17N  42348  dihlspsnat  42358  dihatexv  42363