Theorem hlatl 39859

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

Syntax hints:   → wi 4   ∈ wcel 2119  AtLatcal 39763  CvLatclc 39764  HLchlt 39849

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-cvlat 39821  df-hlat 39850

This theorem is referenced by:  hllat  39862  hlomcmat  39864  intnatN  39906  cvratlem  39920  atcvrj0  39927  atcvrneN  39929  atcvrj1  39930  atcvrj2b  39931  atltcvr  39934  cvrat4  39942  2atjm  39944  atbtwn  39945  3dim2  39967  2dim  39969  1cvrjat  39974  ps-2  39977  ps-2b  39981  islln3  40009  llnnleat  40012  llnexatN  40020  2llnmat  40023  2atm  40026  2llnm3N  40068  2llnm4  40069  2llnmeqat  40070  dalem21  40193  dalem24  40196  dalem25  40197  dalem54  40225  dalem55  40226  dalem57  40228  pmapat  40262  pmapeq0  40265  isline4N  40276  2lnat  40283  2llnma1b  40285  cdlema2N  40291  cdlemblem  40292  pmapjat1  40352  llnexchb2lem  40367  pol1N  40409  pnonsingN  40432  pclfinclN  40449  lhpocnle  40515  lhpmat  40529  lhpmatb  40530  lhp2at0  40531  lhp2atnle  40532  lhp2at0nle  40534  lhpat3  40545  4atexlemcnd  40571  trlatn0  40671  ltrnnidn  40673  trlnidatb  40676  trlnle  40685  trlval3  40686  trlval4  40687  cdlemc5  40694  cdleme0e  40716  cdleme3  40736  cdleme7c  40744  cdleme7ga  40747  cdleme7  40748  cdleme11k  40767  cdleme15b  40774  cdleme16b  40778  cdleme16e  40781  cdleme16f  40782  cdlemednpq  40798  cdleme20zN  40800  cdleme20j  40817  cdleme22aa  40838  cdleme22cN  40841  cdleme22d  40842  cdlemf2  41061  cdlemb3  41105  cdlemg12e  41146  cdlemg17dALTN  41163  cdlemg19a  41182  cdlemg27b  41195  cdlemg31d  41199  cdlemg33c  41207  cdlemg33e  41209  trlcone  41227  cdlemi  41319  tendotr  41329  cdlemk17  41357  cdlemk52  41453  cdleml1N  41475  dian0  41538  dia0  41551  dia2dimlem1  41563  dia2dimlem2  41564  dia2dimlem3  41565  dih0cnv  41782  dihmeetlem4preN  41805  dihmeetlem7N  41809  dihmeetlem17N  41822  dihlspsnat  41832  dihatexv  41837