Theorem prcof2a

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

	Ref	Expression
Hypotheses	prcof2a.n	$$⊢N=D\mathrm{Nat}E$$
	prcof2a.k	$$⊢\phi \to K\in \left(D\mathrm{Func}E\right)$$
	prcof2a.l	$$⊢\phi \to L\in \left(D\mathrm{Func}E\right)$$
	prcof2a.p	No typesetting found for |- ( ph -> ( 2nd ` ( <. D , E >. -o.F F ) ) = P ) with typecode |-
	prcof2a.f	$$⊢\phi \to F\in U$$
Assertion	prcof2a	$$⊢\phi \to KPL=\left(a\in \left(KNL\right)⟼a\circ 1^{st}\left(F\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		prcof2a.n	$$⊢N=D\mathrm{Nat}E$$
2		prcof2a.k	$$⊢\phi \to K\in \left(D\mathrm{Func}E\right)$$
3		prcof2a.l	$$⊢\phi \to L\in \left(D\mathrm{Func}E\right)$$
4		prcof2a.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 |-
5		prcof2a.f	$$⊢\phi \to F\in U$$
6		eqid	$$⊢D\mathrm{Func}E=D\mathrm{Func}E$$
7	2	func1st2nd	$$⊢\phi \to 1^{st}\left(K\right)\left(D\mathrm{Func}E\right)2^{nd}\left(K\right)$$
8	7	funcrcl2	$$⊢\phi \to D\in \mathrm{Cat}$$
9	7	funcrcl3	$$⊢\phi \to E\in \mathrm{Cat}$$
10	6 1 8 9 5	prcofvala	Could not format ( ph -> ( <. D , E >. -o.F F ) = <. ( k e. ( D Func E ) |-> ( k o.func F ) ) , ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) >. ) : No typesetting found for |- ( ph -> ( <. D , E >. -o.F F ) = <. ( k e. ( D Func E ) |-> ( k o.func F ) ) , ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) >. ) with typecode |-
11	10	fveq2d	Could not format ( ph -> ( 2nd ` ( <. D , E >. -o.F F ) ) = ( 2nd ` <. ( k e. ( D Func E ) |-> ( k o.func F ) ) , ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) >. ) ) : No typesetting found for |- ( ph -> ( 2nd ` ( <. D , E >. -o.F F ) ) = ( 2nd ` <. ( k e. ( D Func E ) |-> ( k o.func F ) ) , ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) >. ) ) with typecode |-
12		ovex	$$⊢D\mathrm{Func}E\in \mathrm{V}$$
13	12	mptex	$$⊢\left(k\in \left(D\mathrm{Func}E\right)⟼k{\circ }_{\mathrm{func}}F\right)\in \mathrm{V}$$
14	12 12	mpoex	$$⊢\left(k\in \left(D\mathrm{Func}E\right),l\in \left(D\mathrm{Func}E\right)⟼\left(a\in \left(kNl\right)⟼a\circ 1^{st}\left(F\right)\right)\right)\in \mathrm{V}$$
15	13 14	op2nd	$$⊢2^{nd}\left(⟨\left(k\in \left(D\mathrm{Func}E\right)⟼k{\circ }_{\mathrm{func}}F\right),\left(k\in \left(D\mathrm{Func}E\right),l\in \left(D\mathrm{Func}E\right)⟼\left(a\in \left(kNl\right)⟼a\circ 1^{st}\left(F\right)\right)\right)⟩\right)=\left(k\in \left(D\mathrm{Func}E\right),l\in \left(D\mathrm{Func}E\right)⟼\left(a\in \left(kNl\right)⟼a\circ 1^{st}\left(F\right)\right)\right)$$
16	11 15	eqtrdi	Could not format ( ph -> ( 2nd ` ( <. D , E >. -o.F F ) ) = ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) ) : No typesetting found for |- ( ph -> ( 2nd ` ( <. D , E >. -o.F F ) ) = ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) ) with typecode |-
17	4 16	eqtr3d	$$⊢\phi \to P=\left(k\in \left(D\mathrm{Func}E\right),l\in \left(D\mathrm{Func}E\right)⟼\left(a\in \left(kNl\right)⟼a\circ 1^{st}\left(F\right)\right)\right)$$
18		simprl	$$⊢\left(\phi \wedge \left(k=K\wedge l=L\right)\right)\to k=K$$
19		simprr	$$⊢\left(\phi \wedge \left(k=K\wedge l=L\right)\right)\to l=L$$
20	18 19	oveq12d	$$⊢\left(\phi \wedge \left(k=K\wedge l=L\right)\right)\to kNl=KNL$$
21	20	mpteq1d	$$⊢\left(\phi \wedge \left(k=K\wedge l=L\right)\right)\to \left(a\in \left(kNl\right)⟼a\circ 1^{st}\left(F\right)\right)=\left(a\in \left(KNL\right)⟼a\circ 1^{st}\left(F\right)\right)$$
22		ovex	$$⊢KNL\in \mathrm{V}$$
23	22	mptex	$$⊢\left(a\in \left(KNL\right)⟼a\circ 1^{st}\left(F\right)\right)\in \mathrm{V}$$
24	23	a1i	$$⊢\phi \to \left(a\in \left(KNL\right)⟼a\circ 1^{st}\left(F\right)\right)\in \mathrm{V}$$
25	17 21 2 3 24	ovmpod	$$⊢\phi \to KPL=\left(a\in \left(KNL\right)⟼a\circ 1^{st}\left(F\right)\right)$$