Theorem hlatl 39316

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

Syntax hints:   → wi 4   ∈ wcel 2108  AtLatcal 39220  CvLatclc 39221  HLchlt 39306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-cvlat 39278  df-hlat 39307

This theorem is referenced by:  hllat  39319  hlomcmat  39321  intnatN  39364  cvratlem  39378  atcvrj0  39385  atcvrneN  39387  atcvrj1  39388  atcvrj2b  39389  atltcvr  39392  cvrat4  39400  2atjm  39402  atbtwn  39403  3dim2  39425  2dim  39427  1cvrjat  39432  ps-2  39435  ps-2b  39439  islln3  39467  llnnleat  39470  llnexatN  39478  2llnmat  39481  2atm  39484  2llnm3N  39526  2llnm4  39527  2llnmeqat  39528  dalem21  39651  dalem24  39654  dalem25  39655  dalem54  39683  dalem55  39684  dalem57  39686  pmapat  39720  pmapeq0  39723  isline4N  39734  2lnat  39741  2llnma1b  39743  cdlema2N  39749  cdlemblem  39750  pmapjat1  39810  llnexchb2lem  39825  pol1N  39867  pnonsingN  39890  pclfinclN  39907  lhpocnle  39973  lhpmat  39987  lhpmatb  39988  lhp2at0  39989  lhp2atnle  39990  lhp2at0nle  39992  lhpat3  40003  4atexlemcnd  40029  trlatn0  40129  ltrnnidn  40131  trlnidatb  40134  trlnle  40143  trlval3  40144  trlval4  40145  cdlemc5  40152  cdleme0e  40174  cdleme3  40194  cdleme7c  40202  cdleme7ga  40205  cdleme7  40206  cdleme11k  40225  cdleme15b  40232  cdleme16b  40236  cdleme16e  40239  cdleme16f  40240  cdlemednpq  40256  cdleme20zN  40258  cdleme20j  40275  cdleme22aa  40296  cdleme22cN  40299  cdleme22d  40300  cdlemf2  40519  cdlemb3  40563  cdlemg12e  40604  cdlemg17dALTN  40621  cdlemg19a  40640  cdlemg27b  40653  cdlemg31d  40657  cdlemg33c  40665  cdlemg33e  40667  trlcone  40685  cdlemi  40777  tendotr  40787  cdlemk17  40815  cdlemk52  40911  cdleml1N  40933  dian0  40996  dia0  41009  dia2dimlem1  41021  dia2dimlem2  41022  dia2dimlem3  41023  dih0cnv  41240  dihmeetlem4preN  41263  dihmeetlem7N  41267  dihmeetlem17N  41280  dihlspsnat  41290  dihatexv  41295