![]() |
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 38958 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat) | |
2 | cvlatl 38924 | . 2 ⊢ (𝐾 ∈ CvLat → 𝐾 ∈ AtLat) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 AtLatcal 38863 CvLatclc 38864 HLchlt 38949 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-iota 6501 df-fv 6557 df-ov 7422 df-cvlat 38921 df-hlat 38950 |
This theorem is referenced by: hllat 38962 hlomcmat 38964 intnatN 39007 cvratlem 39021 atcvrj0 39028 atcvrneN 39030 atcvrj1 39031 atcvrj2b 39032 atltcvr 39035 cvrat4 39043 2atjm 39045 atbtwn 39046 3dim2 39068 2dim 39070 1cvrjat 39075 ps-2 39078 ps-2b 39082 islln3 39110 llnnleat 39113 llnexatN 39121 2llnmat 39124 2atm 39127 2llnm3N 39169 2llnm4 39170 2llnmeqat 39171 dalem21 39294 dalem24 39297 dalem25 39298 dalem54 39326 dalem55 39327 dalem57 39329 pmapat 39363 pmapeq0 39366 isline4N 39377 2lnat 39384 2llnma1b 39386 cdlema2N 39392 cdlemblem 39393 pmapjat1 39453 llnexchb2lem 39468 pol1N 39510 pnonsingN 39533 pclfinclN 39550 lhpocnle 39616 lhpmat 39630 lhpmatb 39631 lhp2at0 39632 lhp2atnle 39633 lhp2at0nle 39635 lhpat3 39646 4atexlemcnd 39672 trlatn0 39772 ltrnnidn 39774 trlnidatb 39777 trlnle 39786 trlval3 39787 trlval4 39788 cdlemc5 39795 cdleme0e 39817 cdleme3 39837 cdleme7c 39845 cdleme7ga 39848 cdleme7 39849 cdleme11k 39868 cdleme15b 39875 cdleme16b 39879 cdleme16e 39882 cdleme16f 39883 cdlemednpq 39899 cdleme20zN 39901 cdleme20j 39918 cdleme22aa 39939 cdleme22cN 39942 cdleme22d 39943 cdlemf2 40162 cdlemb3 40206 cdlemg12e 40247 cdlemg17dALTN 40264 cdlemg19a 40283 cdlemg27b 40296 cdlemg31d 40300 cdlemg33c 40308 cdlemg33e 40310 trlcone 40328 cdlemi 40420 tendotr 40430 cdlemk17 40458 cdlemk52 40554 cdleml1N 40576 dian0 40639 dia0 40652 dia2dimlem1 40664 dia2dimlem2 40665 dia2dimlem3 40666 dih0cnv 40883 dihmeetlem4preN 40906 dihmeetlem7N 40910 dihmeetlem17N 40923 dihlspsnat 40933 dihatexv 40938 |
Copyright terms: Public domain | W3C validator |