Theorem prcofval

Description: Value of the pre-composition functor. (Contributed by Zhi Wang, 2-Nov-2025)

	Ref	Expression
Hypotheses	prcofvalg.b	$$⊢B=D\mathrm{Func}E$$
	prcofvalg.n	$$⊢N=D\mathrm{Nat}E$$
	prcofvala.d	$$⊢\phi \to D\in V$$
	prcofvala.e	$$⊢\phi \to E\in W$$
	prcofval.r	$$⊢\mathrm{Rel}R$$
	prcofval.f	$$⊢\phi \to FRG$$
Assertion	prcofval	Could not format assertion : No typesetting found for |- ( ph -> ( <. D , E >. -o.F <. F , G >. ) = <. ( k e. B |-> ( k o.func <. F , G >. ) ) , ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. F ) ) ) >. ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		prcofvalg.b	$$⊢B=D\mathrm{Func}E$$
2		prcofvalg.n	$$⊢N=D\mathrm{Nat}E$$
3		prcofvala.d	$$⊢\phi \to D\in V$$
4		prcofvala.e	$$⊢\phi \to E\in W$$
5		prcofval.r	$$⊢\mathrm{Rel}R$$
6		prcofval.f	$$⊢\phi \to FRG$$
7		opex	$$⊢⟨F,G⟩\in \mathrm{V}$$
8	7	a1i	$$⊢\phi \to ⟨F,G⟩\in \mathrm{V}$$
9	1 2 3 4 8	prcofvala	Could not format ( ph -> ( <. D , E >. -o.F <. F , G >. ) = <. ( k e. B |-> ( k o.func <. F , G >. ) ) , ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` <. F , G >. ) ) ) ) >. ) : No typesetting found for |- ( ph -> ( <. D , E >. -o.F <. F , G >. ) = <. ( k e. B |-> ( k o.func <. F , G >. ) ) , ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` <. F , G >. ) ) ) ) >. ) with typecode |-
10	5	brrelex12i	$$⊢FRG\to \left(F\in \mathrm{V}\wedge G\in \mathrm{V}\right)$$
11		op1stg	$$⊢\left(F\in \mathrm{V}\wedge G\in \mathrm{V}\right)\to 1^{st}\left(⟨F,G⟩\right)=F$$
12	6 10 11	3syl	$$⊢\phi \to 1^{st}\left(⟨F,G⟩\right)=F$$
13	12	coeq2d	$$⊢\phi \to a\circ 1^{st}\left(⟨F,G⟩\right)=a\circ F$$
14	13	mpteq2dv	$$⊢\phi \to \left(a\in \left(kNl\right)⟼a\circ 1^{st}\left(⟨F,G⟩\right)\right)=\left(a\in \left(kNl\right)⟼a\circ F\right)$$
15	14	mpoeq3dv	$$⊢\phi \to \left(k\in B,l\in B⟼\left(a\in \left(kNl\right)⟼a\circ 1^{st}\left(⟨F,G⟩\right)\right)\right)=\left(k\in B,l\in B⟼\left(a\in \left(kNl\right)⟼a\circ F\right)\right)$$
16	15	opeq2d	$$⊢\phi \to ⟨\left(k\in B⟼k{\circ }_{\mathrm{func}}⟨F,G⟩\right),\left(k\in B,l\in B⟼\left(a\in \left(kNl\right)⟼a\circ 1^{st}\left(⟨F,G⟩\right)\right)\right)⟩=⟨\left(k\in B⟼k{\circ }_{\mathrm{func}}⟨F,G⟩\right),\left(k\in B,l\in B⟼\left(a\in \left(kNl\right)⟼a\circ F\right)\right)⟩$$
17	9 16	eqtrd	Could not format ( ph -> ( <. D , E >. -o.F <. F , G >. ) = <. ( k e. B |-> ( k o.func <. F , G >. ) ) , ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. F ) ) ) >. ) : No typesetting found for |- ( ph -> ( <. D , E >. -o.F <. F , G >. ) = <. ( k e. B |-> ( k o.func <. F , G >. ) ) , ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. F ) ) ) >. ) with typecode |-