Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hlatl Structured version   Visualization version   GIF version

Theorem hlatl 37868
Description: A Hilbert lattice is atomic. (Contributed by NM, 20-Oct-2011.)
Assertion
Ref Expression
hlatl (𝐾 ∈ HL → 𝐾 ∈ AtLat)

Proof of Theorem hlatl
StepHypRef Expression
1 hlcvl 37867 . 2 (𝐾 ∈ HL → 𝐾 ∈ CvLat)
2 cvlatl 37833 . 2 (𝐾 ∈ CvLat → 𝐾 ∈ AtLat)
31, 2syl 17 1 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  AtLatcal 37772  CvLatclc 37773  HLchlt 37858
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361  df-cvlat 37830  df-hlat 37859
This theorem is referenced by:  hllat  37871  hlomcmat  37873  intnatN  37916  cvratlem  37930  atcvrj0  37937  atcvrneN  37939  atcvrj1  37940  atcvrj2b  37941  atltcvr  37944  cvrat4  37952  2atjm  37954  atbtwn  37955  3dim2  37977  2dim  37979  1cvrjat  37984  ps-2  37987  ps-2b  37991  islln3  38019  llnnleat  38022  llnexatN  38030  2llnmat  38033  2atm  38036  2llnm3N  38078  2llnm4  38079  2llnmeqat  38080  dalem21  38203  dalem24  38206  dalem25  38207  dalem54  38235  dalem55  38236  dalem57  38238  pmapat  38272  pmapeq0  38275  isline4N  38286  2lnat  38293  2llnma1b  38295  cdlema2N  38301  cdlemblem  38302  pmapjat1  38362  llnexchb2lem  38377  pol1N  38419  pnonsingN  38442  pclfinclN  38459  lhpocnle  38525  lhpmat  38539  lhpmatb  38540  lhp2at0  38541  lhp2atnle  38542  lhp2at0nle  38544  lhpat3  38555  4atexlemcnd  38581  trlatn0  38681  ltrnnidn  38683  trlnidatb  38686  trlnle  38695  trlval3  38696  trlval4  38697  cdlemc5  38704  cdleme0e  38726  cdleme3  38746  cdleme7c  38754  cdleme7ga  38757  cdleme7  38758  cdleme11k  38777  cdleme15b  38784  cdleme16b  38788  cdleme16e  38791  cdleme16f  38792  cdlemednpq  38808  cdleme20zN  38810  cdleme20j  38827  cdleme22aa  38848  cdleme22cN  38851  cdleme22d  38852  cdlemf2  39071  cdlemb3  39115  cdlemg12e  39156  cdlemg17dALTN  39173  cdlemg19a  39192  cdlemg27b  39205  cdlemg31d  39209  cdlemg33c  39217  cdlemg33e  39219  trlcone  39237  cdlemi  39329  tendotr  39339  cdlemk17  39367  cdlemk52  39463  cdleml1N  39485  dian0  39548  dia0  39561  dia2dimlem1  39573  dia2dimlem2  39574  dia2dimlem3  39575  dih0cnv  39792  dihmeetlem4preN  39815  dihmeetlem7N  39819  dihmeetlem17N  39832  dihlspsnat  39842  dihatexv  39847
  Copyright terms: Public domain W3C validator