| 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 39360 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat) | |
| 2 | cvlatl 39326 | . 2 ⊢ (𝐾 ∈ CvLat → 𝐾 ∈ AtLat) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 AtLatcal 39265 CvLatclc 39266 HLchlt 39351 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-iota 6514 df-fv 6569 df-ov 7434 df-cvlat 39323 df-hlat 39352 |
| This theorem is referenced by: hllat 39364 hlomcmat 39366 intnatN 39409 cvratlem 39423 atcvrj0 39430 atcvrneN 39432 atcvrj1 39433 atcvrj2b 39434 atltcvr 39437 cvrat4 39445 2atjm 39447 atbtwn 39448 3dim2 39470 2dim 39472 1cvrjat 39477 ps-2 39480 ps-2b 39484 islln3 39512 llnnleat 39515 llnexatN 39523 2llnmat 39526 2atm 39529 2llnm3N 39571 2llnm4 39572 2llnmeqat 39573 dalem21 39696 dalem24 39699 dalem25 39700 dalem54 39728 dalem55 39729 dalem57 39731 pmapat 39765 pmapeq0 39768 isline4N 39779 2lnat 39786 2llnma1b 39788 cdlema2N 39794 cdlemblem 39795 pmapjat1 39855 llnexchb2lem 39870 pol1N 39912 pnonsingN 39935 pclfinclN 39952 lhpocnle 40018 lhpmat 40032 lhpmatb 40033 lhp2at0 40034 lhp2atnle 40035 lhp2at0nle 40037 lhpat3 40048 4atexlemcnd 40074 trlatn0 40174 ltrnnidn 40176 trlnidatb 40179 trlnle 40188 trlval3 40189 trlval4 40190 cdlemc5 40197 cdleme0e 40219 cdleme3 40239 cdleme7c 40247 cdleme7ga 40250 cdleme7 40251 cdleme11k 40270 cdleme15b 40277 cdleme16b 40281 cdleme16e 40284 cdleme16f 40285 cdlemednpq 40301 cdleme20zN 40303 cdleme20j 40320 cdleme22aa 40341 cdleme22cN 40344 cdleme22d 40345 cdlemf2 40564 cdlemb3 40608 cdlemg12e 40649 cdlemg17dALTN 40666 cdlemg19a 40685 cdlemg27b 40698 cdlemg31d 40702 cdlemg33c 40710 cdlemg33e 40712 trlcone 40730 cdlemi 40822 tendotr 40832 cdlemk17 40860 cdlemk52 40956 cdleml1N 40978 dian0 41041 dia0 41054 dia2dimlem1 41066 dia2dimlem2 41067 dia2dimlem3 41068 dih0cnv 41285 dihmeetlem4preN 41308 dihmeetlem7N 41312 dihmeetlem17N 41325 dihlspsnat 41335 dihatexv 41340 |
| Copyright terms: Public domain | W3C validator |