Step | Hyp | Ref
| Expression |
1 | | mndtcbas.c |
. 2
β’ (π β πΆ = (MndToCatβπ)) |
2 | | mndtcbas.m |
. . 3
β’ (π β π β Mnd) |
3 | | sneq 4597 |
. . . . . 6
β’ (π = π β {π} = {π}) |
4 | 3 | opeq2d 4838 |
. . . . 5
β’ (π = π β β¨(Baseβndx), {π}β© =
β¨(Baseβndx), {π}β©) |
5 | | id 22 |
. . . . . . . 8
β’ (π = π β π = π) |
6 | | fveq2 6843 |
. . . . . . . 8
β’ (π = π β (Baseβπ) = (Baseβπ)) |
7 | 5, 5, 6 | oteq123d 4846 |
. . . . . . 7
β’ (π = π β β¨π, π, (Baseβπ)β© = β¨π, π, (Baseβπ)β©) |
8 | 7 | sneqd 4599 |
. . . . . 6
β’ (π = π β {β¨π, π, (Baseβπ)β©} = {β¨π, π, (Baseβπ)β©}) |
9 | 8 | opeq2d 4838 |
. . . . 5
β’ (π = π β β¨(Hom βndx), {β¨π, π, (Baseβπ)β©}β© = β¨(Hom βndx),
{β¨π, π, (Baseβπ)β©}β©) |
10 | 5, 5, 5 | oteq123d 4846 |
. . . . . . . 8
β’ (π = π β β¨π, π, πβ© = β¨π, π, πβ©) |
11 | | fveq2 6843 |
. . . . . . . 8
β’ (π = π β (+gβπ) = (+gβπ)) |
12 | 10, 11 | opeq12d 4839 |
. . . . . . 7
β’ (π = π β β¨β¨π, π, πβ©, (+gβπ)β© = β¨β¨π, π, πβ©, (+gβπ)β©) |
13 | 12 | sneqd 4599 |
. . . . . 6
β’ (π = π β {β¨β¨π, π, πβ©, (+gβπ)β©} = {β¨β¨π, π, πβ©, (+gβπ)β©}) |
14 | 13 | opeq2d 4838 |
. . . . 5
β’ (π = π β β¨(compβndx),
{β¨β¨π, π, πβ©, (+gβπ)β©}β© =
β¨(compβndx), {β¨β¨π, π, πβ©, (+gβπ)β©}β©) |
15 | 4, 9, 14 | tpeq123d 4710 |
. . . 4
β’ (π = π β {β¨(Baseβndx), {π}β©, β¨(Hom βndx),
{β¨π, π, (Baseβπ)β©}β©, β¨(compβndx),
{β¨β¨π, π, πβ©, (+gβπ)β©}β©} =
{β¨(Baseβndx), {π}β©, β¨(Hom βndx),
{β¨π, π, (Baseβπ)β©}β©, β¨(compβndx),
{β¨β¨π, π, πβ©, (+gβπ)β©}β©}) |
16 | | df-mndtc 47190 |
. . . 4
β’ MndToCat
= (π β Mnd β¦
{β¨(Baseβndx), {π}β©, β¨(Hom βndx), {β¨π, π, (Baseβπ)β©}β©, β¨(compβndx),
{β¨β¨π, π, πβ©, (+gβπ)β©}β©}) |
17 | | tpex 7682 |
. . . 4
β’
{β¨(Baseβndx), {π}β©, β¨(Hom βndx),
{β¨π, π, (Baseβπ)β©}β©, β¨(compβndx),
{β¨β¨π, π, πβ©, (+gβπ)β©}β©} β
V |
18 | 15, 16, 17 | fvmpt 6949 |
. . 3
β’ (π β Mnd β
(MndToCatβπ) =
{β¨(Baseβndx), {π}β©, β¨(Hom βndx),
{β¨π, π, (Baseβπ)β©}β©, β¨(compβndx),
{β¨β¨π, π, πβ©, (+gβπ)β©}β©}) |
19 | 2, 18 | syl 17 |
. 2
β’ (π β (MndToCatβπ) = {β¨(Baseβndx),
{π}β©, β¨(Hom
βndx), {β¨π,
π, (Baseβπ)β©}β©,
β¨(compβndx), {β¨β¨π, π, πβ©, (+gβπ)β©}β©}) |
20 | 1, 19 | eqtrd 2773 |
1
β’ (π β πΆ = {β¨(Baseβndx), {π}β©, β¨(Hom βndx),
{β¨π, π, (Baseβπ)β©}β©, β¨(compβndx),
{β¨β¨π, π, πβ©, (+gβπ)β©}β©}) |