![]() |
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 35434 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat) | |
2 | cvlatl 35400 | . 2 ⊢ (𝐾 ∈ CvLat → 𝐾 ∈ AtLat) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2166 AtLatcal 35339 CvLatclc 35340 HLchlt 35425 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ral 3122 df-rex 3123 df-rab 3126 df-v 3416 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-uni 4659 df-br 4874 df-iota 6086 df-fv 6131 df-ov 6908 df-cvlat 35397 df-hlat 35426 |
This theorem is referenced by: hllat 35438 hlomcmat 35440 intnatN 35482 cvratlem 35496 atcvrj0 35503 atcvrneN 35505 atcvrj1 35506 atcvrj2b 35507 atltcvr 35510 cvrat4 35518 2atjm 35520 atbtwn 35521 3dim2 35543 2dim 35545 1cvrjat 35550 ps-2 35553 ps-2b 35557 islln3 35585 llnnleat 35588 llnexatN 35596 2llnmat 35599 2atm 35602 2llnm3N 35644 2llnm4 35645 2llnmeqat 35646 dalem21 35769 dalem24 35772 dalem25 35773 dalem54 35801 dalem55 35802 dalem57 35804 pmapat 35838 pmapeq0 35841 isline4N 35852 2lnat 35859 2llnma1b 35861 cdlema2N 35867 cdlemblem 35868 pmapjat1 35928 llnexchb2lem 35943 pol1N 35985 pnonsingN 36008 pclfinclN 36025 lhpocnle 36091 lhpmat 36105 lhpmatb 36106 lhp2at0 36107 lhp2atnle 36108 lhp2at0nle 36110 lhpat3 36121 4atexlemcnd 36147 trlatn0 36247 ltrnnidn 36249 trlnidatb 36252 trlnle 36261 trlval3 36262 trlval4 36263 cdlemc5 36270 cdleme0e 36292 cdleme3 36312 cdleme7c 36320 cdleme7ga 36323 cdleme7 36324 cdleme11k 36343 cdleme15b 36350 cdleme16b 36354 cdleme16e 36357 cdleme16f 36358 cdlemednpq 36374 cdleme20zN 36376 cdleme20j 36393 cdleme22aa 36414 cdleme22cN 36417 cdleme22d 36418 cdlemf2 36637 cdlemb3 36681 cdlemg12e 36722 cdlemg17dALTN 36739 cdlemg19a 36758 cdlemg27b 36771 cdlemg31d 36775 cdlemg33c 36783 cdlemg33e 36785 trlcone 36803 cdlemi 36895 tendotr 36905 cdlemk17 36933 cdlemk52 37029 cdleml1N 37051 dian0 37114 dia0 37127 dia2dimlem1 37139 dia2dimlem2 37140 dia2dimlem3 37141 dih0cnv 37358 dihmeetlem4preN 37381 dihmeetlem7N 37385 dihmeetlem17N 37398 dihlspsnat 37408 dihatexv 37413 |
Copyright terms: Public domain | W3C validator |