Step |
Hyp |
Ref |
Expression |
1 |
|
mdsl.1 |
|- A e. CH |
2 |
|
mdsl.2 |
|- B e. CH |
3 |
|
anass |
|- ( ( ( ( A i^i B ) C_ x /\ x C_ ( A vH B ) ) /\ x C_ B ) <-> ( ( A i^i B ) C_ x /\ ( x C_ ( A vH B ) /\ x C_ B ) ) ) |
4 |
2 1
|
chub2i |
|- B C_ ( A vH B ) |
5 |
|
sstr |
|- ( ( x C_ B /\ B C_ ( A vH B ) ) -> x C_ ( A vH B ) ) |
6 |
4 5
|
mpan2 |
|- ( x C_ B -> x C_ ( A vH B ) ) |
7 |
6
|
pm4.71ri |
|- ( x C_ B <-> ( x C_ ( A vH B ) /\ x C_ B ) ) |
8 |
7
|
anbi2i |
|- ( ( ( A i^i B ) C_ x /\ x C_ B ) <-> ( ( A i^i B ) C_ x /\ ( x C_ ( A vH B ) /\ x C_ B ) ) ) |
9 |
3 8
|
bitr4i |
|- ( ( ( ( A i^i B ) C_ x /\ x C_ ( A vH B ) ) /\ x C_ B ) <-> ( ( A i^i B ) C_ x /\ x C_ B ) ) |
10 |
1 2
|
chincli |
|- ( A i^i B ) e. CH |
11 |
|
cvnbtwn4 |
|- ( ( ( A i^i B ) e. CH /\ B e. CH /\ x e. CH ) -> ( ( A i^i B ) ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( x = ( A i^i B ) \/ x = B ) ) ) ) |
12 |
10 2 11
|
mp3an12 |
|- ( x e. CH -> ( ( A i^i B ) ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( x = ( A i^i B ) \/ x = B ) ) ) ) |
13 |
12
|
impcom |
|- ( ( ( A i^i B ) ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( x = ( A i^i B ) \/ x = B ) ) ) |
14 |
10 1
|
chjcomi |
|- ( ( A i^i B ) vH A ) = ( A vH ( A i^i B ) ) |
15 |
1 2
|
chabs1i |
|- ( A vH ( A i^i B ) ) = A |
16 |
14 15
|
eqtri |
|- ( ( A i^i B ) vH A ) = A |
17 |
16
|
ineq1i |
|- ( ( ( A i^i B ) vH A ) i^i B ) = ( A i^i B ) |
18 |
10
|
chjidmi |
|- ( ( A i^i B ) vH ( A i^i B ) ) = ( A i^i B ) |
19 |
17 18
|
eqtr4i |
|- ( ( ( A i^i B ) vH A ) i^i B ) = ( ( A i^i B ) vH ( A i^i B ) ) |
20 |
|
oveq1 |
|- ( x = ( A i^i B ) -> ( x vH A ) = ( ( A i^i B ) vH A ) ) |
21 |
20
|
ineq1d |
|- ( x = ( A i^i B ) -> ( ( x vH A ) i^i B ) = ( ( ( A i^i B ) vH A ) i^i B ) ) |
22 |
|
oveq1 |
|- ( x = ( A i^i B ) -> ( x vH ( A i^i B ) ) = ( ( A i^i B ) vH ( A i^i B ) ) ) |
23 |
19 21 22
|
3eqtr4a |
|- ( x = ( A i^i B ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) |
24 |
|
incom |
|- ( ( B vH A ) i^i B ) = ( B i^i ( B vH A ) ) |
25 |
2 1
|
chabs2i |
|- ( B i^i ( B vH A ) ) = B |
26 |
2 1
|
chabs1i |
|- ( B vH ( B i^i A ) ) = B |
27 |
|
incom |
|- ( B i^i A ) = ( A i^i B ) |
28 |
27
|
oveq2i |
|- ( B vH ( B i^i A ) ) = ( B vH ( A i^i B ) ) |
29 |
25 26 28
|
3eqtr2i |
|- ( B i^i ( B vH A ) ) = ( B vH ( A i^i B ) ) |
30 |
24 29
|
eqtri |
|- ( ( B vH A ) i^i B ) = ( B vH ( A i^i B ) ) |
31 |
|
oveq1 |
|- ( x = B -> ( x vH A ) = ( B vH A ) ) |
32 |
31
|
ineq1d |
|- ( x = B -> ( ( x vH A ) i^i B ) = ( ( B vH A ) i^i B ) ) |
33 |
|
oveq1 |
|- ( x = B -> ( x vH ( A i^i B ) ) = ( B vH ( A i^i B ) ) ) |
34 |
30 32 33
|
3eqtr4a |
|- ( x = B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) |
35 |
23 34
|
jaoi |
|- ( ( x = ( A i^i B ) \/ x = B ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) |
36 |
13 35
|
syl6 |
|- ( ( ( A i^i B ) ( ( ( A i^i B ) C_ x /\ x C_ B ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) |
37 |
9 36
|
syl5bi |
|- ( ( ( A i^i B ) ( ( ( ( A i^i B ) C_ x /\ x C_ ( A vH B ) ) /\ x C_ B ) -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) |
38 |
37
|
exp4b |
|- ( ( A i^i B ) ( x e. CH -> ( ( ( A i^i B ) C_ x /\ x C_ ( A vH B ) ) -> ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) ) ) |
39 |
38
|
ralrimiv |
|- ( ( A i^i B ) A. x e. CH ( ( ( A i^i B ) C_ x /\ x C_ ( A vH B ) ) -> ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) ) |
40 |
1 2
|
mdsl1i |
|- ( A. x e. CH ( ( ( A i^i B ) C_ x /\ x C_ ( A vH B ) ) -> ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) <-> A MH B ) |
41 |
39 40
|
sylib |
|- ( ( A i^i B ) A MH B ) |