Theorem hlatl 39948

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

Syntax hints:   → wi 4   ∈ wcel 2141  AtLatcal 39852  CvLatclc 39853  HLchlt 39938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-ov 7395  df-cvlat 39910  df-hlat 39939

This theorem is referenced by:  hllat  39951  hlomcmat  39953  intnatN  39995  cvratlem  40009  atcvrj0  40016  atcvrneN  40018  atcvrj1  40019  atcvrj2b  40020  atltcvr  40023  cvrat4  40031  2atjm  40033  atbtwn  40034  3dim2  40056  2dim  40058  1cvrjat  40063  ps-2  40066  ps-2b  40070  islln3  40098  llnnleat  40101  llnexatN  40109  2llnmat  40112  2atm  40115  2llnm3N  40157  2llnm4  40158  2llnmeqat  40159  dalem21  40282  dalem24  40285  dalem25  40286  dalem54  40314  dalem55  40315  dalem57  40317  pmapat  40351  pmapeq0  40354  isline4N  40365  2lnat  40372  2llnma1b  40374  cdlema2N  40380  cdlemblem  40381  pmapjat1  40441  llnexchb2lem  40456  pol1N  40498  pnonsingN  40521  pclfinclN  40538  lhpocnle  40604  lhpmat  40618  lhpmatb  40619  lhp2at0  40620  lhp2atnle  40621  lhp2at0nle  40623  lhpat3  40634  4atexlemcnd  40660  trlatn0  40760  ltrnnidn  40762  trlnidatb  40765  trlnle  40774  trlval3  40775  trlval4  40776  cdlemc5  40783  cdleme0e  40805  cdleme3  40825  cdleme7c  40833  cdleme7ga  40836  cdleme7  40837  cdleme11k  40856  cdleme15b  40863  cdleme16b  40867  cdleme16e  40870  cdleme16f  40871  cdlemednpq  40887  cdleme20zN  40889  cdleme20j  40906  cdleme22aa  40927  cdleme22cN  40930  cdleme22d  40931  cdlemf2  41150  cdlemb3  41194  cdlemg12e  41235  cdlemg17dALTN  41252  cdlemg19a  41271  cdlemg27b  41284  cdlemg31d  41288  cdlemg33c  41296  cdlemg33e  41298  trlcone  41316  cdlemi  41408  tendotr  41418  cdlemk17  41446  cdlemk52  41542  cdleml1N  41564  dian0  41627  dia0  41640  dia2dimlem1  41652  dia2dimlem2  41653  dia2dimlem3  41654  dih0cnv  41871  dihmeetlem4preN  41894  dihmeetlem7N  41898  dihmeetlem17N  41911  dihlspsnat  41921  dihatexv  41926