Step |
Hyp |
Ref |
Expression |
1 |
|
unss |
|- ( ( A C_ C /\ B C_ C ) <-> ( A u. B ) C_ C ) |
2 |
|
simp1 |
|- ( ( A e. SH /\ B e. SH /\ C e. CH ) -> A e. SH ) |
3 |
|
shss |
|- ( A e. SH -> A C_ ~H ) |
4 |
2 3
|
syl |
|- ( ( A e. SH /\ B e. SH /\ C e. CH ) -> A C_ ~H ) |
5 |
|
simp2 |
|- ( ( A e. SH /\ B e. SH /\ C e. CH ) -> B e. SH ) |
6 |
|
shss |
|- ( B e. SH -> B C_ ~H ) |
7 |
5 6
|
syl |
|- ( ( A e. SH /\ B e. SH /\ C e. CH ) -> B C_ ~H ) |
8 |
4 7
|
unssd |
|- ( ( A e. SH /\ B e. SH /\ C e. CH ) -> ( A u. B ) C_ ~H ) |
9 |
|
chss |
|- ( C e. CH -> C C_ ~H ) |
10 |
9
|
3ad2ant3 |
|- ( ( A e. SH /\ B e. SH /\ C e. CH ) -> C C_ ~H ) |
11 |
|
occon2 |
|- ( ( ( A u. B ) C_ ~H /\ C C_ ~H ) -> ( ( A u. B ) C_ C -> ( _|_ ` ( _|_ ` ( A u. B ) ) ) C_ ( _|_ ` ( _|_ ` C ) ) ) ) |
12 |
8 10 11
|
syl2anc |
|- ( ( A e. SH /\ B e. SH /\ C e. CH ) -> ( ( A u. B ) C_ C -> ( _|_ ` ( _|_ ` ( A u. B ) ) ) C_ ( _|_ ` ( _|_ ` C ) ) ) ) |
13 |
1 12
|
syl5bi |
|- ( ( A e. SH /\ B e. SH /\ C e. CH ) -> ( ( A C_ C /\ B C_ C ) -> ( _|_ ` ( _|_ ` ( A u. B ) ) ) C_ ( _|_ ` ( _|_ ` C ) ) ) ) |
14 |
|
shjval |
|- ( ( A e. SH /\ B e. SH ) -> ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) ) |
15 |
2 5 14
|
syl2anc |
|- ( ( A e. SH /\ B e. SH /\ C e. CH ) -> ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) ) |
16 |
|
ococ |
|- ( C e. CH -> ( _|_ ` ( _|_ ` C ) ) = C ) |
17 |
16
|
3ad2ant3 |
|- ( ( A e. SH /\ B e. SH /\ C e. CH ) -> ( _|_ ` ( _|_ ` C ) ) = C ) |
18 |
17
|
eqcomd |
|- ( ( A e. SH /\ B e. SH /\ C e. CH ) -> C = ( _|_ ` ( _|_ ` C ) ) ) |
19 |
15 18
|
sseq12d |
|- ( ( A e. SH /\ B e. SH /\ C e. CH ) -> ( ( A vH B ) C_ C <-> ( _|_ ` ( _|_ ` ( A u. B ) ) ) C_ ( _|_ ` ( _|_ ` C ) ) ) ) |
20 |
13 19
|
sylibrd |
|- ( ( A e. SH /\ B e. SH /\ C e. CH ) -> ( ( A C_ C /\ B C_ C ) -> ( A vH B ) C_ C ) ) |
21 |
|
shub1 |
|- ( ( A e. SH /\ B e. SH ) -> A C_ ( A vH B ) ) |
22 |
2 5 21
|
syl2anc |
|- ( ( A e. SH /\ B e. SH /\ C e. CH ) -> A C_ ( A vH B ) ) |
23 |
|
sstr |
|- ( ( A C_ ( A vH B ) /\ ( A vH B ) C_ C ) -> A C_ C ) |
24 |
22 23
|
sylan |
|- ( ( ( A e. SH /\ B e. SH /\ C e. CH ) /\ ( A vH B ) C_ C ) -> A C_ C ) |
25 |
|
shub2 |
|- ( ( B e. SH /\ A e. SH ) -> B C_ ( A vH B ) ) |
26 |
5 2 25
|
syl2anc |
|- ( ( A e. SH /\ B e. SH /\ C e. CH ) -> B C_ ( A vH B ) ) |
27 |
|
sstr |
|- ( ( B C_ ( A vH B ) /\ ( A vH B ) C_ C ) -> B C_ C ) |
28 |
26 27
|
sylan |
|- ( ( ( A e. SH /\ B e. SH /\ C e. CH ) /\ ( A vH B ) C_ C ) -> B C_ C ) |
29 |
24 28
|
jca |
|- ( ( ( A e. SH /\ B e. SH /\ C e. CH ) /\ ( A vH B ) C_ C ) -> ( A C_ C /\ B C_ C ) ) |
30 |
29
|
ex |
|- ( ( A e. SH /\ B e. SH /\ C e. CH ) -> ( ( A vH B ) C_ C -> ( A C_ C /\ B C_ C ) ) ) |
31 |
20 30
|
impbid |
|- ( ( A e. SH /\ B e. SH /\ C e. CH ) -> ( ( A C_ C /\ B C_ C ) <-> ( A vH B ) C_ C ) ) |