Theorem hlatl 36498

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

Syntax hints:   → wi 4   ∈ wcel 2114  AtLatcal 36402  CvLatclc 36403  HLchlt 36488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365  df-ov 7161  df-cvlat 36460  df-hlat 36489

This theorem is referenced by:  hllat  36501  hlomcmat  36503  intnatN  36545  cvratlem  36559  atcvrj0  36566  atcvrneN  36568  atcvrj1  36569  atcvrj2b  36570  atltcvr  36573  cvrat4  36581  2atjm  36583  atbtwn  36584  3dim2  36606  2dim  36608  1cvrjat  36613  ps-2  36616  ps-2b  36620  islln3  36648  llnnleat  36651  llnexatN  36659  2llnmat  36662  2atm  36665  2llnm3N  36707  2llnm4  36708  2llnmeqat  36709  dalem21  36832  dalem24  36835  dalem25  36836  dalem54  36864  dalem55  36865  dalem57  36867  pmapat  36901  pmapeq0  36904  isline4N  36915  2lnat  36922  2llnma1b  36924  cdlema2N  36930  cdlemblem  36931  pmapjat1  36991  llnexchb2lem  37006  pol1N  37048  pnonsingN  37071  pclfinclN  37088  lhpocnle  37154  lhpmat  37168  lhpmatb  37169  lhp2at0  37170  lhp2atnle  37171  lhp2at0nle  37173  lhpat3  37184  4atexlemcnd  37210  trlatn0  37310  ltrnnidn  37312  trlnidatb  37315  trlnle  37324  trlval3  37325  trlval4  37326  cdlemc5  37333  cdleme0e  37355  cdleme3  37375  cdleme7c  37383  cdleme7ga  37386  cdleme7  37387  cdleme11k  37406  cdleme15b  37413  cdleme16b  37417  cdleme16e  37420  cdleme16f  37421  cdlemednpq  37437  cdleme20zN  37439  cdleme20j  37456  cdleme22aa  37477  cdleme22cN  37480  cdleme22d  37481  cdlemf2  37700  cdlemb3  37744  cdlemg12e  37785  cdlemg17dALTN  37802  cdlemg19a  37821  cdlemg27b  37834  cdlemg31d  37838  cdlemg33c  37846  cdlemg33e  37848  trlcone  37866  cdlemi  37958  tendotr  37968  cdlemk17  37996  cdlemk52  38092  cdleml1N  38114  dian0  38177  dia0  38190  dia2dimlem1  38202  dia2dimlem2  38203  dia2dimlem3  38204  dih0cnv  38421  dihmeetlem4preN  38444  dihmeetlem7N  38448  dihmeetlem17N  38461  dihlspsnat  38471  dihatexv  38476