![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > atelch | Structured version Visualization version GIF version |
Description: An atom is a Hilbert lattice element. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
Ref | Expression |
---|---|
atelch | ⊢ (𝐴 ∈ HAtoms → 𝐴 ∈ Cℋ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | atssch 32273 | . 2 ⊢ HAtoms ⊆ Cℋ | |
2 | 1 | sseli 3974 | 1 ⊢ (𝐴 ∈ HAtoms → 𝐴 ∈ Cℋ ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2099 Cℋ cch 30859 HAtomscat 30895 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-ss 3963 df-at 32268 |
This theorem is referenced by: atsseq 32277 atcveq0 32278 chcv1 32285 chcv2 32286 hatomistici 32292 chrelati 32294 chrelat2i 32295 cvati 32296 cvexchlem 32298 cvp 32305 atnemeq0 32307 atcv0eq 32309 atcv1 32310 atexch 32311 atomli 32312 atoml2i 32313 atordi 32314 atcvatlem 32315 atcvati 32316 atcvat2i 32317 chirredlem1 32320 chirredlem2 32321 chirredlem3 32322 chirredlem4 32323 chirredi 32324 atcvat3i 32326 atcvat4i 32327 atdmd 32328 atmd 32329 atmd2 32330 atabsi 32331 mdsymlem2 32334 mdsymlem3 32335 mdsymlem5 32337 mdsymlem8 32340 atdmd2 32344 sumdmdi 32350 dmdbr4ati 32351 dmdbr5ati 32352 dmdbr6ati 32353 |
Copyright terms: Public domain | W3C validator |