Step | Hyp | Ref
| Expression |
1 | | df-bj-end 35224 |
. . 3
⊢ End =
(𝑐 ∈ Cat ↦
(𝑥 ∈ (Base‘𝑐) ↦
{〈(Base‘ndx), (𝑥(Hom ‘𝑐)𝑥)〉, 〈(+g‘ndx),
(〈𝑥, 𝑥〉(comp‘𝑐)𝑥)〉})) |
2 | | fveq2 6722 |
. . . 4
⊢ (𝑐 = 𝐶 → (Base‘𝑐) = (Base‘𝐶)) |
3 | | fveq2 6722 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → (Hom ‘𝑐) = (Hom ‘𝐶)) |
4 | 3 | oveqd 7235 |
. . . . . 6
⊢ (𝑐 = 𝐶 → (𝑥(Hom ‘𝑐)𝑥) = (𝑥(Hom ‘𝐶)𝑥)) |
5 | 4 | opeq2d 4796 |
. . . . 5
⊢ (𝑐 = 𝐶 → 〈(Base‘ndx), (𝑥(Hom ‘𝑐)𝑥)〉 = 〈(Base‘ndx), (𝑥(Hom ‘𝐶)𝑥)〉) |
6 | | fveq2 6722 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → (comp‘𝑐) = (comp‘𝐶)) |
7 | 6 | oveqd 7235 |
. . . . . 6
⊢ (𝑐 = 𝐶 → (〈𝑥, 𝑥〉(comp‘𝑐)𝑥) = (〈𝑥, 𝑥〉(comp‘𝐶)𝑥)) |
8 | 7 | opeq2d 4796 |
. . . . 5
⊢ (𝑐 = 𝐶 → 〈(+g‘ndx),
(〈𝑥, 𝑥〉(comp‘𝑐)𝑥)〉 = 〈(+g‘ndx),
(〈𝑥, 𝑥〉(comp‘𝐶)𝑥)〉) |
9 | 5, 8 | preq12d 4662 |
. . . 4
⊢ (𝑐 = 𝐶 → {〈(Base‘ndx), (𝑥(Hom ‘𝑐)𝑥)〉, 〈(+g‘ndx),
(〈𝑥, 𝑥〉(comp‘𝑐)𝑥)〉} = {〈(Base‘ndx), (𝑥(Hom ‘𝐶)𝑥)〉, 〈(+g‘ndx),
(〈𝑥, 𝑥〉(comp‘𝐶)𝑥)〉}) |
10 | 2, 9 | mpteq12dv 5145 |
. . 3
⊢ (𝑐 = 𝐶 → (𝑥 ∈ (Base‘𝑐) ↦ {〈(Base‘ndx), (𝑥(Hom ‘𝑐)𝑥)〉, 〈(+g‘ndx),
(〈𝑥, 𝑥〉(comp‘𝑐)𝑥)〉}) = (𝑥 ∈ (Base‘𝐶) ↦ {〈(Base‘ndx), (𝑥(Hom ‘𝐶)𝑥)〉, 〈(+g‘ndx),
(〈𝑥, 𝑥〉(comp‘𝐶)𝑥)〉})) |
11 | | bj-endval.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
12 | | fvex 6735 |
. . . . 5
⊢
(Base‘𝐶)
∈ V |
13 | 12 | mptex 7044 |
. . . 4
⊢ (𝑥 ∈ (Base‘𝐶) ↦
{〈(Base‘ndx), (𝑥(Hom ‘𝐶)𝑥)〉, 〈(+g‘ndx),
(〈𝑥, 𝑥〉(comp‘𝐶)𝑥)〉}) ∈ V |
14 | 13 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (Base‘𝐶) ↦ {〈(Base‘ndx), (𝑥(Hom ‘𝐶)𝑥)〉, 〈(+g‘ndx),
(〈𝑥, 𝑥〉(comp‘𝐶)𝑥)〉}) ∈ V) |
15 | 1, 10, 11, 14 | fvmptd3 6846 |
. 2
⊢ (𝜑 → (End ‘𝐶) = (𝑥 ∈ (Base‘𝐶) ↦ {〈(Base‘ndx), (𝑥(Hom ‘𝐶)𝑥)〉, 〈(+g‘ndx),
(〈𝑥, 𝑥〉(comp‘𝐶)𝑥)〉})) |
16 | | id 22 |
. . . . . 6
⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋) |
17 | 16, 16 | oveq12d 7236 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑥(Hom ‘𝐶)𝑥) = (𝑋(Hom ‘𝐶)𝑋)) |
18 | 17 | opeq2d 4796 |
. . . 4
⊢ (𝑥 = 𝑋 → 〈(Base‘ndx), (𝑥(Hom ‘𝐶)𝑥)〉 = 〈(Base‘ndx), (𝑋(Hom ‘𝐶)𝑋)〉) |
19 | 16, 16 | opeq12d 4797 |
. . . . . 6
⊢ (𝑥 = 𝑋 → 〈𝑥, 𝑥〉 = 〈𝑋, 𝑋〉) |
20 | 19, 16 | oveq12d 7236 |
. . . . 5
⊢ (𝑥 = 𝑋 → (〈𝑥, 𝑥〉(comp‘𝐶)𝑥) = (〈𝑋, 𝑋〉(comp‘𝐶)𝑋)) |
21 | 20 | opeq2d 4796 |
. . . 4
⊢ (𝑥 = 𝑋 → 〈(+g‘ndx),
(〈𝑥, 𝑥〉(comp‘𝐶)𝑥)〉 = 〈(+g‘ndx),
(〈𝑋, 𝑋〉(comp‘𝐶)𝑋)〉) |
22 | 18, 21 | preq12d 4662 |
. . 3
⊢ (𝑥 = 𝑋 → {〈(Base‘ndx), (𝑥(Hom ‘𝐶)𝑥)〉, 〈(+g‘ndx),
(〈𝑥, 𝑥〉(comp‘𝐶)𝑥)〉} = {〈(Base‘ndx), (𝑋(Hom ‘𝐶)𝑋)〉, 〈(+g‘ndx),
(〈𝑋, 𝑋〉(comp‘𝐶)𝑋)〉}) |
23 | 22 | adantl 485 |
. 2
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → {〈(Base‘ndx), (𝑥(Hom ‘𝐶)𝑥)〉, 〈(+g‘ndx),
(〈𝑥, 𝑥〉(comp‘𝐶)𝑥)〉} = {〈(Base‘ndx), (𝑋(Hom ‘𝐶)𝑋)〉, 〈(+g‘ndx),
(〈𝑋, 𝑋〉(comp‘𝐶)𝑋)〉}) |
24 | | bj-endval.x |
. 2
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) |
25 | | prex 5330 |
. . 3
⊢
{〈(Base‘ndx), (𝑋(Hom ‘𝐶)𝑋)〉, 〈(+g‘ndx),
(〈𝑋, 𝑋〉(comp‘𝐶)𝑋)〉} ∈ V |
26 | 25 | a1i 11 |
. 2
⊢ (𝜑 → {〈(Base‘ndx),
(𝑋(Hom ‘𝐶)𝑋)〉, 〈(+g‘ndx),
(〈𝑋, 𝑋〉(comp‘𝐶)𝑋)〉} ∈ V) |
27 | 15, 23, 24, 26 | fvmptd 6830 |
1
⊢ (𝜑 → ((End ‘𝐶)‘𝑋) = {〈(Base‘ndx), (𝑋(Hom ‘𝐶)𝑋)〉, 〈(+g‘ndx),
(〈𝑋, 𝑋〉(comp‘𝐶)𝑋)〉}) |