Step | Hyp | Ref
| Expression |
1 | | fucval.q |
. . . 4
β’ π = (πΆ FuncCat π·) |
2 | | fucval.b |
. . . 4
β’ π΅ = (πΆ Func π·) |
3 | | fucval.n |
. . . 4
β’ π = (πΆ Nat π·) |
4 | | fucval.a |
. . . 4
β’ π΄ = (BaseβπΆ) |
5 | | fucval.o |
. . . 4
β’ Β· =
(compβπ·) |
6 | | fucval.c |
. . . 4
β’ (π β πΆ β Cat) |
7 | | fucval.d |
. . . 4
β’ (π β π· β Cat) |
8 | | eqidd 2734 |
. . . 4
β’ (π β (π£ β (π΅ Γ π΅), β β π΅ β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (ππβ), π β (πππ) β¦ (π₯ β π΄ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β© Β· ((1st
ββ)βπ₯))(πβπ₯))))) = (π£ β (π΅ Γ π΅), β β π΅ β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (ππβ), π β (πππ) β¦ (π₯ β π΄ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β© Β· ((1st
ββ)βπ₯))(πβπ₯)))))) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | fucval 17851 |
. . 3
β’ (π β π = {β¨(Baseβndx), π΅β©, β¨(Hom βndx),
πβ©,
β¨(compβndx), (π£
β (π΅ Γ π΅), β β π΅ β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (ππβ), π β (πππ) β¦ (π₯ β π΄ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β© Β· ((1st
ββ)βπ₯))(πβπ₯)))))β©}) |
10 | 9 | fveq2d 6847 |
. 2
β’ (π β (compβπ) =
(compβ{β¨(Baseβndx), π΅β©, β¨(Hom βndx), πβ©, β¨(compβndx),
(π£ β (π΅ Γ π΅), β β π΅ β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (ππβ), π β (πππ) β¦ (π₯ β π΄ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β© Β· ((1st
ββ)βπ₯))(πβπ₯)))))β©})) |
11 | | fuccofval.x |
. 2
β’ β =
(compβπ) |
12 | 2 | ovexi 7392 |
. . . . 5
β’ π΅ β V |
13 | 12, 12 | xpex 7688 |
. . . 4
β’ (π΅ Γ π΅) β V |
14 | 13, 12 | mpoex 8013 |
. . 3
β’ (π£ β (π΅ Γ π΅), β β π΅ β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (ππβ), π β (πππ) β¦ (π₯ β π΄ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β© Β· ((1st
ββ)βπ₯))(πβπ₯))))) β V |
15 | | catstr 17850 |
. . . 4
β’
{β¨(Baseβndx), π΅β©, β¨(Hom βndx), πβ©, β¨(compβndx),
(π£ β (π΅ Γ π΅), β β π΅ β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (ππβ), π β (πππ) β¦ (π₯ β π΄ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β© Β· ((1st
ββ)βπ₯))(πβπ₯)))))β©} Struct β¨1, ;15β© |
16 | | ccoid 17300 |
. . . 4
β’ comp =
Slot (compβndx) |
17 | | snsstp3 4779 |
. . . 4
β’
{β¨(compβndx), (π£ β (π΅ Γ π΅), β β π΅ β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (ππβ), π β (πππ) β¦ (π₯ β π΄ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β© Β· ((1st
ββ)βπ₯))(πβπ₯)))))β©} β {β¨(Baseβndx),
π΅β©, β¨(Hom
βndx), πβ©,
β¨(compβndx), (π£
β (π΅ Γ π΅), β β π΅ β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (ππβ), π β (πππ) β¦ (π₯ β π΄ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β© Β· ((1st
ββ)βπ₯))(πβπ₯)))))β©} |
18 | 15, 16, 17 | strfv 17081 |
. . 3
β’ ((π£ β (π΅ Γ π΅), β β π΅ β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (ππβ), π β (πππ) β¦ (π₯ β π΄ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β© Β· ((1st
ββ)βπ₯))(πβπ₯))))) β V β (π£ β (π΅ Γ π΅), β β π΅ β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (ππβ), π β (πππ) β¦ (π₯ β π΄ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β© Β· ((1st
ββ)βπ₯))(πβπ₯))))) = (compβ{β¨(Baseβndx),
π΅β©, β¨(Hom
βndx), πβ©,
β¨(compβndx), (π£
β (π΅ Γ π΅), β β π΅ β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (ππβ), π β (πππ) β¦ (π₯ β π΄ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β© Β· ((1st
ββ)βπ₯))(πβπ₯)))))β©})) |
19 | 14, 18 | ax-mp 5 |
. 2
β’ (π£ β (π΅ Γ π΅), β β π΅ β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (ππβ), π β (πππ) β¦ (π₯ β π΄ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β© Β· ((1st
ββ)βπ₯))(πβπ₯))))) = (compβ{β¨(Baseβndx),
π΅β©, β¨(Hom
βndx), πβ©,
β¨(compβndx), (π£
β (π΅ Γ π΅), β β π΅ β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (ππβ), π β (πππ) β¦ (π₯ β π΄ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β© Β· ((1st
ββ)βπ₯))(πβπ₯)))))β©}) |
20 | 10, 11, 19 | 3eqtr4g 2798 |
1
β’ (π β β = (π£ β (π΅ Γ π΅), β β π΅ β¦ β¦(1st
βπ£) / πβ¦β¦(2nd
βπ£) / πβ¦(π β (ππβ), π β (πππ) β¦ (π₯ β π΄ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((1st βπ)βπ₯)β© Β· ((1st
ββ)βπ₯))(πβπ₯)))))) |