Theorem hlatl 39353

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

Syntax hints:   → wi 4   ∈ wcel 2109  AtLatcal 39257  CvLatclc 39258  HLchlt 39343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-cvlat 39315  df-hlat 39344

This theorem is referenced by:  hllat  39356  hlomcmat  39358  intnatN  39401  cvratlem  39415  atcvrj0  39422  atcvrneN  39424  atcvrj1  39425  atcvrj2b  39426  atltcvr  39429  cvrat4  39437  2atjm  39439  atbtwn  39440  3dim2  39462  2dim  39464  1cvrjat  39469  ps-2  39472  ps-2b  39476  islln3  39504  llnnleat  39507  llnexatN  39515  2llnmat  39518  2atm  39521  2llnm3N  39563  2llnm4  39564  2llnmeqat  39565  dalem21  39688  dalem24  39691  dalem25  39692  dalem54  39720  dalem55  39721  dalem57  39723  pmapat  39757  pmapeq0  39760  isline4N  39771  2lnat  39778  2llnma1b  39780  cdlema2N  39786  cdlemblem  39787  pmapjat1  39847  llnexchb2lem  39862  pol1N  39904  pnonsingN  39927  pclfinclN  39944  lhpocnle  40010  lhpmat  40024  lhpmatb  40025  lhp2at0  40026  lhp2atnle  40027  lhp2at0nle  40029  lhpat3  40040  4atexlemcnd  40066  trlatn0  40166  ltrnnidn  40168  trlnidatb  40171  trlnle  40180  trlval3  40181  trlval4  40182  cdlemc5  40189  cdleme0e  40211  cdleme3  40231  cdleme7c  40239  cdleme7ga  40242  cdleme7  40243  cdleme11k  40262  cdleme15b  40269  cdleme16b  40273  cdleme16e  40276  cdleme16f  40277  cdlemednpq  40293  cdleme20zN  40295  cdleme20j  40312  cdleme22aa  40333  cdleme22cN  40336  cdleme22d  40337  cdlemf2  40556  cdlemb3  40600  cdlemg12e  40641  cdlemg17dALTN  40658  cdlemg19a  40677  cdlemg27b  40690  cdlemg31d  40694  cdlemg33c  40702  cdlemg33e  40704  trlcone  40722  cdlemi  40814  tendotr  40824  cdlemk17  40852  cdlemk52  40948  cdleml1N  40970  dian0  41033  dia0  41046  dia2dimlem1  41058  dia2dimlem2  41059  dia2dimlem3  41060  dih0cnv  41277  dihmeetlem4preN  41300  dihmeetlem7N  41304  dihmeetlem17N  41317  dihlspsnat  41327  dihatexv  41332