Theorem atelch 10266

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 10265	. 2 |- Atoms (_ CH
2	1	sseli 2068	1 |- (A e. Atoms -> A e. CH)

Syntax hints:   -> wi 3   e. wcel 960  CHcch 8793  Atomscat 8828

This theorem is referenced by:  atsseq 10269  atcveq0 10270  chcv1t 10277  chcv2t 10278  hatomistic 10284  chrelat 10286  chrelat2 10287  cvat 10288  cvexchlem 10290  cvp 10297  atnem0 10299  atcv0eq 10301  atcv1t 10302  atexcht 10303  atoml 10304  atoml2 10305  atord 10306  atcvatlem 10307  atcvat 10308  atcvat2 10309  irredlem1 10312  irredlem2 10313  irredlem3 10314  irredlem4 10315  irred 10316  atcvat3 10318  atcvat4 10319  atdmd 10320  atmd 10321  atmd2 10322  atabs 10323  mdsymlem2 10326  mdsymlem3 10327  mdsymlem5 10329  mdsymlem8 10332  atdmd2 10336  sumdmd 10342  dmdbr4at 10343  dmdbr5at 10344  dmdbr6at 10345

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-rab 1655  df-in 2054  df-ss 2056  df-at 10260

Copyright terms: Public domain