Theorem atelch 32979

Description: An atom is a Hilbert lattice element. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)

Assertion

Ref	Expression
atelch	⊢ (𝐴 ∈ HAtoms → 𝐴 ∈ Cℋ )

Proof of Theorem atelch

Step	Hyp	Ref	Expression
1		atssch 32978	. 2 ⊢ HAtoms ⊆ Cℋ
2	1	sseli 3909	1 ⊢ (𝐴 ∈ HAtoms → 𝐴 ∈ Cℋ )

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   C_ℋ cch 31564  HAtomscat 31600

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-ss 3901  df-at 32973

This theorem is used by:  atsseq  32982  atcveq0  32983  chcv1  32990  chcv2  32991  hatomistici  32997  chrelati  32999  chrelat2i  33000  cvati  33001  cvexchlem  33003  cvp  33010  atnemeq0  33012  atcv0eq  33014  atcv1  33015  atexch  33016  atomli  33017  atoml2i  33018  atordi  33019  atcvatlem  33020  atcvati  33021  atcvat2i  33022  chirredlem1  33025  chirredlem2  33026  chirredlem3  33027  chirredlem4  33028  chirredi  33029  atcvat3i  33031  atcvat4i  33032  atdmd  33033  atmd  33034  atmd2  33035  atabsi  33036  mdsymlem2  33039  mdsymlem3  33040  mdsymlem5  33042  mdsymlem8  33045  atdmd2  33049  sumdmdi  33055  dmdbr4ati  33056  dmdbr5ati  33057  dmdbr6ati  33058