Theorem postcofval

Description: Value of the post-composition functor as a curry of the functor composition bifunctor. (Contributed by Zhi Wang, 11-Oct-2025)

	Ref	Expression
Hypotheses	postcofval.q	$$⊢Q=C\mathrm{FuncCat}D$$
	postcofval.r	$$⊢R=D\mathrm{FuncCat}E$$
	postcofval.o	No typesetting found for |- .o. = ( <. R , Q >. curryF ( <. C , D >. o.F E ) ) with typecode |-
	postcofval.f	$$⊢\phi \to F\in \left(D\mathrm{Func}E\right)$$
	postcofval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	postcofval.k	No typesetting found for |- K = ( ( 1st ` .o. ) ` F ) with typecode |-
Assertion	postcofval	$$⊢\phi \to K=⟨\left(g\in \left(C\mathrm{Func}D\right)⟼F{\circ }_{\mathrm{func}}g\right),\left(g\in \left(C\mathrm{Func}D\right),h\in \left(C\mathrm{Func}D\right)⟼\left(a\in \left(g\left(C\mathrm{Nat}D\right)h\right)⟼\left(x\in {\mathrm{Base}}_C⟼\left(1^{st}\left(g\right)\left(x\right)2^{nd}\left(F\right)1^{st}\left(h\right)\left(x\right)\right)\left(a\left(x\right)\right)\right)\right)\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		postcofval.q	$$⊢Q=C\mathrm{FuncCat}D$$
2		postcofval.r	$$⊢R=D\mathrm{FuncCat}E$$
3		postcofval.o	Could not format .o. = ( <. R , Q >. curryF ( <. C , D >. o.F E ) ) : No typesetting found for |- .o. = ( <. R , Q >. curryF ( <. C , D >. o.F E ) ) with typecode |-
4		postcofval.f	$$⊢\phi \to F\in \left(D\mathrm{Func}E\right)$$
5		postcofval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
6		postcofval.k	Could not format K = ( ( 1st ` .o. ) ` F ) : No typesetting found for |- K = ( ( 1st ` .o. ) ` F ) with typecode |-
7	2	fucbas	$$⊢D\mathrm{Func}E={\mathrm{Base}}_R$$
8		relfunc	$$⊢\mathrm{Rel}\left(D\mathrm{Func}E\right)$$
9		1st2ndbr	$$⊢\left(\mathrm{Rel}\left(D\mathrm{Func}E\right)\wedge F\in \left(D\mathrm{Func}E\right)\right)\to 1^{st}\left(F\right)\left(D\mathrm{Func}E\right)2^{nd}\left(F\right)$$
10	8 4 9	sylancr	$$⊢\phi \to 1^{st}\left(F\right)\left(D\mathrm{Func}E\right)2^{nd}\left(F\right)$$
11	10	funcrcl2	$$⊢\phi \to D\in \mathrm{Cat}$$
12	10	funcrcl3	$$⊢\phi \to E\in \mathrm{Cat}$$
13	2 11 12	fuccat	$$⊢\phi \to R\in \mathrm{Cat}$$
14	1 5 11	fuccat	$$⊢\phi \to Q\in \mathrm{Cat}$$
15	2 1	oveq12i	$$⊢R{\times }_{c}Q=\left(D\mathrm{FuncCat}E\right){\times }_c\left(C\mathrm{FuncCat}D\right)$$
16		eqid	$$⊢C\mathrm{FuncCat}E=C\mathrm{FuncCat}E$$
17	15 16 5 11 12	fucofunca	Could not format ( ph -> ( <. C , D >. o.F E ) e. ( ( R Xc. Q ) Func ( C FuncCat E ) ) ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) e. ( ( R Xc. Q ) Func ( C FuncCat E ) ) ) with typecode |-
18	1	fucbas	$$⊢C\mathrm{Func}D={\mathrm{Base}}_Q$$
19		eqid	$$⊢C\mathrm{Nat}D=C\mathrm{Nat}D$$
20	1 19	fuchom	$$⊢C\mathrm{Nat}D=\mathrm{Hom}\left(Q\right)$$
21		eqid	$$⊢\mathrm{Id}\left(R\right)=\mathrm{Id}\left(R\right)$$
22	3 7 13 14 17 18 4 6 20 21	curf1	Could not format ( ph -> K = <. ( g e. ( C Func D ) |-> ( F ( 1st ` ( <. C , D >. o.F E ) ) g ) ) , ( g e. ( C Func D ) , h e. ( C Func D ) |-> ( a e. ( g ( C Nat D ) h ) |-> ( ( ( Id ` R ) ` F ) ( <. F , g >. ( 2nd ` ( <. C , D >. o.F E ) ) <. F , h >. ) a ) ) ) >. ) : No typesetting found for |- ( ph -> K = <. ( g e. ( C Func D ) |-> ( F ( 1st ` ( <. C , D >. o.F E ) ) g ) ) , ( g e. ( C Func D ) , h e. ( C Func D ) |-> ( a e. ( g ( C Nat D ) h ) |-> ( ( ( Id ` R ) ` F ) ( <. F , g >. ( 2nd ` ( <. C , D >. o.F E ) ) <. F , h >. ) a ) ) ) >. ) with typecode |-
23		eqidd	Could not format ( ( ph /\ g e. ( C Func D ) ) -> ( 1st ` ( <. C , D >. o.F E ) ) = ( 1st ` ( <. C , D >. o.F E ) ) ) : No typesetting found for |- ( ( ph /\ g e. ( C Func D ) ) -> ( 1st ` ( <. C , D >. o.F E ) ) = ( 1st ` ( <. C , D >. o.F E ) ) ) with typecode |-
24		simpr	$$⊢\left(\phi \wedge g\in \left(C\mathrm{Func}D\right)\right)\to g\in \left(C\mathrm{Func}D\right)$$
25	4	adantr	$$⊢\left(\phi \wedge g\in \left(C\mathrm{Func}D\right)\right)\to F\in \left(D\mathrm{Func}E\right)$$
26	23 24 25	fuco11b	Could not format ( ( ph /\ g e. ( C Func D ) ) -> ( F ( 1st ` ( <. C , D >. o.F E ) ) g ) = ( F o.func g ) ) : No typesetting found for |- ( ( ph /\ g e. ( C Func D ) ) -> ( F ( 1st ` ( <. C , D >. o.F E ) ) g ) = ( F o.func g ) ) with typecode |-
27	26	mpteq2dva	Could not format ( ph -> ( g e. ( C Func D ) |-> ( F ( 1st ` ( <. C , D >. o.F E ) ) g ) ) = ( g e. ( C Func D ) |-> ( F o.func g ) ) ) : No typesetting found for |- ( ph -> ( g e. ( C Func D ) |-> ( F ( 1st ` ( <. C , D >. o.F E ) ) g ) ) = ( g e. ( C Func D ) |-> ( F o.func g ) ) ) with typecode |-
28		eqidd	Could not format ( ( ph /\ a e. ( g ( C Nat D ) h ) ) -> ( 2nd ` ( <. C , D >. o.F E ) ) = ( 2nd ` ( <. C , D >. o.F E ) ) ) : No typesetting found for |- ( ( ph /\ a e. ( g ( C Nat D ) h ) ) -> ( 2nd ` ( <. C , D >. o.F E ) ) = ( 2nd ` ( <. C , D >. o.F E ) ) ) with typecode |-
29		simpr	$$⊢\left(\phi \wedge a\in \left(g\left(C\mathrm{Nat}D\right)h\right)\right)\to a\in \left(g\left(C\mathrm{Nat}D\right)h\right)$$
30	4	adantr	$$⊢\left(\phi \wedge a\in \left(g\left(C\mathrm{Nat}D\right)h\right)\right)\to F\in \left(D\mathrm{Func}E\right)$$
31	28 21 2 29 30	fucolid	Could not format ( ( ph /\ a e. ( g ( C Nat D ) h ) ) -> ( ( ( Id ` R ) ` F ) ( <. F , g >. ( 2nd ` ( <. C , D >. o.F E ) ) <. F , h >. ) a ) = ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` g ) ` x ) ( 2nd ` F ) ( ( 1st ` h ) ` x ) ) ` ( a ` x ) ) ) ) : No typesetting found for |- ( ( ph /\ a e. ( g ( C Nat D ) h ) ) -> ( ( ( Id ` R ) ` F ) ( <. F , g >. ( 2nd ` ( <. C , D >. o.F E ) ) <. F , h >. ) a ) = ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` g ) ` x ) ( 2nd ` F ) ( ( 1st ` h ) ` x ) ) ` ( a ` x ) ) ) ) with typecode |-
32	31	mpteq2dva	Could not format ( ph -> ( a e. ( g ( C Nat D ) h ) |-> ( ( ( Id ` R ) ` F ) ( <. F , g >. ( 2nd ` ( <. C , D >. o.F E ) ) <. F , h >. ) a ) ) = ( a e. ( g ( C Nat D ) h ) |-> ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` g ) ` x ) ( 2nd ` F ) ( ( 1st ` h ) ` x ) ) ` ( a ` x ) ) ) ) ) : No typesetting found for |- ( ph -> ( a e. ( g ( C Nat D ) h ) |-> ( ( ( Id ` R ) ` F ) ( <. F , g >. ( 2nd ` ( <. C , D >. o.F E ) ) <. F , h >. ) a ) ) = ( a e. ( g ( C Nat D ) h ) |-> ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` g ) ` x ) ( 2nd ` F ) ( ( 1st ` h ) ` x ) ) ` ( a ` x ) ) ) ) ) with typecode |-
33	32	mpoeq3dv	Could not format ( ph -> ( g e. ( C Func D ) , h e. ( C Func D ) |-> ( a e. ( g ( C Nat D ) h ) |-> ( ( ( Id ` R ) ` F ) ( <. F , g >. ( 2nd ` ( <. C , D >. o.F E ) ) <. F , h >. ) a ) ) ) = ( g e. ( C Func D ) , h e. ( C Func D ) |-> ( a e. ( g ( C Nat D ) h ) |-> ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` g ) ` x ) ( 2nd ` F ) ( ( 1st ` h ) ` x ) ) ` ( a ` x ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( g e. ( C Func D ) , h e. ( C Func D ) |-> ( a e. ( g ( C Nat D ) h ) |-> ( ( ( Id ` R ) ` F ) ( <. F , g >. ( 2nd ` ( <. C , D >. o.F E ) ) <. F , h >. ) a ) ) ) = ( g e. ( C Func D ) , h e. ( C Func D ) |-> ( a e. ( g ( C Nat D ) h ) |-> ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` g ) ` x ) ( 2nd ` F ) ( ( 1st ` h ) ` x ) ) ` ( a ` x ) ) ) ) ) ) with typecode |-
34	27 33	opeq12d	Could not format ( ph -> <. ( g e. ( C Func D ) |-> ( F ( 1st ` ( <. C , D >. o.F E ) ) g ) ) , ( g e. ( C Func D ) , h e. ( C Func D ) |-> ( a e. ( g ( C Nat D ) h ) |-> ( ( ( Id ` R ) ` F ) ( <. F , g >. ( 2nd ` ( <. C , D >. o.F E ) ) <. F , h >. ) a ) ) ) >. = <. ( g e. ( C Func D ) |-> ( F o.func g ) ) , ( g e. ( C Func D ) , h e. ( C Func D ) |-> ( a e. ( g ( C Nat D ) h ) |-> ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` g ) ` x ) ( 2nd ` F ) ( ( 1st ` h ) ` x ) ) ` ( a ` x ) ) ) ) ) >. ) : No typesetting found for |- ( ph -> <. ( g e. ( C Func D ) |-> ( F ( 1st ` ( <. C , D >. o.F E ) ) g ) ) , ( g e. ( C Func D ) , h e. ( C Func D ) |-> ( a e. ( g ( C Nat D ) h ) |-> ( ( ( Id ` R ) ` F ) ( <. F , g >. ( 2nd ` ( <. C , D >. o.F E ) ) <. F , h >. ) a ) ) ) >. = <. ( g e. ( C Func D ) |-> ( F o.func g ) ) , ( g e. ( C Func D ) , h e. ( C Func D ) |-> ( a e. ( g ( C Nat D ) h ) |-> ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` g ) ` x ) ( 2nd ` F ) ( ( 1st ` h ) ` x ) ) ` ( a ` x ) ) ) ) ) >. ) with typecode |-
35	22 34	eqtrd	$$⊢\phi \to K=⟨\left(g\in \left(C\mathrm{Func}D\right)⟼F{\circ }_{\mathrm{func}}g\right),\left(g\in \left(C\mathrm{Func}D\right),h\in \left(C\mathrm{Func}D\right)⟼\left(a\in \left(g\left(C\mathrm{Nat}D\right)h\right)⟼\left(x\in {\mathrm{Base}}_C⟼\left(1^{st}\left(g\right)\left(x\right)2^{nd}\left(F\right)1^{st}\left(h\right)\left(x\right)\right)\left(a\left(x\right)\right)\right)\right)\right)⟩$$