Theorem hlatl 39765

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

Syntax hints:   → wi 4   ∈ wcel 2114  AtLatcal 39669  CvLatclc 39670  HLchlt 39755

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6458  df-fv 6510  df-ov 7373  df-cvlat 39727  df-hlat 39756

This theorem is referenced by:  hllat  39768  hlomcmat  39770  intnatN  39812  cvratlem  39826  atcvrj0  39833  atcvrneN  39835  atcvrj1  39836  atcvrj2b  39837  atltcvr  39840  cvrat4  39848  2atjm  39850  atbtwn  39851  3dim2  39873  2dim  39875  1cvrjat  39880  ps-2  39883  ps-2b  39887  islln3  39915  llnnleat  39918  llnexatN  39926  2llnmat  39929  2atm  39932  2llnm3N  39974  2llnm4  39975  2llnmeqat  39976  dalem21  40099  dalem24  40102  dalem25  40103  dalem54  40131  dalem55  40132  dalem57  40134  pmapat  40168  pmapeq0  40171  isline4N  40182  2lnat  40189  2llnma1b  40191  cdlema2N  40197  cdlemblem  40198  pmapjat1  40258  llnexchb2lem  40273  pol1N  40315  pnonsingN  40338  pclfinclN  40355  lhpocnle  40421  lhpmat  40435  lhpmatb  40436  lhp2at0  40437  lhp2atnle  40438  lhp2at0nle  40440  lhpat3  40451  4atexlemcnd  40477  trlatn0  40577  ltrnnidn  40579  trlnidatb  40582  trlnle  40591  trlval3  40592  trlval4  40593  cdlemc5  40600  cdleme0e  40622  cdleme3  40642  cdleme7c  40650  cdleme7ga  40653  cdleme7  40654  cdleme11k  40673  cdleme15b  40680  cdleme16b  40684  cdleme16e  40687  cdleme16f  40688  cdlemednpq  40704  cdleme20zN  40706  cdleme20j  40723  cdleme22aa  40744  cdleme22cN  40747  cdleme22d  40748  cdlemf2  40967  cdlemb3  41011  cdlemg12e  41052  cdlemg17dALTN  41069  cdlemg19a  41088  cdlemg27b  41101  cdlemg31d  41105  cdlemg33c  41113  cdlemg33e  41115  trlcone  41133  cdlemi  41225  tendotr  41235  cdlemk17  41263  cdlemk52  41359  cdleml1N  41381  dian0  41444  dia0  41457  dia2dimlem1  41469  dia2dimlem2  41470  dia2dimlem3  41471  dih0cnv  41688  dihmeetlem4preN  41711  dihmeetlem7N  41715  dihmeetlem17N  41728  dihlspsnat  41738  dihatexv  41743