Step |
Hyp |
Ref |
Expression |
1 |
|
sseq2 |
|- ( A = if ( A e. CH , A , ~H ) -> ( B C_ A <-> B C_ if ( A e. CH , A , ~H ) ) ) |
2 |
|
id |
|- ( A = if ( A e. CH , A , ~H ) -> A = if ( A e. CH , A , ~H ) ) |
3 |
|
fveq2 |
|- ( A = if ( A e. CH , A , ~H ) -> ( _|_ ` A ) = ( _|_ ` if ( A e. CH , A , ~H ) ) ) |
4 |
3
|
oveq1d |
|- ( A = if ( A e. CH , A , ~H ) -> ( ( _|_ ` A ) vH B ) = ( ( _|_ ` if ( A e. CH , A , ~H ) ) vH B ) ) |
5 |
2 4
|
ineq12d |
|- ( A = if ( A e. CH , A , ~H ) -> ( A i^i ( ( _|_ ` A ) vH B ) ) = ( if ( A e. CH , A , ~H ) i^i ( ( _|_ ` if ( A e. CH , A , ~H ) ) vH B ) ) ) |
6 |
5
|
eqeq1d |
|- ( A = if ( A e. CH , A , ~H ) -> ( ( A i^i ( ( _|_ ` A ) vH B ) ) = B <-> ( if ( A e. CH , A , ~H ) i^i ( ( _|_ ` if ( A e. CH , A , ~H ) ) vH B ) ) = B ) ) |
7 |
1 6
|
imbi12d |
|- ( A = if ( A e. CH , A , ~H ) -> ( ( B C_ A -> ( A i^i ( ( _|_ ` A ) vH B ) ) = B ) <-> ( B C_ if ( A e. CH , A , ~H ) -> ( if ( A e. CH , A , ~H ) i^i ( ( _|_ ` if ( A e. CH , A , ~H ) ) vH B ) ) = B ) ) ) |
8 |
|
sseq1 |
|- ( B = if ( B e. CH , B , ~H ) -> ( B C_ if ( A e. CH , A , ~H ) <-> if ( B e. CH , B , ~H ) C_ if ( A e. CH , A , ~H ) ) ) |
9 |
|
oveq2 |
|- ( B = if ( B e. CH , B , ~H ) -> ( ( _|_ ` if ( A e. CH , A , ~H ) ) vH B ) = ( ( _|_ ` if ( A e. CH , A , ~H ) ) vH if ( B e. CH , B , ~H ) ) ) |
10 |
9
|
ineq2d |
|- ( B = if ( B e. CH , B , ~H ) -> ( if ( A e. CH , A , ~H ) i^i ( ( _|_ ` if ( A e. CH , A , ~H ) ) vH B ) ) = ( if ( A e. CH , A , ~H ) i^i ( ( _|_ ` if ( A e. CH , A , ~H ) ) vH if ( B e. CH , B , ~H ) ) ) ) |
11 |
|
id |
|- ( B = if ( B e. CH , B , ~H ) -> B = if ( B e. CH , B , ~H ) ) |
12 |
10 11
|
eqeq12d |
|- ( B = if ( B e. CH , B , ~H ) -> ( ( if ( A e. CH , A , ~H ) i^i ( ( _|_ ` if ( A e. CH , A , ~H ) ) vH B ) ) = B <-> ( if ( A e. CH , A , ~H ) i^i ( ( _|_ ` if ( A e. CH , A , ~H ) ) vH if ( B e. CH , B , ~H ) ) ) = if ( B e. CH , B , ~H ) ) ) |
13 |
8 12
|
imbi12d |
|- ( B = if ( B e. CH , B , ~H ) -> ( ( B C_ if ( A e. CH , A , ~H ) -> ( if ( A e. CH , A , ~H ) i^i ( ( _|_ ` if ( A e. CH , A , ~H ) ) vH B ) ) = B ) <-> ( if ( B e. CH , B , ~H ) C_ if ( A e. CH , A , ~H ) -> ( if ( A e. CH , A , ~H ) i^i ( ( _|_ ` if ( A e. CH , A , ~H ) ) vH if ( B e. CH , B , ~H ) ) ) = if ( B e. CH , B , ~H ) ) ) ) |
14 |
|
ifchhv |
|- if ( A e. CH , A , ~H ) e. CH |
15 |
|
ifchhv |
|- if ( B e. CH , B , ~H ) e. CH |
16 |
14 15
|
pjoml3i |
|- ( if ( B e. CH , B , ~H ) C_ if ( A e. CH , A , ~H ) -> ( if ( A e. CH , A , ~H ) i^i ( ( _|_ ` if ( A e. CH , A , ~H ) ) vH if ( B e. CH , B , ~H ) ) ) = if ( B e. CH , B , ~H ) ) |
17 |
7 13 16
|
dedth2h |
|- ( ( A e. CH /\ B e. CH ) -> ( B C_ A -> ( A i^i ( ( _|_ ` A ) vH B ) ) = B ) ) |