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

Theorem hlatl 33311
Description: A Hilbert lattice is atomic. (Contributed by NM, 20-Oct-2011.)
Assertion
Ref Expression
hlatl  |-  ( K  e.  HL  ->  K  e.  AtLat )

Proof of Theorem hlatl
StepHypRef Expression
1 hlcvl 33310 . 2  |-  ( K  e.  HL  ->  K  e.  CvLat )
2 cvlatl 33276 . 2  |-  ( K  e.  CvLat  ->  K  e.  AtLat
)
31, 2syl 16 1  |-  ( K  e.  HL  ->  K  e.  AtLat )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   AtLatcal 33215   CvLatclc 33216   HLchlt 33301
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-iota 5479  df-fv 5524  df-ov 6193  df-cvlat 33273  df-hlat 33302
This theorem is referenced by:  hllat  33314  hlomcmat  33315  intnatN  33357  cvratlem  33371  atcvrj0  33378  atcvrneN  33380  atcvrj1  33381  atcvrj2b  33382  atltcvr  33385  cvrat4  33393  2atjm  33395  atbtwn  33396  3dim2  33418  2dim  33420  1cvrjat  33425  ps-2  33428  ps-2b  33432  islln3  33460  llnnleat  33463  llnexatN  33471  2llnmat  33474  2atm  33477  2llnm3N  33519  2llnm4  33520  2llnmeqat  33521  dalem21  33644  dalem24  33647  dalem25  33648  dalem54  33676  dalem55  33677  dalem57  33679  pmapat  33713  pmapeq0  33716  isline4N  33727  2lnat  33734  2llnma1b  33736  cdlema2N  33742  cdlemblem  33743  pmapjat1  33803  llnexchb2lem  33818  pol1N  33860  pnonsingN  33883  pclfinclN  33900  lhpocnle  33966  lhpmat  33980  lhpmatb  33981  lhp2at0  33982  lhp2atnle  33983  lhp2at0nle  33985  lhpat3  33996  4atexlemcnd  34022  ltrnmw  34101  trlatn0  34122  ltrnnidn  34124  trlnidatb  34127  trlnle  34136  trlval3  34137  trlval4  34138  cdlemc5  34145  cdleme0e  34167  cdleme3  34187  cdleme7c  34195  cdleme7ga  34198  cdleme7  34199  cdleme11k  34218  cdleme15b  34225  cdleme16b  34229  cdleme16e  34232  cdleme16f  34233  cdlemednpq  34249  cdleme20zN  34251  cdleme20y  34252  cdleme20j  34268  cdleme22aa  34289  cdleme22cN  34292  cdleme22d  34293  cdlemf2  34512  cdlemb3  34556  cdlemg12e  34597  cdlemg17dALTN  34614  cdlemg19a  34633  cdlemg27b  34646  cdlemg31d  34650  cdlemg33c  34658  cdlemg33e  34660  trlcone  34678  cdlemi  34770  tendotr  34780  cdlemk17  34808  cdlemk52  34904  cdleml1N  34926  dian0  34990  dia0  35003  dia2dimlem1  35015  dia2dimlem2  35016  dia2dimlem3  35017  dih0cnv  35234  dihmeetlem4preN  35257  dihmeetlem7N  35261  dihmeetlem17N  35274  dihlspsnat  35284  dihatexv  35289
  Copyright terms: Public domain W3C validator