Step |
Hyp |
Ref |
Expression |
1 |
|
shjshs.1 |
|- A e. SH |
2 |
|
shjshs.2 |
|- B e. SH |
3 |
|
shjval |
|- ( ( A e. SH /\ B e. SH ) -> ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) ) |
4 |
1 2 3
|
mp2an |
|- ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) |
5 |
1 2
|
shunssi |
|- ( A u. B ) C_ ( A +H B ) |
6 |
1
|
shssii |
|- A C_ ~H |
7 |
2
|
shssii |
|- B C_ ~H |
8 |
6 7
|
unssi |
|- ( A u. B ) C_ ~H |
9 |
1 2
|
shscli |
|- ( A +H B ) e. SH |
10 |
9
|
shssii |
|- ( A +H B ) C_ ~H |
11 |
8 10
|
occon2i |
|- ( ( A u. B ) C_ ( A +H B ) -> ( _|_ ` ( _|_ ` ( A u. B ) ) ) C_ ( _|_ ` ( _|_ ` ( A +H B ) ) ) ) |
12 |
5 11
|
ax-mp |
|- ( _|_ ` ( _|_ ` ( A u. B ) ) ) C_ ( _|_ ` ( _|_ ` ( A +H B ) ) ) |
13 |
4 12
|
eqsstri |
|- ( A vH B ) C_ ( _|_ ` ( _|_ ` ( A +H B ) ) ) |
14 |
1 2
|
shsleji |
|- ( A +H B ) C_ ( A vH B ) |
15 |
1 2
|
shjcli |
|- ( A vH B ) e. CH |
16 |
15
|
chssii |
|- ( A vH B ) C_ ~H |
17 |
|
occon |
|- ( ( ( A +H B ) C_ ~H /\ ( A vH B ) C_ ~H ) -> ( ( A +H B ) C_ ( A vH B ) -> ( _|_ ` ( A vH B ) ) C_ ( _|_ ` ( A +H B ) ) ) ) |
18 |
10 16 17
|
mp2an |
|- ( ( A +H B ) C_ ( A vH B ) -> ( _|_ ` ( A vH B ) ) C_ ( _|_ ` ( A +H B ) ) ) |
19 |
14 18
|
ax-mp |
|- ( _|_ ` ( A vH B ) ) C_ ( _|_ ` ( A +H B ) ) |
20 |
|
occl |
|- ( ( A +H B ) C_ ~H -> ( _|_ ` ( A +H B ) ) e. CH ) |
21 |
10 20
|
ax-mp |
|- ( _|_ ` ( A +H B ) ) e. CH |
22 |
15 21
|
chsscon1i |
|- ( ( _|_ ` ( A vH B ) ) C_ ( _|_ ` ( A +H B ) ) <-> ( _|_ ` ( _|_ ` ( A +H B ) ) ) C_ ( A vH B ) ) |
23 |
19 22
|
mpbi |
|- ( _|_ ` ( _|_ ` ( A +H B ) ) ) C_ ( A vH B ) |
24 |
13 23
|
eqssi |
|- ( A vH B ) = ( _|_ ` ( _|_ ` ( A +H B ) ) ) |