Theorem precofval

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

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

Proof

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