Theorem hlatl 36656

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

Syntax hints:   → wi 4   ∈ wcel 2111  AtLatcal 36560  CvLatclc 36561  HLchlt 36646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-cvlat 36618  df-hlat 36647

This theorem is referenced by:  hllat  36659  hlomcmat  36661  intnatN  36703  cvratlem  36717  atcvrj0  36724  atcvrneN  36726  atcvrj1  36727  atcvrj2b  36728  atltcvr  36731  cvrat4  36739  2atjm  36741  atbtwn  36742  3dim2  36764  2dim  36766  1cvrjat  36771  ps-2  36774  ps-2b  36778  islln3  36806  llnnleat  36809  llnexatN  36817  2llnmat  36820  2atm  36823  2llnm3N  36865  2llnm4  36866  2llnmeqat  36867  dalem21  36990  dalem24  36993  dalem25  36994  dalem54  37022  dalem55  37023  dalem57  37025  pmapat  37059  pmapeq0  37062  isline4N  37073  2lnat  37080  2llnma1b  37082  cdlema2N  37088  cdlemblem  37089  pmapjat1  37149  llnexchb2lem  37164  pol1N  37206  pnonsingN  37229  pclfinclN  37246  lhpocnle  37312  lhpmat  37326  lhpmatb  37327  lhp2at0  37328  lhp2atnle  37329  lhp2at0nle  37331  lhpat3  37342  4atexlemcnd  37368  trlatn0  37468  ltrnnidn  37470  trlnidatb  37473  trlnle  37482  trlval3  37483  trlval4  37484  cdlemc5  37491  cdleme0e  37513  cdleme3  37533  cdleme7c  37541  cdleme7ga  37544  cdleme7  37545  cdleme11k  37564  cdleme15b  37571  cdleme16b  37575  cdleme16e  37578  cdleme16f  37579  cdlemednpq  37595  cdleme20zN  37597  cdleme20j  37614  cdleme22aa  37635  cdleme22cN  37638  cdleme22d  37639  cdlemf2  37858  cdlemb3  37902  cdlemg12e  37943  cdlemg17dALTN  37960  cdlemg19a  37979  cdlemg27b  37992  cdlemg31d  37996  cdlemg33c  38004  cdlemg33e  38006  trlcone  38024  cdlemi  38116  tendotr  38126  cdlemk17  38154  cdlemk52  38250  cdleml1N  38272  dian0  38335  dia0  38348  dia2dimlem1  38360  dia2dimlem2  38361  dia2dimlem3  38362  dih0cnv  38579  dihmeetlem4preN  38602  dihmeetlem7N  38606  dihmeetlem17N  38619  dihlspsnat  38629  dihatexv  38634