Step | Hyp | Ref
| Expression |
1 | | cofuval.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐶) |
2 | | cofuval.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) |
3 | | cofuval.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸)) |
4 | 1, 2, 3 | cofuval 16365 |
. . . 4
⊢ (𝜑 → (𝐺 ∘func 𝐹) = 〈((1st
‘𝐺) ∘
(1st ‘𝐹)),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))〉) |
5 | 4 | fveq2d 6107 |
. . 3
⊢ (𝜑 → (2nd
‘(𝐺
∘func 𝐹)) = (2nd
‘〈((1st ‘𝐺) ∘ (1st ‘𝐹)), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))〉)) |
6 | | fvex 6113 |
. . . . 5
⊢
(1st ‘𝐺) ∈ V |
7 | | fvex 6113 |
. . . . 5
⊢
(1st ‘𝐹) ∈ V |
8 | 6, 7 | coex 7011 |
. . . 4
⊢
((1st ‘𝐺) ∘ (1st ‘𝐹)) ∈ V |
9 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝐶)
∈ V |
10 | 1, 9 | eqeltri 2684 |
. . . . 5
⊢ 𝐵 ∈ V |
11 | 10, 10 | mpt2ex 7136 |
. . . 4
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) ∈ V |
12 | 8, 11 | op2nd 7068 |
. . 3
⊢
(2nd ‘〈((1st ‘𝐺) ∘ (1st ‘𝐹)), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))〉) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) |
13 | 5, 12 | syl6eq 2660 |
. 2
⊢ (𝜑 → (2nd
‘(𝐺
∘func 𝐹)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))) |
14 | | simprl 790 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → 𝑥 = 𝑋) |
15 | 14 | fveq2d 6107 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → ((1st ‘𝐹)‘𝑥) = ((1st ‘𝐹)‘𝑋)) |
16 | | simprr 792 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → 𝑦 = 𝑌) |
17 | 16 | fveq2d 6107 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → ((1st ‘𝐹)‘𝑦) = ((1st ‘𝐹)‘𝑌)) |
18 | 15, 17 | oveq12d 6567 |
. . 3
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → (((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) = (((1st ‘𝐹)‘𝑋)(2nd ‘𝐺)((1st ‘𝐹)‘𝑌))) |
19 | 14, 16 | oveq12d 6567 |
. . 3
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → (𝑥(2nd ‘𝐹)𝑦) = (𝑋(2nd ‘𝐹)𝑌)) |
20 | 18, 19 | coeq12d 5208 |
. 2
⊢ ((𝜑 ∧ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌)) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)) = ((((1st ‘𝐹)‘𝑋)(2nd ‘𝐺)((1st ‘𝐹)‘𝑌)) ∘ (𝑋(2nd ‘𝐹)𝑌))) |
21 | | cofu2nd.x |
. 2
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
22 | | cofu2nd.y |
. 2
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
23 | | ovex 6577 |
. . . 4
⊢
(((1st ‘𝐹)‘𝑋)(2nd ‘𝐺)((1st ‘𝐹)‘𝑌)) ∈ V |
24 | | ovex 6577 |
. . . 4
⊢ (𝑋(2nd ‘𝐹)𝑌) ∈ V |
25 | 23, 24 | coex 7011 |
. . 3
⊢
((((1st ‘𝐹)‘𝑋)(2nd ‘𝐺)((1st ‘𝐹)‘𝑌)) ∘ (𝑋(2nd ‘𝐹)𝑌)) ∈ V |
26 | 25 | a1i 11 |
. 2
⊢ (𝜑 → ((((1st
‘𝐹)‘𝑋)(2nd ‘𝐺)((1st ‘𝐹)‘𝑌)) ∘ (𝑋(2nd ‘𝐹)𝑌)) ∈ V) |
27 | 13, 20, 21, 22, 26 | ovmpt2d 6686 |
1
⊢ (𝜑 → (𝑋(2nd ‘(𝐺 ∘func 𝐹))𝑌) = ((((1st ‘𝐹)‘𝑋)(2nd ‘𝐺)((1st ‘𝐹)‘𝑌)) ∘ (𝑋(2nd ‘𝐹)𝑌))) |