Theorem hlatl 35435

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

Syntax hints:   → wi 4   ∈ wcel 2166  AtLatcal 35339  CvLatclc 35340  HLchlt 35425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-iota 6086  df-fv 6131  df-ov 6908  df-cvlat 35397  df-hlat 35426

This theorem is referenced by:  hllat  35438  hlomcmat  35440  intnatN  35482  cvratlem  35496  atcvrj0  35503  atcvrneN  35505  atcvrj1  35506  atcvrj2b  35507  atltcvr  35510  cvrat4  35518  2atjm  35520  atbtwn  35521  3dim2  35543  2dim  35545  1cvrjat  35550  ps-2  35553  ps-2b  35557  islln3  35585  llnnleat  35588  llnexatN  35596  2llnmat  35599  2atm  35602  2llnm3N  35644  2llnm4  35645  2llnmeqat  35646  dalem21  35769  dalem24  35772  dalem25  35773  dalem54  35801  dalem55  35802  dalem57  35804  pmapat  35838  pmapeq0  35841  isline4N  35852  2lnat  35859  2llnma1b  35861  cdlema2N  35867  cdlemblem  35868  pmapjat1  35928  llnexchb2lem  35943  pol1N  35985  pnonsingN  36008  pclfinclN  36025  lhpocnle  36091  lhpmat  36105  lhpmatb  36106  lhp2at0  36107  lhp2atnle  36108  lhp2at0nle  36110  lhpat3  36121  4atexlemcnd  36147  trlatn0  36247  ltrnnidn  36249  trlnidatb  36252  trlnle  36261  trlval3  36262  trlval4  36263  cdlemc5  36270  cdleme0e  36292  cdleme3  36312  cdleme7c  36320  cdleme7ga  36323  cdleme7  36324  cdleme11k  36343  cdleme15b  36350  cdleme16b  36354  cdleme16e  36357  cdleme16f  36358  cdlemednpq  36374  cdleme20zN  36376  cdleme20j  36393  cdleme22aa  36414  cdleme22cN  36417  cdleme22d  36418  cdlemf2  36637  cdlemb3  36681  cdlemg12e  36722  cdlemg17dALTN  36739  cdlemg19a  36758  cdlemg27b  36771  cdlemg31d  36775  cdlemg33c  36783  cdlemg33e  36785  trlcone  36803  cdlemi  36895  tendotr  36905  cdlemk17  36933  cdlemk52  37029  cdleml1N  37051  dian0  37114  dia0  37127  dia2dimlem1  37139  dia2dimlem2  37140  dia2dimlem3  37141  dih0cnv  37358  dihmeetlem4preN  37381  dihmeetlem7N  37385  dihmeetlem17N  37398  dihlspsnat  37408  dihatexv  37413