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 36376
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 36375 . 2 (𝐾 ∈ HL → 𝐾 ∈ CvLat)
2 cvlatl 36341 . 2 (𝐾 ∈ CvLat → 𝐾 ∈ AtLat)
31, 2syl 17 1 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  AtLatcal 36280  CvLatclc 36281  HLchlt 36366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148  df-cvlat 36338  df-hlat 36367
This theorem is referenced by:  hllat  36379  hlomcmat  36381  intnatN  36423  cvratlem  36437  atcvrj0  36444  atcvrneN  36446  atcvrj1  36447  atcvrj2b  36448  atltcvr  36451  cvrat4  36459  2atjm  36461  atbtwn  36462  3dim2  36484  2dim  36486  1cvrjat  36491  ps-2  36494  ps-2b  36498  islln3  36526  llnnleat  36529  llnexatN  36537  2llnmat  36540  2atm  36543  2llnm3N  36585  2llnm4  36586  2llnmeqat  36587  dalem21  36710  dalem24  36713  dalem25  36714  dalem54  36742  dalem55  36743  dalem57  36745  pmapat  36779  pmapeq0  36782  isline4N  36793  2lnat  36800  2llnma1b  36802  cdlema2N  36808  cdlemblem  36809  pmapjat1  36869  llnexchb2lem  36884  pol1N  36926  pnonsingN  36949  pclfinclN  36966  lhpocnle  37032  lhpmat  37046  lhpmatb  37047  lhp2at0  37048  lhp2atnle  37049  lhp2at0nle  37051  lhpat3  37062  4atexlemcnd  37088  trlatn0  37188  ltrnnidn  37190  trlnidatb  37193  trlnle  37202  trlval3  37203  trlval4  37204  cdlemc5  37211  cdleme0e  37233  cdleme3  37253  cdleme7c  37261  cdleme7ga  37264  cdleme7  37265  cdleme11k  37284  cdleme15b  37291  cdleme16b  37295  cdleme16e  37298  cdleme16f  37299  cdlemednpq  37315  cdleme20zN  37317  cdleme20j  37334  cdleme22aa  37355  cdleme22cN  37358  cdleme22d  37359  cdlemf2  37578  cdlemb3  37622  cdlemg12e  37663  cdlemg17dALTN  37680  cdlemg19a  37699  cdlemg27b  37712  cdlemg31d  37716  cdlemg33c  37724  cdlemg33e  37726  trlcone  37744  cdlemi  37836  tendotr  37846  cdlemk17  37874  cdlemk52  37970  cdleml1N  37992  dian0  38055  dia0  38068  dia2dimlem1  38080  dia2dimlem2  38081  dia2dimlem3  38082  dih0cnv  38299  dihmeetlem4preN  38322  dihmeetlem7N  38326  dihmeetlem17N  38339  dihlspsnat  38349  dihatexv  38354
  Copyright terms: Public domain W3C validator