![]() |
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 29727 | . 2 ⊢ HAtoms ⊆ Cℋ | |
2 | 1 | sseli 3794 | 1 ⊢ (𝐴 ∈ HAtoms → 𝐴 ∈ Cℋ ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2157 Cℋ cch 28311 HAtomscat 28347 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-rab 3098 df-in 3776 df-ss 3783 df-at 29722 |
This theorem is referenced by: atsseq 29731 atcveq0 29732 chcv1 29739 chcv2 29740 hatomistici 29746 chrelati 29748 chrelat2i 29749 cvati 29750 cvexchlem 29752 cvp 29759 atnemeq0 29761 atcv0eq 29763 atcv1 29764 atexch 29765 atomli 29766 atoml2i 29767 atordi 29768 atcvatlem 29769 atcvati 29770 atcvat2i 29771 chirredlem1 29774 chirredlem2 29775 chirredlem3 29776 chirredlem4 29777 chirredi 29778 atcvat3i 29780 atcvat4i 29781 atdmd 29782 atmd 29783 atmd2 29784 atabsi 29785 mdsymlem2 29788 mdsymlem3 29789 mdsymlem5 29791 mdsymlem8 29794 atdmd2 29798 sumdmdi 29804 dmdbr4ati 29805 dmdbr5ati 29806 dmdbr6ati 29807 |
Copyright terms: Public domain | W3C validator |