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 |
|
eqeq1 |
|- ( A = if ( A e. CH , A , 0H ) -> ( A = ( _|_ ` ( _|_ ` { B } ) ) <-> if ( A e. CH , A , 0H ) = ( _|_ ` ( _|_ ` { B } ) ) ) ) |
3 |
|
eqeq1 |
|- ( A = if ( A e. CH , A , 0H ) -> ( A = 0H <-> if ( A e. CH , A , 0H ) = 0H ) ) |
4 |
2 3
|
orbi12d |
|- ( A = if ( A e. CH , A , 0H ) -> ( ( A = ( _|_ ` ( _|_ ` { B } ) ) \/ A = 0H ) <-> ( if ( A e. CH , A , 0H ) = ( _|_ ` ( _|_ ` { B } ) ) \/ if ( A e. CH , A , 0H ) = 0H ) ) ) |
5 |
1 4
|
imbi12d |
|- ( A = if ( A e. CH , A , 0H ) -> ( ( A C_ ( _|_ ` ( _|_ ` { B } ) ) -> ( A = ( _|_ ` ( _|_ ` { B } ) ) \/ A = 0H ) ) <-> ( if ( A e. CH , A , 0H ) C_ ( _|_ ` ( _|_ ` { B } ) ) -> ( if ( A e. CH , A , 0H ) = ( _|_ ` ( _|_ ` { B } ) ) \/ if ( A e. CH , A , 0H ) = 0H ) ) ) ) |
6 |
|
sneq |
|- ( B = if ( B e. ~H , B , 0h ) -> { B } = { if ( B e. ~H , B , 0h ) } ) |
7 |
6
|
fveq2d |
|- ( B = if ( B e. ~H , B , 0h ) -> ( _|_ ` { B } ) = ( _|_ ` { if ( B e. ~H , B , 0h ) } ) ) |
8 |
7
|
fveq2d |
|- ( B = if ( B e. ~H , B , 0h ) -> ( _|_ ` ( _|_ ` { B } ) ) = ( _|_ ` ( _|_ ` { if ( B e. ~H , B , 0h ) } ) ) ) |
9 |
8
|
sseq2d |
|- ( B = if ( B e. ~H , B , 0h ) -> ( if ( A e. CH , A , 0H ) C_ ( _|_ ` ( _|_ ` { B } ) ) <-> if ( A e. CH , A , 0H ) C_ ( _|_ ` ( _|_ ` { if ( B e. ~H , B , 0h ) } ) ) ) ) |
10 |
8
|
eqeq2d |
|- ( B = if ( B e. ~H , B , 0h ) -> ( if ( A e. CH , A , 0H ) = ( _|_ ` ( _|_ ` { B } ) ) <-> if ( A e. CH , A , 0H ) = ( _|_ ` ( _|_ ` { if ( B e. ~H , B , 0h ) } ) ) ) ) |
11 |
10
|
orbi1d |
|- ( B = if ( B e. ~H , B , 0h ) -> ( ( if ( A e. CH , A , 0H ) = ( _|_ ` ( _|_ ` { B } ) ) \/ if ( A e. CH , A , 0H ) = 0H ) <-> ( if ( A e. CH , A , 0H ) = ( _|_ ` ( _|_ ` { if ( B e. ~H , B , 0h ) } ) ) \/ if ( A e. CH , A , 0H ) = 0H ) ) ) |
12 |
9 11
|
imbi12d |
|- ( B = if ( B e. ~H , B , 0h ) -> ( ( if ( A e. CH , A , 0H ) C_ ( _|_ ` ( _|_ ` { B } ) ) -> ( if ( A e. CH , A , 0H ) = ( _|_ ` ( _|_ ` { B } ) ) \/ if ( A e. CH , A , 0H ) = 0H ) ) <-> ( if ( A e. CH , A , 0H ) C_ ( _|_ ` ( _|_ ` { if ( B e. ~H , B , 0h ) } ) ) -> ( if ( A e. CH , A , 0H ) = ( _|_ ` ( _|_ ` { if ( B e. ~H , B , 0h ) } ) ) \/ if ( A e. CH , A , 0H ) = 0H ) ) ) ) |
13 |
|
h0elch |
|- 0H e. CH |
14 |
13
|
elimel |
|- if ( A e. CH , A , 0H ) e. CH |
15 |
|
ifhvhv0 |
|- if ( B e. ~H , B , 0h ) e. ~H |
16 |
14 15
|
h1datomi |
|- ( if ( A e. CH , A , 0H ) C_ ( _|_ ` ( _|_ ` { if ( B e. ~H , B , 0h ) } ) ) -> ( if ( A e. CH , A , 0H ) = ( _|_ ` ( _|_ ` { if ( B e. ~H , B , 0h ) } ) ) \/ if ( A e. CH , A , 0H ) = 0H ) ) |
17 |
5 12 16
|
dedth2h |
|- ( ( A e. CH /\ B e. ~H ) -> ( A C_ ( _|_ ` ( _|_ ` { B } ) ) -> ( A = ( _|_ ` ( _|_ ` { B } ) ) \/ A = 0H ) ) ) |