Theorem prcof22a

Description: The morphism part of the pre-composition functor. (Contributed by Zhi Wang, 3-Nov-2025)

	Ref	Expression
Hypotheses	prcof21a.n	|- N = ( D Nat E )
	prcof21a.a	|- ( ph -> A e. ( K N L ) )
	prcof21a.p	|- ( ph -> ( 2nd ` ( <. D , E >. -o.F F ) ) = P )
	prcof22a.b	|- B = ( Base ` C )
	prcof22a.x	|- ( ph -> X e. B )
	prcof22a.f	|- ( ph -> F e. ( C Func D ) )
Assertion	prcof22a	|- ( ph -> ( ( ( K P L ) ` A ) ` X ) = ( A ` ( ( 1st ` F ) ` X ) ) )

Proof

Step	Hyp	Ref	Expression
1		prcof21a.n	|- N = ( D Nat E )
2		prcof21a.a	|- ( ph -> A e. ( K N L ) )
3		prcof21a.p	|- ( ph -> ( 2nd ` ( <. D , E >. -o.F F ) ) = P )
4		prcof22a.b	|- B = ( Base ` C )
5		prcof22a.x	|- ( ph -> X e. B )
6		prcof22a.f	|- ( ph -> F e. ( C Func D ) )
7	1 2 3 6	prcof21a	|- ( ph -> ( ( K P L ) ` A ) = ( A o. ( 1st ` F ) ) )
8	7	fveq1d	|- ( ph -> ( ( ( K P L ) ` A ) ` X ) = ( ( A o. ( 1st ` F ) ) ` X ) )
9		eqid	|- ( Base ` D ) = ( Base ` D )
10	6	func1st2nd	|- ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
11	4 9 10	funcf1	|- ( ph -> ( 1st ` F ) : B --> ( Base ` D ) )
12	11 5	fvco3d	|- ( ph -> ( ( A o. ( 1st ` F ) ) ` X ) = ( A ` ( ( 1st ` F ) ` X ) ) )
13	8 12	eqtrd	|- ( ph -> ( ( ( K P L ) ` A ) ` X ) = ( A ` ( ( 1st ` F ) ` X ) ) )