Theorem prcofvala

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$$
	prcofvala.f	$$⊢\phi \to F\in U$$
Assertion	prcofvala	Could not format assertion : No typesetting found for |- ( ph -> ( <. D , E >. -o.F F ) = <. ( k e. B |-> ( k o.func F ) ) , ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` 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		prcofvala.f	$$⊢\phi \to F\in U$$
6		opex	$$⊢⟨D,E⟩\in \mathrm{V}$$
7	6	a1i	$$⊢\phi \to ⟨D,E⟩\in \mathrm{V}$$
8		op1stg	$$⊢\left(D\in V\wedge E\in W\right)\to 1^{st}\left(⟨D,E⟩\right)=D$$
9	3 4 8	syl2anc	$$⊢\phi \to 1^{st}\left(⟨D,E⟩\right)=D$$
10		op2ndg	$$⊢\left(D\in V\wedge E\in W\right)\to 2^{nd}\left(⟨D,E⟩\right)=E$$
11	3 4 10	syl2anc	$$⊢\phi \to 2^{nd}\left(⟨D,E⟩\right)=E$$
12	1 2 5 7 9 11	prcofvalg	Could not format ( ph -> ( <. D , E >. -o.F F ) = <. ( k e. B |-> ( k o.func F ) ) , ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) >. ) : No typesetting found for |- ( ph -> ( <. D , E >. -o.F F ) = <. ( k e. B |-> ( k o.func F ) ) , ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) >. ) with typecode |-