Step | Hyp | Ref
| Expression |
1 | | hofval.m |
. 2
⊢ 𝑀 =
(Hom_{F}‘𝐶) |
2 | | df-hof 16811 |
. . . 4
⊢
Hom_{F} = (𝑐 ∈ Cat ↦
⟨(Hom_{f} ‘𝑐), ⦋(Base‘𝑐) / 𝑏⦌(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝑐)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓))))⟩) |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → Hom_{F} =
(𝑐 ∈ Cat ↦
⟨(Hom_{f} ‘𝑐), ⦋(Base‘𝑐) / 𝑏⦌(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝑐)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓))))⟩)) |
4 | | simpr 477 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 = 𝐶) → 𝑐 = 𝐶) |
5 | 4 | fveq2d 6152 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 = 𝐶) → (Hom_{f}
‘𝑐) =
(Hom_{f} ‘𝐶)) |
6 | | fvex 6158 |
. . . . . 6
⊢
(Base‘𝑐)
∈ V |
7 | 6 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 = 𝐶) → (Base‘𝑐) ∈ V) |
8 | 4 | fveq2d 6152 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 = 𝐶) → (Base‘𝑐) = (Base‘𝐶)) |
9 | | hofval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐶) |
10 | 8, 9 | syl6eqr 2673 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 = 𝐶) → (Base‘𝑐) = 𝐵) |
11 | | simpr 477 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
12 | 11 | sqxpeqd 5101 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵)) |
13 | | simplr 791 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → 𝑐 = 𝐶) |
14 | 13 | fveq2d 6152 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (Hom ‘𝑐) = (Hom ‘𝐶)) |
15 | | hofval.h |
. . . . . . . . 9
⊢ 𝐻 = (Hom ‘𝐶) |
16 | 14, 15 | syl6eqr 2673 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (Hom ‘𝑐) = 𝐻) |
17 | 16 | oveqd 6621 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → ((1^{st} ‘𝑦)(Hom ‘𝑐)(1^{st} ‘𝑥)) = ((1^{st} ‘𝑦)𝐻(1^{st} ‘𝑥))) |
18 | 16 | oveqd 6621 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) = ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦))) |
19 | 16 | fveq1d 6150 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → ((Hom ‘𝑐)‘𝑥) = (𝐻‘𝑥)) |
20 | 13 | fveq2d 6152 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (comp‘𝑐) = (comp‘𝐶)) |
21 | | hofval.o |
. . . . . . . . . . 11
⊢ · =
(comp‘𝐶) |
22 | 20, 21 | syl6eqr 2673 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (comp‘𝑐) = · ) |
23 | 22 | oveqd 6621 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦)) = (⟨(1^{st}
‘𝑦), (1^{st}
‘𝑥)⟩ ·
(2^{nd} ‘𝑦))) |
24 | 22 | oveqd 6621 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑥(comp‘𝑐)(2^{nd} ‘𝑦)) = (𝑥 · (2^{nd}
‘𝑦))) |
25 | 24 | oveqd 6621 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ) = (𝑔(𝑥 · (2^{nd}
‘𝑦))ℎ)) |
26 | | eqidd 2622 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → 𝑓 = 𝑓) |
27 | 23, 25, 26 | oveq123d 6625 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓) = ((𝑔(𝑥 · (2^{nd}
‘𝑦))ℎ)(⟨(1^{st}
‘𝑦), (1^{st}
‘𝑥)⟩ ·
(2^{nd} ‘𝑦))𝑓)) |
28 | 19, 27 | mpteq12dv 4693 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓)) = (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2^{nd}
‘𝑦))ℎ)(⟨(1^{st}
‘𝑦), (1^{st}
‘𝑥)⟩ ·
(2^{nd} ‘𝑦))𝑓))) |
29 | 17, 18, 28 | mpt2eq123dv 6670 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝑐)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓))) = (𝑓 ∈ ((1^{st} ‘𝑦)𝐻(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2^{nd}
‘𝑦))ℎ)(⟨(1^{st}
‘𝑦), (1^{st}
‘𝑥)⟩ ·
(2^{nd} ‘𝑦))𝑓)))) |
30 | 12, 12, 29 | mpt2eq123dv 6670 |
. . . . 5
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝑐)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓)))) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)𝐻(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2^{nd}
‘𝑦))ℎ)(⟨(1^{st}
‘𝑦), (1^{st}
‘𝑥)⟩ ·
(2^{nd} ‘𝑦))𝑓))))) |
31 | 7, 10, 30 | csbied2 3542 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 = 𝐶) → ⦋(Base‘𝑐) / 𝑏⦌(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝑐)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓)))) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)𝐻(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2^{nd}
‘𝑦))ℎ)(⟨(1^{st}
‘𝑦), (1^{st}
‘𝑥)⟩ ·
(2^{nd} ‘𝑦))𝑓))))) |
32 | 5, 31 | opeq12d 4378 |
. . 3
⊢ ((𝜑 ∧ 𝑐 = 𝐶) → ⟨(Hom_{f}
‘𝑐),
⦋(Base‘𝑐) / 𝑏⦌(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝑐)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓))))⟩ = ⟨(Hom_{f}
‘𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)𝐻(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2^{nd}
‘𝑦))ℎ)(⟨(1^{st}
‘𝑦), (1^{st}
‘𝑥)⟩ ·
(2^{nd} ‘𝑦))𝑓))))⟩) |
33 | | hofval.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
34 | | opex 4893 |
. . . 4
⊢
⟨(Hom_{f} ‘𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)𝐻(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2^{nd}
‘𝑦))ℎ)(⟨(1^{st}
‘𝑦), (1^{st}
‘𝑥)⟩ ·
(2^{nd} ‘𝑦))𝑓))))⟩ ∈ V |
35 | 34 | a1i 11 |
. . 3
⊢ (𝜑 →
⟨(Hom_{f} ‘𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)𝐻(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2^{nd}
‘𝑦))ℎ)(⟨(1^{st}
‘𝑦), (1^{st}
‘𝑥)⟩ ·
(2^{nd} ‘𝑦))𝑓))))⟩ ∈ V) |
36 | 3, 32, 33, 35 | fvmptd 6245 |
. 2
⊢ (𝜑 →
(Hom_{F}‘𝐶) = ⟨(Hom_{f}
‘𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)𝐻(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2^{nd}
‘𝑦))ℎ)(⟨(1^{st}
‘𝑦), (1^{st}
‘𝑥)⟩ ·
(2^{nd} ‘𝑦))𝑓))))⟩) |
37 | 1, 36 | syl5eq 2667 |
1
⊢ (𝜑 → 𝑀 = ⟨(Hom_{f}
‘𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)𝐻(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2^{nd}
‘𝑦))ℎ)(⟨(1^{st}
‘𝑦), (1^{st}
‘𝑥)⟩ ·
(2^{nd} ‘𝑦))𝑓))))⟩) |