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

Theorem hlatl 34034
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 34033 . 2  |-  ( K  e.  HL  ->  K  e.  CvLat )
2 cvlatl 33999 . 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 1762   AtLatcal 33938   CvLatclc 33939   HLchlt 34024
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ral 2814  df-rex 2815  df-rab 2818  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-uni 4241  df-br 4443  df-iota 5544  df-fv 5589  df-ov 6280  df-cvlat 33996  df-hlat 34025
This theorem is referenced by:  hllat  34037  hlomcmat  34038  intnatN  34080  cvratlem  34094  atcvrj0  34101  atcvrneN  34103  atcvrj1  34104  atcvrj2b  34105  atltcvr  34108  cvrat4  34116  2atjm  34118  atbtwn  34119  3dim2  34141  2dim  34143  1cvrjat  34148  ps-2  34151  ps-2b  34155  islln3  34183  llnnleat  34186  llnexatN  34194  2llnmat  34197  2atm  34200  2llnm3N  34242  2llnm4  34243  2llnmeqat  34244  dalem21  34367  dalem24  34370  dalem25  34371  dalem54  34399  dalem55  34400  dalem57  34402  pmapat  34436  pmapeq0  34439  isline4N  34450  2lnat  34457  2llnma1b  34459  cdlema2N  34465  cdlemblem  34466  pmapjat1  34526  llnexchb2lem  34541  pol1N  34583  pnonsingN  34606  pclfinclN  34623  lhpocnle  34689  lhpmat  34703  lhpmatb  34704  lhp2at0  34705  lhp2atnle  34706  lhp2at0nle  34708  lhpat3  34719  4atexlemcnd  34745  ltrnmw  34824  trlatn0  34845  ltrnnidn  34847  trlnidatb  34850  trlnle  34859  trlval3  34860  trlval4  34861  cdlemc5  34868  cdleme0e  34890  cdleme3  34910  cdleme7c  34918  cdleme7ga  34921  cdleme7  34922  cdleme11k  34941  cdleme15b  34948  cdleme16b  34952  cdleme16e  34955  cdleme16f  34956  cdlemednpq  34972  cdleme20zN  34974  cdleme20y  34975  cdleme20j  34991  cdleme22aa  35012  cdleme22cN  35015  cdleme22d  35016  cdlemf2  35235  cdlemb3  35279  cdlemg12e  35320  cdlemg17dALTN  35337  cdlemg19a  35356  cdlemg27b  35369  cdlemg31d  35373  cdlemg33c  35381  cdlemg33e  35383  trlcone  35401  cdlemi  35493  tendotr  35503  cdlemk17  35531  cdlemk52  35627  cdleml1N  35649  dian0  35713  dia0  35726  dia2dimlem1  35738  dia2dimlem2  35739  dia2dimlem3  35740  dih0cnv  35957  dihmeetlem4preN  35980  dihmeetlem7N  35984  dihmeetlem17N  35997  dihlspsnat  36007  dihatexv  36012
  Copyright terms: Public domain W3C validator