Step | Hyp | Ref
| Expression |
1 | | df-bj-end 36195 |
. . 3
β’ End =
(π β Cat β¦
(π₯ β (Baseβπ) β¦
{β¨(Baseβndx), (π₯(Hom βπ)π₯)β©, β¨(+gβndx),
(β¨π₯, π₯β©(compβπ)π₯)β©})) |
2 | | fveq2 6892 |
. . . 4
β’ (π = πΆ β (Baseβπ) = (BaseβπΆ)) |
3 | | fveq2 6892 |
. . . . . . 7
β’ (π = πΆ β (Hom βπ) = (Hom βπΆ)) |
4 | 3 | oveqd 7426 |
. . . . . 6
β’ (π = πΆ β (π₯(Hom βπ)π₯) = (π₯(Hom βπΆ)π₯)) |
5 | 4 | opeq2d 4881 |
. . . . 5
β’ (π = πΆ β β¨(Baseβndx), (π₯(Hom βπ)π₯)β© = β¨(Baseβndx), (π₯(Hom βπΆ)π₯)β©) |
6 | | fveq2 6892 |
. . . . . . 7
β’ (π = πΆ β (compβπ) = (compβπΆ)) |
7 | 6 | oveqd 7426 |
. . . . . 6
β’ (π = πΆ β (β¨π₯, π₯β©(compβπ)π₯) = (β¨π₯, π₯β©(compβπΆ)π₯)) |
8 | 7 | opeq2d 4881 |
. . . . 5
β’ (π = πΆ β β¨(+gβndx),
(β¨π₯, π₯β©(compβπ)π₯)β© = β¨(+gβndx),
(β¨π₯, π₯β©(compβπΆ)π₯)β©) |
9 | 5, 8 | preq12d 4746 |
. . . 4
β’ (π = πΆ β {β¨(Baseβndx), (π₯(Hom βπ)π₯)β©, β¨(+gβndx),
(β¨π₯, π₯β©(compβπ)π₯)β©} = {β¨(Baseβndx), (π₯(Hom βπΆ)π₯)β©, β¨(+gβndx),
(β¨π₯, π₯β©(compβπΆ)π₯)β©}) |
10 | 2, 9 | mpteq12dv 5240 |
. . 3
β’ (π = πΆ β (π₯ β (Baseβπ) β¦ {β¨(Baseβndx), (π₯(Hom βπ)π₯)β©, β¨(+gβndx),
(β¨π₯, π₯β©(compβπ)π₯)β©}) = (π₯ β (BaseβπΆ) β¦ {β¨(Baseβndx), (π₯(Hom βπΆ)π₯)β©, β¨(+gβndx),
(β¨π₯, π₯β©(compβπΆ)π₯)β©})) |
11 | | bj-endval.c |
. . 3
β’ (π β πΆ β Cat) |
12 | | fvex 6905 |
. . . . 5
β’
(BaseβπΆ)
β V |
13 | 12 | mptex 7225 |
. . . 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 7022 |
. 2
β’ (π β (End βπΆ) = (π₯ β (BaseβπΆ) β¦ {β¨(Baseβndx), (π₯(Hom βπΆ)π₯)β©, β¨(+gβndx),
(β¨π₯, π₯β©(compβπΆ)π₯)β©})) |
16 | | id 22 |
. . . . . 6
β’ (π₯ = π β π₯ = π) |
17 | 16, 16 | oveq12d 7427 |
. . . . 5
β’ (π₯ = π β (π₯(Hom βπΆ)π₯) = (π(Hom βπΆ)π)) |
18 | 17 | opeq2d 4881 |
. . . 4
β’ (π₯ = π β β¨(Baseβndx), (π₯(Hom βπΆ)π₯)β© = β¨(Baseβndx), (π(Hom βπΆ)π)β©) |
19 | 16, 16 | opeq12d 4882 |
. . . . . 6
β’ (π₯ = π β β¨π₯, π₯β© = β¨π, πβ©) |
20 | 19, 16 | oveq12d 7427 |
. . . . 5
β’ (π₯ = π β (β¨π₯, π₯β©(compβπΆ)π₯) = (β¨π, πβ©(compβπΆ)π)) |
21 | 20 | opeq2d 4881 |
. . . 4
β’ (π₯ = π β β¨(+gβndx),
(β¨π₯, π₯β©(compβπΆ)π₯)β© = β¨(+gβndx),
(β¨π, πβ©(compβπΆ)π)β©) |
22 | 18, 21 | preq12d 4746 |
. . 3
β’ (π₯ = π β {β¨(Baseβndx), (π₯(Hom βπΆ)π₯)β©, β¨(+gβndx),
(β¨π₯, π₯β©(compβπΆ)π₯)β©} = {β¨(Baseβndx), (π(Hom βπΆ)π)β©, β¨(+gβndx),
(β¨π, πβ©(compβπΆ)π)β©}) |
23 | 22 | adantl 483 |
. 2
β’ ((π β§ π₯ = π) β {β¨(Baseβndx), (π₯(Hom βπΆ)π₯)β©, β¨(+gβndx),
(β¨π₯, π₯β©(compβπΆ)π₯)β©} = {β¨(Baseβndx), (π(Hom βπΆ)π)β©, β¨(+gβndx),
(β¨π, πβ©(compβπΆ)π)β©}) |
24 | | bj-endval.x |
. 2
β’ (π β π β (BaseβπΆ)) |
25 | | prex 5433 |
. . 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 7006 |
1
β’ (π β ((End βπΆ)βπ) = {β¨(Baseβndx), (π(Hom βπΆ)π)β©, β¨(+gβndx),
(β¨π, πβ©(compβπΆ)π)β©}) |