Step |
Hyp |
Ref |
Expression |
1 |
|
fveq2 |
⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) → ( projℎ ‘ 𝐻 ) = ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ) |
2 |
|
foeq1 |
⊢ ( ( projℎ ‘ 𝐻 ) = ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) → ( ( projℎ ‘ 𝐻 ) : ℋ –onto→ 𝐻 ↔ ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) : ℋ –onto→ 𝐻 ) ) |
3 |
1 2
|
syl |
⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) → ( ( projℎ ‘ 𝐻 ) : ℋ –onto→ 𝐻 ↔ ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) : ℋ –onto→ 𝐻 ) ) |
4 |
|
foeq3 |
⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) → ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) : ℋ –onto→ 𝐻 ↔ ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) : ℋ –onto→ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ) |
5 |
|
h0elch |
⊢ 0ℋ ∈ Cℋ |
6 |
5
|
elimel |
⊢ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ∈ Cℋ |
7 |
6
|
pjfoi |
⊢ ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) : ℋ –onto→ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) |
8 |
3 4 7
|
dedth2v |
⊢ ( 𝐻 ∈ Cℋ → ( projℎ ‘ 𝐻 ) : ℋ –onto→ 𝐻 ) |