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 34646 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat) | |
2 | cvlatl 34612 | . 2 ⊢ (𝐾 ∈ CvLat → 𝐾 ∈ AtLat) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 1990 AtLatcal 34551 CvLatclc 34552 HLchlt 34637 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-iota 5851 df-fv 5896 df-ov 6653 df-cvlat 34609 df-hlat 34638 |
This theorem is referenced by: hllat 34650 hlomcmat 34651 intnatN 34693 cvratlem 34707 atcvrj0 34714 atcvrneN 34716 atcvrj1 34717 atcvrj2b 34718 atltcvr 34721 cvrat4 34729 2atjm 34731 atbtwn 34732 3dim2 34754 2dim 34756 1cvrjat 34761 ps-2 34764 ps-2b 34768 islln3 34796 llnnleat 34799 llnexatN 34807 2llnmat 34810 2atm 34813 2llnm3N 34855 2llnm4 34856 2llnmeqat 34857 dalem21 34980 dalem24 34983 dalem25 34984 dalem54 35012 dalem55 35013 dalem57 35015 pmapat 35049 pmapeq0 35052 isline4N 35063 2lnat 35070 2llnma1b 35072 cdlema2N 35078 cdlemblem 35079 pmapjat1 35139 llnexchb2lem 35154 pol1N 35196 pnonsingN 35219 pclfinclN 35236 lhpocnle 35302 lhpmat 35316 lhpmatb 35317 lhp2at0 35318 lhp2atnle 35319 lhp2at0nle 35321 lhpat3 35332 4atexlemcnd 35358 ltrnmwOLD 35438 trlatn0 35459 ltrnnidn 35461 trlnidatb 35464 trlnle 35473 trlval3 35474 trlval4 35475 cdlemc5 35482 cdleme0e 35504 cdleme3 35524 cdleme7c 35532 cdleme7ga 35535 cdleme7 35536 cdleme11k 35555 cdleme15b 35562 cdleme16b 35566 cdleme16e 35569 cdleme16f 35570 cdlemednpq 35586 cdleme20zN 35588 cdleme20yOLD 35590 cdleme20j 35606 cdleme22aa 35627 cdleme22cN 35630 cdleme22d 35631 cdlemf2 35850 cdlemb3 35894 cdlemg12e 35935 cdlemg17dALTN 35952 cdlemg19a 35971 cdlemg27b 35984 cdlemg31d 35988 cdlemg33c 35996 cdlemg33e 35998 trlcone 36016 cdlemi 36108 tendotr 36118 cdlemk17 36146 cdlemk52 36242 cdleml1N 36264 dian0 36328 dia0 36341 dia2dimlem1 36353 dia2dimlem2 36354 dia2dimlem3 36355 dih0cnv 36572 dihmeetlem4preN 36595 dihmeetlem7N 36599 dihmeetlem17N 36612 dihlspsnat 36622 dihatexv 36627 |
Copyright terms: Public domain | W3C validator |