Step |
Hyp |
Ref |
Expression |
1 |
|
shincl.1 |
|- A e. SH |
2 |
|
shincl.2 |
|- B e. SH |
3 |
1 2
|
shseli |
|- ( x e. ( A +H B ) <-> E. y e. A E. z e. B x = ( y +h z ) ) |
4 |
|
ssun1 |
|- A C_ ( A u. B ) |
5 |
1 2
|
shunssji |
|- ( A u. B ) C_ ( A vH B ) |
6 |
4 5
|
sstri |
|- A C_ ( A vH B ) |
7 |
6
|
sseli |
|- ( y e. A -> y e. ( A vH B ) ) |
8 |
|
ssun2 |
|- B C_ ( A u. B ) |
9 |
8 5
|
sstri |
|- B C_ ( A vH B ) |
10 |
9
|
sseli |
|- ( z e. B -> z e. ( A vH B ) ) |
11 |
|
shjcl |
|- ( ( A e. SH /\ B e. SH ) -> ( A vH B ) e. CH ) |
12 |
1 2 11
|
mp2an |
|- ( A vH B ) e. CH |
13 |
12
|
chshii |
|- ( A vH B ) e. SH |
14 |
|
shaddcl |
|- ( ( ( A vH B ) e. SH /\ y e. ( A vH B ) /\ z e. ( A vH B ) ) -> ( y +h z ) e. ( A vH B ) ) |
15 |
13 14
|
mp3an1 |
|- ( ( y e. ( A vH B ) /\ z e. ( A vH B ) ) -> ( y +h z ) e. ( A vH B ) ) |
16 |
7 10 15
|
syl2an |
|- ( ( y e. A /\ z e. B ) -> ( y +h z ) e. ( A vH B ) ) |
17 |
|
eleq1a |
|- ( ( y +h z ) e. ( A vH B ) -> ( x = ( y +h z ) -> x e. ( A vH B ) ) ) |
18 |
16 17
|
syl |
|- ( ( y e. A /\ z e. B ) -> ( x = ( y +h z ) -> x e. ( A vH B ) ) ) |
19 |
18
|
rexlimivv |
|- ( E. y e. A E. z e. B x = ( y +h z ) -> x e. ( A vH B ) ) |
20 |
3 19
|
sylbi |
|- ( x e. ( A +H B ) -> x e. ( A vH B ) ) |
21 |
20
|
ssriv |
|- ( A +H B ) C_ ( A vH B ) |