Step |
Hyp |
Ref |
Expression |
1 |
|
pjoml2.1 |
|- A e. CH |
2 |
|
pjoml2.2 |
|- B e. CH |
3 |
|
inss2 |
|- ( ( _|_ ` A ) i^i B ) C_ B |
4 |
1
|
choccli |
|- ( _|_ ` A ) e. CH |
5 |
4 2
|
chincli |
|- ( ( _|_ ` A ) i^i B ) e. CH |
6 |
1 5 2
|
chlubii |
|- ( ( A C_ B /\ ( ( _|_ ` A ) i^i B ) C_ B ) -> ( A vH ( ( _|_ ` A ) i^i B ) ) C_ B ) |
7 |
3 6
|
mpan2 |
|- ( A C_ B -> ( A vH ( ( _|_ ` A ) i^i B ) ) C_ B ) |
8 |
1 5
|
chdmj1i |
|- ( _|_ ` ( A vH ( ( _|_ ` A ) i^i B ) ) ) = ( ( _|_ ` A ) i^i ( _|_ ` ( ( _|_ ` A ) i^i B ) ) ) |
9 |
8
|
ineq2i |
|- ( B i^i ( _|_ ` ( A vH ( ( _|_ ` A ) i^i B ) ) ) ) = ( B i^i ( ( _|_ ` A ) i^i ( _|_ ` ( ( _|_ ` A ) i^i B ) ) ) ) |
10 |
|
incom |
|- ( B i^i ( _|_ ` A ) ) = ( ( _|_ ` A ) i^i B ) |
11 |
10
|
ineq1i |
|- ( ( B i^i ( _|_ ` A ) ) i^i ( _|_ ` ( ( _|_ ` A ) i^i B ) ) ) = ( ( ( _|_ ` A ) i^i B ) i^i ( _|_ ` ( ( _|_ ` A ) i^i B ) ) ) |
12 |
|
inass |
|- ( ( B i^i ( _|_ ` A ) ) i^i ( _|_ ` ( ( _|_ ` A ) i^i B ) ) ) = ( B i^i ( ( _|_ ` A ) i^i ( _|_ ` ( ( _|_ ` A ) i^i B ) ) ) ) |
13 |
5
|
chocini |
|- ( ( ( _|_ ` A ) i^i B ) i^i ( _|_ ` ( ( _|_ ` A ) i^i B ) ) ) = 0H |
14 |
11 12 13
|
3eqtr3i |
|- ( B i^i ( ( _|_ ` A ) i^i ( _|_ ` ( ( _|_ ` A ) i^i B ) ) ) ) = 0H |
15 |
9 14
|
eqtri |
|- ( B i^i ( _|_ ` ( A vH ( ( _|_ ` A ) i^i B ) ) ) ) = 0H |
16 |
1 5
|
chjcli |
|- ( A vH ( ( _|_ ` A ) i^i B ) ) e. CH |
17 |
2
|
chshii |
|- B e. SH |
18 |
16 17
|
pjomli |
|- ( ( ( A vH ( ( _|_ ` A ) i^i B ) ) C_ B /\ ( B i^i ( _|_ ` ( A vH ( ( _|_ ` A ) i^i B ) ) ) ) = 0H ) -> ( A vH ( ( _|_ ` A ) i^i B ) ) = B ) |
19 |
7 15 18
|
sylancl |
|- ( A C_ B -> ( A vH ( ( _|_ ` A ) i^i B ) ) = B ) |