Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > hlatl | Structured version Visualization version GIF version |
Description: A Hilbert lattice is atomic. (Contributed by NM, 20-Oct-2011.) |
Ref | Expression |
---|---|
hlatl | ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hlcvl 36375 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat) | |
2 | cvlatl 36341 | . 2 ⊢ (𝐾 ∈ CvLat → 𝐾 ∈ AtLat) | |
3 | 1, 2 | syl 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 |