Theorem hlatl 38535

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

Syntax hints:   → wi 4   ∈ wcel 2104  AtLatcal 38439  CvLatclc 38440  HLchlt 38525

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7416  df-cvlat 38497  df-hlat 38526

This theorem is referenced by:  hllat  38538  hlomcmat  38540  intnatN  38583  cvratlem  38597  atcvrj0  38604  atcvrneN  38606  atcvrj1  38607  atcvrj2b  38608  atltcvr  38611  cvrat4  38619  2atjm  38621  atbtwn  38622  3dim2  38644  2dim  38646  1cvrjat  38651  ps-2  38654  ps-2b  38658  islln3  38686  llnnleat  38689  llnexatN  38697  2llnmat  38700  2atm  38703  2llnm3N  38745  2llnm4  38746  2llnmeqat  38747  dalem21  38870  dalem24  38873  dalem25  38874  dalem54  38902  dalem55  38903  dalem57  38905  pmapat  38939  pmapeq0  38942  isline4N  38953  2lnat  38960  2llnma1b  38962  cdlema2N  38968  cdlemblem  38969  pmapjat1  39029  llnexchb2lem  39044  pol1N  39086  pnonsingN  39109  pclfinclN  39126  lhpocnle  39192  lhpmat  39206  lhpmatb  39207  lhp2at0  39208  lhp2atnle  39209  lhp2at0nle  39211  lhpat3  39222  4atexlemcnd  39248  trlatn0  39348  ltrnnidn  39350  trlnidatb  39353  trlnle  39362  trlval3  39363  trlval4  39364  cdlemc5  39371  cdleme0e  39393  cdleme3  39413  cdleme7c  39421  cdleme7ga  39424  cdleme7  39425  cdleme11k  39444  cdleme15b  39451  cdleme16b  39455  cdleme16e  39458  cdleme16f  39459  cdlemednpq  39475  cdleme20zN  39477  cdleme20j  39494  cdleme22aa  39515  cdleme22cN  39518  cdleme22d  39519  cdlemf2  39738  cdlemb3  39782  cdlemg12e  39823  cdlemg17dALTN  39840  cdlemg19a  39859  cdlemg27b  39872  cdlemg31d  39876  cdlemg33c  39884  cdlemg33e  39886  trlcone  39904  cdlemi  39996  tendotr  40006  cdlemk17  40034  cdlemk52  40130  cdleml1N  40152  dian0  40215  dia0  40228  dia2dimlem1  40240  dia2dimlem2  40241  dia2dimlem3  40242  dih0cnv  40459  dihmeetlem4preN  40482  dihmeetlem7N  40486  dihmeetlem17N  40499  dihlspsnat  40509  dihatexv  40514