Step |
Hyp |
Ref |
Expression |
1 |
|
cofuval.b |
⊢ 𝐵 = ( Base ‘ 𝐶 ) |
2 |
|
cofuval.f |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) |
3 |
|
cofuval.g |
⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) ) |
4 |
|
cofu2nd.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
5 |
|
cofu2nd.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝐵 ) |
6 |
|
cofu2.h |
⊢ 𝐻 = ( Hom ‘ 𝐶 ) |
7 |
|
cofu2.y |
⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) ) |
8 |
1 2 3 4 5
|
cofu2nd |
⊢ ( 𝜑 → ( 𝑋 ( 2nd ‘ ( 𝐺 ∘func 𝐹 ) ) 𝑌 ) = ( ( ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ( 2nd ‘ 𝐺 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑌 ) ) ∘ ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ) ) |
9 |
8
|
fveq1d |
⊢ ( 𝜑 → ( ( 𝑋 ( 2nd ‘ ( 𝐺 ∘func 𝐹 ) ) 𝑌 ) ‘ 𝑅 ) = ( ( ( ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ( 2nd ‘ 𝐺 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑌 ) ) ∘ ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ) ‘ 𝑅 ) ) |
10 |
|
eqid |
⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 ) |
11 |
|
relfunc |
⊢ Rel ( 𝐶 Func 𝐷 ) |
12 |
|
1st2ndbr |
⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) ) |
13 |
11 2 12
|
sylancr |
⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) ) |
14 |
1 6 10 13 4 5
|
funcf2 |
⊢ ( 𝜑 → ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑌 ) ) ) |
15 |
|
fvco3 |
⊢ ( ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( ( ( ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ( 2nd ‘ 𝐺 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑌 ) ) ∘ ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ) ‘ 𝑅 ) = ( ( ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ( 2nd ‘ 𝐺 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑌 ) ) ‘ ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ 𝑅 ) ) ) |
16 |
14 7 15
|
syl2anc |
⊢ ( 𝜑 → ( ( ( ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ( 2nd ‘ 𝐺 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑌 ) ) ∘ ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ) ‘ 𝑅 ) = ( ( ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ( 2nd ‘ 𝐺 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑌 ) ) ‘ ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ 𝑅 ) ) ) |
17 |
9 16
|
eqtrd |
⊢ ( 𝜑 → ( ( 𝑋 ( 2nd ‘ ( 𝐺 ∘func 𝐹 ) ) 𝑌 ) ‘ 𝑅 ) = ( ( ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ( 2nd ‘ 𝐺 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑌 ) ) ‘ ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ 𝑅 ) ) ) |