Theorem postcof2nd

Description: The morphism part of the explicit post-composition functor sends a pair of functors to the induced map on natural transformations. (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypotheses	postcof1st.q	|- Q = ( C FuncCat D )
	postcof1st.r	|- R = ( D FuncCat E )
	postcof1st.o	|- .o. = ( <. R , Q >. curryF ( <. C , D >. o.F E ) )
	postcof1st.f	|- ( ph -> F e. ( D Func E ) )
	postcof1st.c	|- ( ph -> C e. Cat )
	postcof1st.k	|- K = ( ( 1st ` .o. ) ` F )
Assertion	postcof2nd	|- ( ph -> ( 2nd ` K ) = ( 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 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		postcof1st.q	|- Q = ( C FuncCat D )
2		postcof1st.r	|- R = ( D FuncCat E )
3		postcof1st.o	|- .o. = ( <. R , Q >. curryF ( <. C , D >. o.F E ) )
4		postcof1st.f	|- ( ph -> F e. ( D Func E ) )
5		postcof1st.c	|- ( ph -> C e. Cat )
6		postcof1st.k	|- K = ( ( 1st ` .o. ) ` F )
7	1 2 3 4 5 6	postcofval	|- ( ph -> K = <. ( 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 ) ) ) ) ) >. )
8		ovex	|- ( C Func D ) e. _V
9	8	mptex	|- ( g e. ( C Func D ) |-> ( F o.func g ) ) e. _V
10	8 8	mpoex	|- ( 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 ) ) ) ) ) e. _V
11	9 10	op2ndd	|- ( K = <. ( 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 ) ) ) ) ) >. -> ( 2nd ` K ) = ( 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 ) ) ) ) ) )
12	7 11	syl	|- ( ph -> ( 2nd ` K ) = ( 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 ) ) ) ) ) )