Theorem hlatl 40112

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

Syntax hints:   → wi 4   ∈ wcel 2143  AtLatcal 40016  CvLatclc 40017  HLchlt 40102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-cvlat 40074  df-hlat 40103

This theorem is referenced by:  hllat  40115  hlomcmat  40117  intnatN  40159  cvratlem  40173  atcvrj0  40180  atcvrneN  40182  atcvrj1  40183  atcvrj2b  40184  atltcvr  40187  cvrat4  40195  2atjm  40197  atbtwn  40198  3dim2  40220  2dim  40222  1cvrjat  40227  ps-2  40230  ps-2b  40234  islln3  40262  llnnleat  40265  llnexatN  40273  2llnmat  40276  2atm  40279  2llnm3N  40321  2llnm4  40322  2llnmeqat  40323  dalem21  40446  dalem24  40449  dalem25  40450  dalem54  40478  dalem55  40479  dalem57  40481  pmapat  40515  pmapeq0  40518  isline4N  40529  2lnat  40536  2llnma1b  40538  cdlema2N  40544  cdlemblem  40545  pmapjat1  40605  llnexchb2lem  40620  pol1N  40662  pnonsingN  40685  pclfinclN  40702  lhpocnle  40768  lhpmat  40782  lhpmatb  40783  lhp2at0  40784  lhp2atnle  40785  lhp2at0nle  40787  lhpat3  40798  4atexlemcnd  40824  trlatn0  40924  ltrnnidn  40926  trlnidatb  40929  trlnle  40938  trlval3  40939  trlval4  40940  cdlemc5  40947  cdleme0e  40969  cdleme3  40989  cdleme7c  40997  cdleme7ga  41000  cdleme7  41001  cdleme11k  41020  cdleme15b  41027  cdleme16b  41031  cdleme16e  41034  cdleme16f  41035  cdlemednpq  41051  cdleme20zN  41053  cdleme20j  41070  cdleme22aa  41091  cdleme22cN  41094  cdleme22d  41095  cdlemf2  41314  cdlemb3  41358  cdlemg12e  41399  cdlemg17dALTN  41416  cdlemg19a  41435  cdlemg27b  41448  cdlemg31d  41452  cdlemg33c  41460  cdlemg33e  41462  trlcone  41480  cdlemi  41572  tendotr  41582  cdlemk17  41610  cdlemk52  41706  cdleml1N  41728  dian0  41791  dia0  41804  dia2dimlem1  41816  dia2dimlem2  41817  dia2dimlem3  41818  dih0cnv  42035  dihmeetlem4preN  42058  dihmeetlem7N  42062  dihmeetlem17N  42075  dihlspsnat  42085  dihatexv  42090