Step |
Hyp |
Ref |
Expression |
1 |
|
sseq1 |
|- ( A = if ( A e. CH , A , 0H ) -> ( A C_ B <-> if ( A e. CH , A , 0H ) C_ B ) ) |
2 |
|
fveq2 |
|- ( A = if ( A e. CH , A , 0H ) -> ( _|_ ` A ) = ( _|_ ` if ( A e. CH , A , 0H ) ) ) |
3 |
2
|
ineq2d |
|- ( A = if ( A e. CH , A , 0H ) -> ( B i^i ( _|_ ` A ) ) = ( B i^i ( _|_ ` if ( A e. CH , A , 0H ) ) ) ) |
4 |
3
|
eqeq1d |
|- ( A = if ( A e. CH , A , 0H ) -> ( ( B i^i ( _|_ ` A ) ) = 0H <-> ( B i^i ( _|_ ` if ( A e. CH , A , 0H ) ) ) = 0H ) ) |
5 |
1 4
|
anbi12d |
|- ( A = if ( A e. CH , A , 0H ) -> ( ( A C_ B /\ ( B i^i ( _|_ ` A ) ) = 0H ) <-> ( if ( A e. CH , A , 0H ) C_ B /\ ( B i^i ( _|_ ` if ( A e. CH , A , 0H ) ) ) = 0H ) ) ) |
6 |
|
eqeq1 |
|- ( A = if ( A e. CH , A , 0H ) -> ( A = B <-> if ( A e. CH , A , 0H ) = B ) ) |
7 |
5 6
|
imbi12d |
|- ( A = if ( A e. CH , A , 0H ) -> ( ( ( A C_ B /\ ( B i^i ( _|_ ` A ) ) = 0H ) -> A = B ) <-> ( ( if ( A e. CH , A , 0H ) C_ B /\ ( B i^i ( _|_ ` if ( A e. CH , A , 0H ) ) ) = 0H ) -> if ( A e. CH , A , 0H ) = B ) ) ) |
8 |
|
sseq2 |
|- ( B = if ( B e. SH , B , 0H ) -> ( if ( A e. CH , A , 0H ) C_ B <-> if ( A e. CH , A , 0H ) C_ if ( B e. SH , B , 0H ) ) ) |
9 |
|
ineq1 |
|- ( B = if ( B e. SH , B , 0H ) -> ( B i^i ( _|_ ` if ( A e. CH , A , 0H ) ) ) = ( if ( B e. SH , B , 0H ) i^i ( _|_ ` if ( A e. CH , A , 0H ) ) ) ) |
10 |
9
|
eqeq1d |
|- ( B = if ( B e. SH , B , 0H ) -> ( ( B i^i ( _|_ ` if ( A e. CH , A , 0H ) ) ) = 0H <-> ( if ( B e. SH , B , 0H ) i^i ( _|_ ` if ( A e. CH , A , 0H ) ) ) = 0H ) ) |
11 |
8 10
|
anbi12d |
|- ( B = if ( B e. SH , B , 0H ) -> ( ( if ( A e. CH , A , 0H ) C_ B /\ ( B i^i ( _|_ ` if ( A e. CH , A , 0H ) ) ) = 0H ) <-> ( if ( A e. CH , A , 0H ) C_ if ( B e. SH , B , 0H ) /\ ( if ( B e. SH , B , 0H ) i^i ( _|_ ` if ( A e. CH , A , 0H ) ) ) = 0H ) ) ) |
12 |
|
eqeq2 |
|- ( B = if ( B e. SH , B , 0H ) -> ( if ( A e. CH , A , 0H ) = B <-> if ( A e. CH , A , 0H ) = if ( B e. SH , B , 0H ) ) ) |
13 |
11 12
|
imbi12d |
|- ( B = if ( B e. SH , B , 0H ) -> ( ( ( if ( A e. CH , A , 0H ) C_ B /\ ( B i^i ( _|_ ` if ( A e. CH , A , 0H ) ) ) = 0H ) -> if ( A e. CH , A , 0H ) = B ) <-> ( ( if ( A e. CH , A , 0H ) C_ if ( B e. SH , B , 0H ) /\ ( if ( B e. SH , B , 0H ) i^i ( _|_ ` if ( A e. CH , A , 0H ) ) ) = 0H ) -> if ( A e. CH , A , 0H ) = if ( B e. SH , B , 0H ) ) ) ) |
14 |
|
h0elch |
|- 0H e. CH |
15 |
14
|
elimel |
|- if ( A e. CH , A , 0H ) e. CH |
16 |
|
h0elsh |
|- 0H e. SH |
17 |
16
|
elimel |
|- if ( B e. SH , B , 0H ) e. SH |
18 |
15 17
|
pjomli |
|- ( ( if ( A e. CH , A , 0H ) C_ if ( B e. SH , B , 0H ) /\ ( if ( B e. SH , B , 0H ) i^i ( _|_ ` if ( A e. CH , A , 0H ) ) ) = 0H ) -> if ( A e. CH , A , 0H ) = if ( B e. SH , B , 0H ) ) |
19 |
7 13 18
|
dedth2h |
|- ( ( A e. CH /\ B e. SH ) -> ( ( A C_ B /\ ( B i^i ( _|_ ` A ) ) = 0H ) -> A = B ) ) |
20 |
19
|
imp |
|- ( ( ( A e. CH /\ B e. SH ) /\ ( A C_ B /\ ( B i^i ( _|_ ` A ) ) = 0H ) ) -> A = B ) |