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

Theorem hlatl 30059
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 30058 . 2  |-  ( K  e.  HL  ->  K  e.  CvLat )
2 cvlatl 30024 . 2  |-  ( K  e.  CvLat  ->  K  e.  AtLat
)
31, 2syl 16 1  |-  ( K  e.  HL  ->  K  e.  AtLat )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   AtLatcal 29963   CvLatclc 29964   HLchlt 30049
This theorem is referenced by:  hllat  30062  hlomcmat  30063  intnatN  30105  cvratlem  30119  atcvrj0  30126  atcvrneN  30128  atcvrj1  30129  atcvrj2b  30130  atltcvr  30133  cvrat4  30141  2atjm  30143  atbtwn  30144  3dim2  30166  2dim  30168  1cvrjat  30173  ps-2  30176  ps-2b  30180  islln3  30208  llnnleat  30211  llnexatN  30219  2llnmat  30222  2atm  30225  2llnm3N  30267  2llnm4  30268  2llnmeqat  30269  dalem21  30392  dalem24  30395  dalem25  30396  dalem54  30424  dalem55  30425  dalem57  30427  pmapat  30461  pmapeq0  30464  isline4N  30475  2lnat  30482  2llnma1b  30484  cdlema2N  30490  cdlemblem  30491  pmapjat1  30551  llnexchb2lem  30566  pol1N  30608  pnonsingN  30631  pclfinclN  30648  lhpocnle  30714  lhpmat  30728  lhpmatb  30729  lhp2at0  30730  lhp2atnle  30731  lhp2at0nle  30733  lhpat3  30744  4atexlemcnd  30770  ltrnmw  30849  trlatn0  30870  ltrnnidn  30872  trlnidatb  30875  trlnle  30884  trlval3  30885  trlval4  30886  cdlemc5  30893  cdleme0e  30915  cdleme3  30935  cdleme7c  30943  cdleme7ga  30946  cdleme7  30947  cdleme11k  30966  cdleme15b  30973  cdleme16b  30977  cdleme16e  30980  cdleme16f  30981  cdlemednpq  30997  cdleme20zN  30999  cdleme20y  31000  cdleme20j  31016  cdleme22aa  31037  cdleme22cN  31040  cdleme22d  31041  cdlemf2  31260  cdlemb3  31304  cdlemg12e  31345  cdlemg17dALTN  31362  cdlemg19a  31381  cdlemg27b  31394  cdlemg31d  31398  cdlemg33c  31406  cdlemg33e  31408  trlcone  31426  cdlemi  31518  tendotr  31528  cdlemk17  31556  cdlemk52  31652  cdleml1N  31674  dian0  31738  dia0  31751  dia2dimlem1  31763  dia2dimlem2  31764  dia2dimlem3  31765  dih0cnv  31982  dihmeetlem4preN  32005  dihmeetlem7N  32009  dihmeetlem17N  32022  dihlspsnat  32032  dihatexv  32037
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-iota 5410  df-fv 5454  df-ov 6076  df-cvlat 30021  df-hlat 30050
  Copyright terms: Public domain W3C validator