Theorem hlatl 38959

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

Syntax hints:   → wi 4   ∈ wcel 2098  AtLatcal 38863  CvLatclc 38864  HLchlt 38949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-iota 6501  df-fv 6557  df-ov 7422  df-cvlat 38921  df-hlat 38950

This theorem is referenced by:  hllat  38962  hlomcmat  38964  intnatN  39007  cvratlem  39021  atcvrj0  39028  atcvrneN  39030  atcvrj1  39031  atcvrj2b  39032  atltcvr  39035  cvrat4  39043  2atjm  39045  atbtwn  39046  3dim2  39068  2dim  39070  1cvrjat  39075  ps-2  39078  ps-2b  39082  islln3  39110  llnnleat  39113  llnexatN  39121  2llnmat  39124  2atm  39127  2llnm3N  39169  2llnm4  39170  2llnmeqat  39171  dalem21  39294  dalem24  39297  dalem25  39298  dalem54  39326  dalem55  39327  dalem57  39329  pmapat  39363  pmapeq0  39366  isline4N  39377  2lnat  39384  2llnma1b  39386  cdlema2N  39392  cdlemblem  39393  pmapjat1  39453  llnexchb2lem  39468  pol1N  39510  pnonsingN  39533  pclfinclN  39550  lhpocnle  39616  lhpmat  39630  lhpmatb  39631  lhp2at0  39632  lhp2atnle  39633  lhp2at0nle  39635  lhpat3  39646  4atexlemcnd  39672  trlatn0  39772  ltrnnidn  39774  trlnidatb  39777  trlnle  39786  trlval3  39787  trlval4  39788  cdlemc5  39795  cdleme0e  39817  cdleme3  39837  cdleme7c  39845  cdleme7ga  39848  cdleme7  39849  cdleme11k  39868  cdleme15b  39875  cdleme16b  39879  cdleme16e  39882  cdleme16f  39883  cdlemednpq  39899  cdleme20zN  39901  cdleme20j  39918  cdleme22aa  39939  cdleme22cN  39942  cdleme22d  39943  cdlemf2  40162  cdlemb3  40206  cdlemg12e  40247  cdlemg17dALTN  40264  cdlemg19a  40283  cdlemg27b  40296  cdlemg31d  40300  cdlemg33c  40308  cdlemg33e  40310  trlcone  40328  cdlemi  40420  tendotr  40430  cdlemk17  40458  cdlemk52  40554  cdleml1N  40576  dian0  40639  dia0  40652  dia2dimlem1  40664  dia2dimlem2  40665  dia2dimlem3  40666  dih0cnv  40883  dihmeetlem4preN  40906  dihmeetlem7N  40910  dihmeetlem17N  40923  dihlspsnat  40933  dihatexv  40938