Theorem hlatl 39341

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

Syntax hints:   → wi 4   ∈ wcel 2105  AtLatcal 39245  CvLatclc 39246  HLchlt 39331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-cvlat 39303  df-hlat 39332

This theorem is referenced by:  hllat  39344  hlomcmat  39346  intnatN  39389  cvratlem  39403  atcvrj0  39410  atcvrneN  39412  atcvrj1  39413  atcvrj2b  39414  atltcvr  39417  cvrat4  39425  2atjm  39427  atbtwn  39428  3dim2  39450  2dim  39452  1cvrjat  39457  ps-2  39460  ps-2b  39464  islln3  39492  llnnleat  39495  llnexatN  39503  2llnmat  39506  2atm  39509  2llnm3N  39551  2llnm4  39552  2llnmeqat  39553  dalem21  39676  dalem24  39679  dalem25  39680  dalem54  39708  dalem55  39709  dalem57  39711  pmapat  39745  pmapeq0  39748  isline4N  39759  2lnat  39766  2llnma1b  39768  cdlema2N  39774  cdlemblem  39775  pmapjat1  39835  llnexchb2lem  39850  pol1N  39892  pnonsingN  39915  pclfinclN  39932  lhpocnle  39998  lhpmat  40012  lhpmatb  40013  lhp2at0  40014  lhp2atnle  40015  lhp2at0nle  40017  lhpat3  40028  4atexlemcnd  40054  trlatn0  40154  ltrnnidn  40156  trlnidatb  40159  trlnle  40168  trlval3  40169  trlval4  40170  cdlemc5  40177  cdleme0e  40199  cdleme3  40219  cdleme7c  40227  cdleme7ga  40230  cdleme7  40231  cdleme11k  40250  cdleme15b  40257  cdleme16b  40261  cdleme16e  40264  cdleme16f  40265  cdlemednpq  40281  cdleme20zN  40283  cdleme20j  40300  cdleme22aa  40321  cdleme22cN  40324  cdleme22d  40325  cdlemf2  40544  cdlemb3  40588  cdlemg12e  40629  cdlemg17dALTN  40646  cdlemg19a  40665  cdlemg27b  40678  cdlemg31d  40682  cdlemg33c  40690  cdlemg33e  40692  trlcone  40710  cdlemi  40802  tendotr  40812  cdlemk17  40840  cdlemk52  40936  cdleml1N  40958  dian0  41021  dia0  41034  dia2dimlem1  41046  dia2dimlem2  41047  dia2dimlem3  41048  dih0cnv  41265  dihmeetlem4preN  41288  dihmeetlem7N  41292  dihmeetlem17N  41305  dihlspsnat  41315  dihatexv  41320