Theorem prcof1

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

	Ref	Expression
Hypotheses	prcof1.k	$$⊢\phi \to K\in \left(D\mathrm{Func}E\right)$$
	prcof1.o	No typesetting found for |- ( ph -> ( 1st ` ( <. D , E >. -o.F F ) ) = O ) with typecode |-
Assertion	prcof1	$$⊢\phi \to O\left(K\right)=K{\circ }_{\mathrm{func}}F$$

Proof

Step	Hyp	Ref	Expression
1		prcof1.k	$$⊢\phi \to K\in \left(D\mathrm{Func}E\right)$$
2		prcof1.o	Could not format ( ph -> ( 1st ` ( <. D , E >. -o.F F ) ) = O ) : No typesetting found for |- ( ph -> ( 1st ` ( <. D , E >. -o.F F ) ) = O ) with typecode |-
3	2	adantr	Could not format ( ( ph /\ F e. _V ) -> ( 1st ` ( <. D , E >. -o.F F ) ) = O ) : No typesetting found for |- ( ( ph /\ F e. _V ) -> ( 1st ` ( <. D , E >. -o.F F ) ) = O ) with typecode |-
4		eqid	$$⊢D\mathrm{Func}E=D\mathrm{Func}E$$
5		eqid	$$⊢D\mathrm{Nat}E=D\mathrm{Nat}E$$
6	1	adantr	$$⊢\left(\phi \wedge F\in \mathrm{V}\right)\to K\in \left(D\mathrm{Func}E\right)$$
7	6	func1st2nd	$$⊢\left(\phi \wedge F\in \mathrm{V}\right)\to 1^{st}\left(K\right)\left(D\mathrm{Func}E\right)2^{nd}\left(K\right)$$
8	7	funcrcl2	$$⊢\left(\phi \wedge F\in \mathrm{V}\right)\to D\in \mathrm{Cat}$$
9	7	funcrcl3	$$⊢\left(\phi \wedge F\in \mathrm{V}\right)\to E\in \mathrm{Cat}$$
10		simpr	$$⊢\left(\phi \wedge F\in \mathrm{V}\right)\to F\in \mathrm{V}$$
11	4 5 8 9 10	prcofvala	Could not format ( ( ph /\ F e. _V ) -> ( <. 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 ( D Nat E ) l ) |-> ( a o. ( 1st ` F ) ) ) ) >. ) : No typesetting found for |- ( ( ph /\ F e. _V ) -> ( <. 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 ( D Nat E ) l ) |-> ( a o. ( 1st ` F ) ) ) ) >. ) with typecode |-
12	11	fveq2d	Could not format ( ( ph /\ F e. _V ) -> ( 1st ` ( <. D , E >. -o.F F ) ) = ( 1st ` <. ( k e. ( D Func E ) |-> ( k o.func F ) ) , ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k ( D Nat E ) l ) |-> ( a o. ( 1st ` F ) ) ) ) >. ) ) : No typesetting found for |- ( ( ph /\ F e. _V ) -> ( 1st ` ( <. D , E >. -o.F F ) ) = ( 1st ` <. ( k e. ( D Func E ) |-> ( k o.func F ) ) , ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k ( D Nat E ) l ) |-> ( a o. ( 1st ` 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\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(k\left(D\mathrm{Nat}E\right)l\right)⟼a\circ 1^{st}\left(F\right)\right)\right)\in \mathrm{V}$$
16	14 15	op1st	$$⊢1^{st}\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(k\left(D\mathrm{Nat}E\right)l\right)⟼a\circ 1^{st}\left(F\right)\right)\right)⟩\right)=\left(k\in \left(D\mathrm{Func}E\right)⟼k{\circ }_{\mathrm{func}}F\right)$$
17	12 16	eqtrdi	Could not format ( ( ph /\ F e. _V ) -> ( 1st ` ( <. D , E >. -o.F F ) ) = ( k e. ( D Func E ) |-> ( k o.func F ) ) ) : No typesetting found for |- ( ( ph /\ F e. _V ) -> ( 1st ` ( <. D , E >. -o.F F ) ) = ( k e. ( D Func E ) |-> ( k o.func F ) ) ) with typecode |-
18	3 17	eqtr3d	$$⊢\left(\phi \wedge F\in \mathrm{V}\right)\to O=\left(k\in \left(D\mathrm{Func}E\right)⟼k{\circ }_{\mathrm{func}}F\right)$$
19		simpr	$$⊢\left(\left(\phi \wedge F\in \mathrm{V}\right)\wedge k=K\right)\to k=K$$
20	19	oveq1d	$$⊢\left(\left(\phi \wedge F\in \mathrm{V}\right)\wedge k=K\right)\to k{\circ }_{\mathrm{func}}F=K{\circ }_{\mathrm{func}}F$$
21		ovexd	$$⊢\left(\phi \wedge F\in \mathrm{V}\right)\to K{\circ }_{\mathrm{func}}F\in \mathrm{V}$$
22	18 20 6 21	fvmptd	$$⊢\left(\phi \wedge F\in \mathrm{V}\right)\to O\left(K\right)=K{\circ }_{\mathrm{func}}F$$
23		0fv	$$⊢\varnothing \left(K\right)=\varnothing$$
24		reldmprcof	Could not format Rel dom -o.F : No typesetting found for |- Rel dom -o.F with typecode |-
25	24	ovprc2	Could not format ( -. F e. _V -> ( <. D , E >. -o.F F ) = (/) ) : No typesetting found for |- ( -. F e. _V -> ( <. D , E >. -o.F F ) = (/) ) with typecode |-
26	25	fveq2d	Could not format ( -. F e. _V -> ( 1st ` ( <. D , E >. -o.F F ) ) = ( 1st ` (/) ) ) : No typesetting found for |- ( -. F e. _V -> ( 1st ` ( <. D , E >. -o.F F ) ) = ( 1st ` (/) ) ) with typecode |-
27		1st0	$$⊢1^{st}\left(\varnothing \right)=\varnothing$$
28	26 27	eqtrdi	Could not format ( -. F e. _V -> ( 1st ` ( <. D , E >. -o.F F ) ) = (/) ) : No typesetting found for |- ( -. F e. _V -> ( 1st ` ( <. D , E >. -o.F F ) ) = (/) ) with typecode |-
29	2 28	sylan9req	$$⊢\left(\phi \wedge \neg F\in \mathrm{V}\right)\to O=\varnothing$$
30	29	fveq1d	$$⊢\left(\phi \wedge \neg F\in \mathrm{V}\right)\to O\left(K\right)=\varnothing \left(K\right)$$
31		df-cofu	$$⊢{\circ }_{\mathrm{func}}=\left(l\in \mathrm{V},k\in \mathrm{V}⟼⟨1^{st}\left(l\right)\circ 1^{st}\left(k\right),\left(a\in \mathrm{dom}\mathrm{dom}{2}^{nd}\left(k\right),b\in \mathrm{dom}\mathrm{dom}{2}^{nd}\left(k\right)⟼\left(1^{st}\left(k\right)\left(a\right)2^{nd}\left(l\right)1^{st}\left(k\right)\left(b\right)\right)\circ \left(a{2}^{nd}\left(k\right)b\right)\right)⟩\right)$$
32	31	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}{\circ }_{\mathrm{func}}$$
33	32	ovprc2	$$⊢\neg F\in \mathrm{V}\to K{\circ }_{\mathrm{func}}F=\varnothing$$
34	33	adantl	$$⊢\left(\phi \wedge \neg F\in \mathrm{V}\right)\to K{\circ }_{\mathrm{func}}F=\varnothing$$
35	23 30 34	3eqtr4a	$$⊢\left(\phi \wedge \neg F\in \mathrm{V}\right)\to O\left(K\right)=K{\circ }_{\mathrm{func}}F$$
36	22 35	pm2.61dan	$$⊢\phi \to O\left(K\right)=K{\circ }_{\mathrm{func}}F$$