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\mathrm{Nat}E$$
	prcof21a.a	$$⊢\phi \to A\in \left(KNL\right)$$
	prcof21a.p	No typesetting found for |- ( ph -> ( 2nd ` ( <. D , E >. -o.F F ) ) = P ) with typecode |-
	prcof22a.b	$$⊢B={\mathrm{Base}}_C$$
	prcof22a.x	$$⊢\phi \to X\in B$$
	prcof22a.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
Assertion	prcof22a	$$⊢\phi \to \left(KPL\right)\left(A\right)\left(X\right)=A\left(1^{st}\left(F\right)\left(X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		prcof21a.n	$$⊢N=D\mathrm{Nat}E$$
2		prcof21a.a	$$⊢\phi \to A\in \left(KNL\right)$$
3		prcof21a.p	Could not format ( ph -> ( 2nd ` ( <. D , E >. -o.F F ) ) = P ) : No typesetting found for |- ( ph -> ( 2nd ` ( <. D , E >. -o.F F ) ) = P ) with typecode |-
4		prcof22a.b	$$⊢B={\mathrm{Base}}_C$$
5		prcof22a.x	$$⊢\phi \to X\in B$$
6		prcof22a.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
7	1 2 3 6	prcof21a	$$⊢\phi \to \left(KPL\right)\left(A\right)=A\circ 1^{st}\left(F\right)$$
8	7	fveq1d	$$⊢\phi \to \left(KPL\right)\left(A\right)\left(X\right)=\left(A\circ 1^{st}\left(F\right)\right)\left(X\right)$$
9		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
10	6	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
11	4 9 10	funcf1	$$⊢\phi \to 1^{st}\left(F\right):B⟶{\mathrm{Base}}_D$$
12	11 5	fvco3d	$$⊢\phi \to \left(A\circ 1^{st}\left(F\right)\right)\left(X\right)=A\left(1^{st}\left(F\right)\left(X\right)\right)$$
13	8 12	eqtrd	$$⊢\phi \to \left(KPL\right)\left(A\right)\left(X\right)=A\left(1^{st}\left(F\right)\left(X\right)\right)$$