Theorem hlatl 40620

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  AtLatcal 40524  CvLatclc 40525  HLchlt 40610

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6515  df-fv 6569  df-ov 7449  df-cvlat 40582  df-hlat 40611

This theorem is used by:  hllat  40623  hlomcmat  40625  intnatN  40667  cvratlem  40681  atcvrj0  40688  atcvrneN  40690  atcvrj1  40691  atcvrj2b  40692  atltcvr  40695  cvrat4  40703  2atjm  40705  atbtwn  40706  3dim2  40728  2dim  40730  1cvrjat  40735  ps-2  40738  ps-2b  40742  islln3  40770  llnnleat  40773  llnexatN  40781  2llnmat  40784  2atm  40787  2llnm3N  40829  2llnm4  40830  2llnmeqat  40831  dalem21  40954  dalem24  40957  dalem25  40958  dalem54  40986  dalem55  40987  dalem57  40989  pmapat  41023  pmapeq0  41026  isline4N  41037  2lnat  41044  2llnma1b  41046  cdlema2N  41052  cdlemblem  41053  pmapjat1  41113  llnexchb2lem  41128  pol1N  41170  pnonsingN  41193  pclfinclN  41210  lhpocnle  41276  lhpmat  41290  lhpmatb  41291  lhp2at0  41292  lhp2atnle  41293  lhp2at0nle  41295  lhpat3  41306  4atexlemcnd  41332  trlatn0  41432  ltrnnidn  41434  trlnidatb  41437  trlnle  41446  trlval3  41447  trlval4  41448  cdlemc5  41455  cdleme0e  41477  cdleme3  41497  cdleme7c  41505  cdleme7ga  41508  cdleme7  41509  cdleme11k  41528  cdleme15b  41535  cdleme16b  41539  cdleme16e  41542  cdleme16f  41543  cdlemednpq  41559  cdleme20zN  41561  cdleme20j  41578  cdleme22aa  41599  cdleme22cN  41602  cdleme22d  41603  cdlemf2  41822  cdlemb3  41866  cdlemg12e  41907  cdlemg17dALTN  41924  cdlemg19a  41943  cdlemg27b  41956  cdlemg31d  41960  cdlemg33c  41968  cdlemg33e  41970  trlcone  41988  cdlemi  42080  tendotr  42090  cdlemk17  42118  cdlemk52  42214  cdleml1N  42236  dian0  42299  dia0  42312  dia2dimlem1  42324  dia2dimlem2  42325  dia2dimlem3  42326  dih0cnv  42543  dihmeetlem4preN  42566  dihmeetlem7N  42570  dihmeetlem17N  42583  dihlspsnat  42593  dihatexv  42598