Theorem hlatl 40175

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  AtLatcal 40079  CvLatclc 40080  HLchlt 40165

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426  df-cvlat 40137  df-hlat 40166

This theorem is used by:  hllat  40178  hlomcmat  40180  intnatN  40222  cvratlem  40236  atcvrj0  40243  atcvrneN  40245  atcvrj1  40246  atcvrj2b  40247  atltcvr  40250  cvrat4  40258  2atjm  40260  atbtwn  40261  3dim2  40283  2dim  40285  1cvrjat  40290  ps-2  40293  ps-2b  40297  islln3  40325  llnnleat  40328  llnexatN  40336  2llnmat  40339  2atm  40342  2llnm3N  40384  2llnm4  40385  2llnmeqat  40386  dalem21  40509  dalem24  40512  dalem25  40513  dalem54  40541  dalem55  40542  dalem57  40544  pmapat  40578  pmapeq0  40581  isline4N  40592  2lnat  40599  2llnma1b  40601  cdlema2N  40607  cdlemblem  40608  pmapjat1  40668  llnexchb2lem  40683  pol1N  40725  pnonsingN  40748  pclfinclN  40765  lhpocnle  40831  lhpmat  40845  lhpmatb  40846  lhp2at0  40847  lhp2atnle  40848  lhp2at0nle  40850  lhpat3  40861  4atexlemcnd  40887  trlatn0  40987  ltrnnidn  40989  trlnidatb  40992  trlnle  41001  trlval3  41002  trlval4  41003  cdlemc5  41010  cdleme0e  41032  cdleme3  41052  cdleme7c  41060  cdleme7ga  41063  cdleme7  41064  cdleme11k  41083  cdleme15b  41090  cdleme16b  41094  cdleme16e  41097  cdleme16f  41098  cdlemednpq  41114  cdleme20zN  41116  cdleme20j  41133  cdleme22aa  41154  cdleme22cN  41157  cdleme22d  41158  cdlemf2  41377  cdlemb3  41421  cdlemg12e  41462  cdlemg17dALTN  41479  cdlemg19a  41498  cdlemg27b  41511  cdlemg31d  41515  cdlemg33c  41523  cdlemg33e  41525  trlcone  41543  cdlemi  41635  tendotr  41645  cdlemk17  41673  cdlemk52  41769  cdleml1N  41791  dian0  41854  dia0  41867  dia2dimlem1  41879  dia2dimlem2  41880  dia2dimlem3  41881  dih0cnv  42098  dihmeetlem4preN  42121  dihmeetlem7N  42125  dihmeetlem17N  42138  dihlspsnat  42148  dihatexv  42153