Step |
Hyp |
Ref |
Expression |
1 |
|
cofuval.b |
⊢ 𝐵 = ( Base ‘ 𝐶 ) |
2 |
|
cofuval.f |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) |
3 |
|
cofuval.g |
⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) ) |
4 |
1 2 3
|
cofuval |
⊢ ( 𝜑 → ( 𝐺 ∘func 𝐹 ) = 〈 ( ( 1st ‘ 𝐺 ) ∘ ( 1st ‘ 𝐹 ) ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ( 2nd ‘ 𝐺 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ) ) 〉 ) |
5 |
4
|
fveq2d |
⊢ ( 𝜑 → ( 1st ‘ ( 𝐺 ∘func 𝐹 ) ) = ( 1st ‘ 〈 ( ( 1st ‘ 𝐺 ) ∘ ( 1st ‘ 𝐹 ) ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ( 2nd ‘ 𝐺 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ) ) 〉 ) ) |
6 |
|
fvex |
⊢ ( 1st ‘ 𝐺 ) ∈ V |
7 |
|
fvex |
⊢ ( 1st ‘ 𝐹 ) ∈ V |
8 |
6 7
|
coex |
⊢ ( ( 1st ‘ 𝐺 ) ∘ ( 1st ‘ 𝐹 ) ) ∈ V |
9 |
1
|
fvexi |
⊢ 𝐵 ∈ V |
10 |
9 9
|
mpoex |
⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ( 2nd ‘ 𝐺 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ) ) ∈ V |
11 |
8 10
|
op1st |
⊢ ( 1st ‘ 〈 ( ( 1st ‘ 𝐺 ) ∘ ( 1st ‘ 𝐹 ) ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ( 2nd ‘ 𝐺 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ) ) 〉 ) = ( ( 1st ‘ 𝐺 ) ∘ ( 1st ‘ 𝐹 ) ) |
12 |
5 11
|
eqtrdi |
⊢ ( 𝜑 → ( 1st ‘ ( 𝐺 ∘func 𝐹 ) ) = ( ( 1st ‘ 𝐺 ) ∘ ( 1st ‘ 𝐹 ) ) ) |