Theorem prcof21a

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 |-
	prcof21a.f	$$⊢\phi \to F\in U$$
Assertion	prcof21a	$$⊢\phi \to \left(KPL\right)\left(A\right)=A\circ 1^{st}\left(F\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		prcof21a.f	$$⊢\phi \to F\in U$$
5	1	natrcl	$$⊢A\in \left(KNL\right)\to \left(K\in \left(D\mathrm{Func}E\right)\wedge L\in \left(D\mathrm{Func}E\right)\right)$$
6	2 5	syl	$$⊢\phi \to \left(K\in \left(D\mathrm{Func}E\right)\wedge L\in \left(D\mathrm{Func}E\right)\right)$$
7	6	simpld	$$⊢\phi \to K\in \left(D\mathrm{Func}E\right)$$
8	6	simprd	$$⊢\phi \to L\in \left(D\mathrm{Func}E\right)$$
9	1 7 8 3 4	prcof2a	$$⊢\phi \to KPL=\left(a\in \left(KNL\right)⟼a\circ 1^{st}\left(F\right)\right)$$
10		simpr	$$⊢\left(\phi \wedge a=A\right)\to a=A$$
11	10	coeq1d	$$⊢\left(\phi \wedge a=A\right)\to a\circ 1^{st}\left(F\right)=A\circ 1^{st}\left(F\right)$$
12		fvexd	$$⊢\phi \to 1^{st}\left(F\right)\in \mathrm{V}$$
13	2 12	coexd	$$⊢\phi \to A\circ 1^{st}\left(F\right)\in \mathrm{V}$$
14	9 11 2 13	fvmptd	$$⊢\phi \to \left(KPL\right)\left(A\right)=A\circ 1^{st}\left(F\right)$$