Step |
Hyp |
Ref |
Expression |
1 |
|
fveq2 |
|- ( H = if ( H e. CH , H , 0H ) -> ( projh ` H ) = ( projh ` if ( H e. CH , H , 0H ) ) ) |
2 |
|
foeq1 |
|- ( ( projh ` H ) = ( projh ` if ( H e. CH , H , 0H ) ) -> ( ( projh ` H ) : ~H -onto-> H <-> ( projh ` if ( H e. CH , H , 0H ) ) : ~H -onto-> H ) ) |
3 |
1 2
|
syl |
|- ( H = if ( H e. CH , H , 0H ) -> ( ( projh ` H ) : ~H -onto-> H <-> ( projh ` if ( H e. CH , H , 0H ) ) : ~H -onto-> H ) ) |
4 |
|
foeq3 |
|- ( H = if ( H e. CH , H , 0H ) -> ( ( projh ` if ( H e. CH , H , 0H ) ) : ~H -onto-> H <-> ( projh ` if ( H e. CH , H , 0H ) ) : ~H -onto-> if ( H e. CH , H , 0H ) ) ) |
5 |
|
h0elch |
|- 0H e. CH |
6 |
5
|
elimel |
|- if ( H e. CH , H , 0H ) e. CH |
7 |
6
|
pjfoi |
|- ( projh ` if ( H e. CH , H , 0H ) ) : ~H -onto-> if ( H e. CH , H , 0H ) |
8 |
3 4 7
|
dedth2v |
|- ( H e. CH -> ( projh ` H ) : ~H -onto-> H ) |