Theorem prcof2

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