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 36566
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 36565 . 2 (𝐾 ∈ HL → 𝐾 ∈ CvLat)
2 cvlatl 36531 . 2 (𝐾 ∈ CvLat → 𝐾 ∈ AtLat)
31, 2syl 17 1 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115  AtLatcal 36470  CvLatclc 36471  HLchlt 36556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-un 3924  df-in 3926  df-ss 3936  df-sn 4550  df-pr 4552  df-op 4556  df-uni 4825  df-br 5053  df-iota 6302  df-fv 6351  df-ov 7148  df-cvlat 36528  df-hlat 36557
This theorem is referenced by:  hllat  36569  hlomcmat  36571  intnatN  36613  cvratlem  36627  atcvrj0  36634  atcvrneN  36636  atcvrj1  36637  atcvrj2b  36638  atltcvr  36641  cvrat4  36649  2atjm  36651  atbtwn  36652  3dim2  36674  2dim  36676  1cvrjat  36681  ps-2  36684  ps-2b  36688  islln3  36716  llnnleat  36719  llnexatN  36727  2llnmat  36730  2atm  36733  2llnm3N  36775  2llnm4  36776  2llnmeqat  36777  dalem21  36900  dalem24  36903  dalem25  36904  dalem54  36932  dalem55  36933  dalem57  36935  pmapat  36969  pmapeq0  36972  isline4N  36983  2lnat  36990  2llnma1b  36992  cdlema2N  36998  cdlemblem  36999  pmapjat1  37059  llnexchb2lem  37074  pol1N  37116  pnonsingN  37139  pclfinclN  37156  lhpocnle  37222  lhpmat  37236  lhpmatb  37237  lhp2at0  37238  lhp2atnle  37239  lhp2at0nle  37241  lhpat3  37252  4atexlemcnd  37278  trlatn0  37378  ltrnnidn  37380  trlnidatb  37383  trlnle  37392  trlval3  37393  trlval4  37394  cdlemc5  37401  cdleme0e  37423  cdleme3  37443  cdleme7c  37451  cdleme7ga  37454  cdleme7  37455  cdleme11k  37474  cdleme15b  37481  cdleme16b  37485  cdleme16e  37488  cdleme16f  37489  cdlemednpq  37505  cdleme20zN  37507  cdleme20j  37524  cdleme22aa  37545  cdleme22cN  37548  cdleme22d  37549  cdlemf2  37768  cdlemb3  37812  cdlemg12e  37853  cdlemg17dALTN  37870  cdlemg19a  37889  cdlemg27b  37902  cdlemg31d  37906  cdlemg33c  37914  cdlemg33e  37916  trlcone  37934  cdlemi  38026  tendotr  38036  cdlemk17  38064  cdlemk52  38160  cdleml1N  38182  dian0  38245  dia0  38258  dia2dimlem1  38270  dia2dimlem2  38271  dia2dimlem3  38272  dih0cnv  38489  dihmeetlem4preN  38512  dihmeetlem7N  38516  dihmeetlem17N  38529  dihlspsnat  38539  dihatexv  38544
  Copyright terms: Public domain W3C validator