Step |
Hyp |
Ref |
Expression |
1 |
|
sseq2 |
|- ( A = if ( A e. CH , A , 0H ) -> ( B C_ A <-> B C_ if ( A e. CH , A , 0H ) ) ) |
2 |
1
|
notbid |
|- ( A = if ( A e. CH , A , 0H ) -> ( -. B C_ A <-> -. B C_ if ( A e. CH , A , 0H ) ) ) |
3 |
|
id |
|- ( A = if ( A e. CH , A , 0H ) -> A = if ( A e. CH , A , 0H ) ) |
4 |
|
oveq1 |
|- ( A = if ( A e. CH , A , 0H ) -> ( A vH B ) = ( if ( A e. CH , A , 0H ) vH B ) ) |
5 |
3 4
|
psseq12d |
|- ( A = if ( A e. CH , A , 0H ) -> ( A C. ( A vH B ) <-> if ( A e. CH , A , 0H ) C. ( if ( A e. CH , A , 0H ) vH B ) ) ) |
6 |
2 5
|
bibi12d |
|- ( A = if ( A e. CH , A , 0H ) -> ( ( -. B C_ A <-> A C. ( A vH B ) ) <-> ( -. B C_ if ( A e. CH , A , 0H ) <-> if ( A e. CH , A , 0H ) C. ( if ( A e. CH , A , 0H ) vH B ) ) ) ) |
7 |
|
sseq1 |
|- ( B = if ( B e. CH , B , 0H ) -> ( B C_ if ( A e. CH , A , 0H ) <-> if ( B e. CH , B , 0H ) C_ if ( A e. CH , A , 0H ) ) ) |
8 |
7
|
notbid |
|- ( B = if ( B e. CH , B , 0H ) -> ( -. B C_ if ( A e. CH , A , 0H ) <-> -. if ( B e. CH , B , 0H ) C_ if ( A e. CH , A , 0H ) ) ) |
9 |
|
oveq2 |
|- ( B = if ( B e. CH , B , 0H ) -> ( if ( A e. CH , A , 0H ) vH B ) = ( if ( A e. CH , A , 0H ) vH if ( B e. CH , B , 0H ) ) ) |
10 |
9
|
psseq2d |
|- ( B = if ( B e. CH , B , 0H ) -> ( if ( A e. CH , A , 0H ) C. ( if ( A e. CH , A , 0H ) vH B ) <-> if ( A e. CH , A , 0H ) C. ( if ( A e. CH , A , 0H ) vH if ( B e. CH , B , 0H ) ) ) ) |
11 |
8 10
|
bibi12d |
|- ( B = if ( B e. CH , B , 0H ) -> ( ( -. B C_ if ( A e. CH , A , 0H ) <-> if ( A e. CH , A , 0H ) C. ( if ( A e. CH , A , 0H ) vH B ) ) <-> ( -. if ( B e. CH , B , 0H ) C_ if ( A e. CH , A , 0H ) <-> if ( A e. CH , A , 0H ) C. ( if ( A e. CH , A , 0H ) vH if ( B e. CH , B , 0H ) ) ) ) ) |
12 |
|
h0elch |
|- 0H e. CH |
13 |
12
|
elimel |
|- if ( A e. CH , A , 0H ) e. CH |
14 |
12
|
elimel |
|- if ( B e. CH , B , 0H ) e. CH |
15 |
13 14
|
chnlei |
|- ( -. if ( B e. CH , B , 0H ) C_ if ( A e. CH , A , 0H ) <-> if ( A e. CH , A , 0H ) C. ( if ( A e. CH , A , 0H ) vH if ( B e. CH , B , 0H ) ) ) |
16 |
6 11 15
|
dedth2h |
|- ( ( A e. CH /\ B e. CH ) -> ( -. B C_ A <-> A C. ( A vH B ) ) ) |