Step | Hyp | Ref
| Expression |
1 | | cofuval2.b |
. . 3
⊢ 𝐵 = (Base‘𝐶) |
2 | | cofuval2.f |
. . . 4
⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) |
3 | | df-br 5107 |
. . . 4
⊢ (𝐹(𝐶 Func 𝐷)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷)) |
4 | 2, 3 | sylib 217 |
. . 3
⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷)) |
5 | | cofuval2.x |
. . . 4
⊢ (𝜑 → 𝐻(𝐷 Func 𝐸)𝐾) |
6 | | df-br 5107 |
. . . 4
⊢ (𝐻(𝐷 Func 𝐸)𝐾 ↔ ⟨𝐻, 𝐾⟩ ∈ (𝐷 Func 𝐸)) |
7 | 5, 6 | sylib 217 |
. . 3
⊢ (𝜑 → ⟨𝐻, 𝐾⟩ ∈ (𝐷 Func 𝐸)) |
8 | 1, 4, 7 | cofuval 17773 |
. 2
⊢ (𝜑 → (⟨𝐻, 𝐾⟩ ∘func
⟨𝐹, 𝐺⟩) = ⟨((1st
‘⟨𝐻, 𝐾⟩) ∘ (1st
‘⟨𝐹, 𝐺⟩)), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((((1st
‘⟨𝐹, 𝐺⟩)‘𝑥)(2nd ‘⟨𝐻, 𝐾⟩)((1st ‘⟨𝐹, 𝐺⟩)‘𝑦)) ∘ (𝑥(2nd ‘⟨𝐹, 𝐺⟩)𝑦)))⟩) |
9 | | relfunc 17753 |
. . . . . 6
⊢ Rel
(𝐷 Func 𝐸) |
10 | | brrelex12 5685 |
. . . . . 6
⊢ ((Rel
(𝐷 Func 𝐸) ∧ 𝐻(𝐷 Func 𝐸)𝐾) → (𝐻 ∈ V ∧ 𝐾 ∈ V)) |
11 | 9, 5, 10 | sylancr 588 |
. . . . 5
⊢ (𝜑 → (𝐻 ∈ V ∧ 𝐾 ∈ V)) |
12 | | op1stg 7934 |
. . . . 5
⊢ ((𝐻 ∈ V ∧ 𝐾 ∈ V) →
(1st ‘⟨𝐻, 𝐾⟩) = 𝐻) |
13 | 11, 12 | syl 17 |
. . . 4
⊢ (𝜑 → (1st
‘⟨𝐻, 𝐾⟩) = 𝐻) |
14 | | relfunc 17753 |
. . . . . 6
⊢ Rel
(𝐶 Func 𝐷) |
15 | | brrelex12 5685 |
. . . . . 6
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐹(𝐶 Func 𝐷)𝐺) → (𝐹 ∈ V ∧ 𝐺 ∈ V)) |
16 | 14, 2, 15 | sylancr 588 |
. . . . 5
⊢ (𝜑 → (𝐹 ∈ V ∧ 𝐺 ∈ V)) |
17 | | op1stg 7934 |
. . . . 5
⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) →
(1st ‘⟨𝐹, 𝐺⟩) = 𝐹) |
18 | 16, 17 | syl 17 |
. . . 4
⊢ (𝜑 → (1st
‘⟨𝐹, 𝐺⟩) = 𝐹) |
19 | 13, 18 | coeq12d 5821 |
. . 3
⊢ (𝜑 → ((1st
‘⟨𝐻, 𝐾⟩) ∘ (1st
‘⟨𝐹, 𝐺⟩)) = (𝐻 ∘ 𝐹)) |
20 | | op2ndg 7935 |
. . . . . . . 8
⊢ ((𝐻 ∈ V ∧ 𝐾 ∈ V) →
(2nd ‘⟨𝐻, 𝐾⟩) = 𝐾) |
21 | 11, 20 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (2nd
‘⟨𝐻, 𝐾⟩) = 𝐾) |
22 | 21 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (2nd ‘⟨𝐻, 𝐾⟩) = 𝐾) |
23 | 18 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (1st ‘⟨𝐹, 𝐺⟩) = 𝐹) |
24 | 23 | fveq1d 6845 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((1st ‘⟨𝐹, 𝐺⟩)‘𝑥) = (𝐹‘𝑥)) |
25 | 23 | fveq1d 6845 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((1st ‘⟨𝐹, 𝐺⟩)‘𝑦) = (𝐹‘𝑦)) |
26 | 22, 24, 25 | oveq123d 7379 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (((1st
‘⟨𝐹, 𝐺⟩)‘𝑥)(2nd ‘⟨𝐻, 𝐾⟩)((1st ‘⟨𝐹, 𝐺⟩)‘𝑦)) = ((𝐹‘𝑥)𝐾(𝐹‘𝑦))) |
27 | | op2ndg 7935 |
. . . . . . . 8
⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) →
(2nd ‘⟨𝐹, 𝐺⟩) = 𝐺) |
28 | 16, 27 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (2nd
‘⟨𝐹, 𝐺⟩) = 𝐺) |
29 | 28 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (2nd ‘⟨𝐹, 𝐺⟩) = 𝐺) |
30 | 29 | oveqd 7375 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(2nd ‘⟨𝐹, 𝐺⟩)𝑦) = (𝑥𝐺𝑦)) |
31 | 26, 30 | coeq12d 5821 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((((1st
‘⟨𝐹, 𝐺⟩)‘𝑥)(2nd ‘⟨𝐻, 𝐾⟩)((1st ‘⟨𝐹, 𝐺⟩)‘𝑦)) ∘ (𝑥(2nd ‘⟨𝐹, 𝐺⟩)𝑦)) = (((𝐹‘𝑥)𝐾(𝐹‘𝑦)) ∘ (𝑥𝐺𝑦))) |
32 | 31 | mpoeq3dva 7435 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((((1st
‘⟨𝐹, 𝐺⟩)‘𝑥)(2nd ‘⟨𝐻, 𝐾⟩)((1st ‘⟨𝐹, 𝐺⟩)‘𝑦)) ∘ (𝑥(2nd ‘⟨𝐹, 𝐺⟩)𝑦))) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (((𝐹‘𝑥)𝐾(𝐹‘𝑦)) ∘ (𝑥𝐺𝑦)))) |
33 | 19, 32 | opeq12d 4839 |
. 2
⊢ (𝜑 → ⟨((1st
‘⟨𝐻, 𝐾⟩) ∘ (1st
‘⟨𝐹, 𝐺⟩)), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((((1st
‘⟨𝐹, 𝐺⟩)‘𝑥)(2nd ‘⟨𝐻, 𝐾⟩)((1st ‘⟨𝐹, 𝐺⟩)‘𝑦)) ∘ (𝑥(2nd ‘⟨𝐹, 𝐺⟩)𝑦)))⟩ = ⟨(𝐻 ∘ 𝐹), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (((𝐹‘𝑥)𝐾(𝐹‘𝑦)) ∘ (𝑥𝐺𝑦)))⟩) |
34 | 8, 33 | eqtrd 2773 |
1
⊢ (𝜑 → (⟨𝐻, 𝐾⟩ ∘func
⟨𝐹, 𝐺⟩) = ⟨(𝐻 ∘ 𝐹), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (((𝐹‘𝑥)𝐾(𝐹‘𝑦)) ∘ (𝑥𝐺𝑦)))⟩) |