Theorem atelch 5742

Description: An atom is a Hilbert lattice element.

Assertion

Ref	Expression
atelch	|- (A e. Atoms -> A e. CH)

Proof of Theorem atelch

Step	Hyp	Ref	Expression
1		atssch 5741	. 2 |- Atoms (_ CH
2	1	sseli 1504	1 |- (A e. Atoms -> A e. CH)

Syntax hints:   -> wi 2   e. wcel 1092  CHcch 4968  Atomscat 4980

This theorem is referenced by:  atsseq 5745  atcveq0 5746  chcv1t 5751  chcv2t 5752  hatomistic 5755  chrelat 5757  chrelat2 5758  cvexchlem 5759  cvp 5764  atnem0 5766  atcv0eq 5767  atcv1 5768  atexch 5769  atcvatlem 5770  atcvat 5771  atcvat2 5772  atcvat3 5774  atcvat4 5775  mdsymlem2 5777  mdsymlem3 5778  mdsymlem5 5780  mdsymlem8 5783

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-rab 1208  df-in 1491  df-ss 1492  df-at 5737

metamath.org