Theorem fucofval

Description: Value of the function giving the functor composition bifunctor. Hypotheses fucofval.c and fucofval.d are not redundant ( fucofvalne ). (Contributed by Zhi Wang, 29-Sep-2025)

	Ref	Expression
Hypotheses	fucofval.c	$$⊢\phi \to C\in T$$
	fucofval.d	$$⊢\phi \to D\in U$$
	fucofval.e	$$⊢\phi \to E\in V$$
	fucofval.o	No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = .o. ) with typecode |-
	fucofval.w	$$⊢\phi \to W=\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)$$
Assertion	fucofval	Could not format assertion : No typesetting found for |- ( ph -> .o. = <. ( o.func |` W ) , ( u e. W , v e. W |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fucofval.c	$$⊢\phi \to C\in T$$
2		fucofval.d	$$⊢\phi \to D\in U$$
3		fucofval.e	$$⊢\phi \to E\in V$$
4		fucofval.o	Could not format ( ph -> ( <. C , D >. o.F E ) = .o. ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = .o. ) with typecode |-
5		fucofval.w	$$⊢\phi \to W=\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)$$
6		opex	$$⊢⟨C,D⟩\in \mathrm{V}$$
7	6	a1i	$$⊢\phi \to ⟨C,D⟩\in \mathrm{V}$$
8		op1stg	$$⊢\left(C\in T\wedge D\in U\right)\to 1^{st}\left(⟨C,D⟩\right)=C$$
9	1 2 8	syl2anc	$$⊢\phi \to 1^{st}\left(⟨C,D⟩\right)=C$$
10		op2ndg	$$⊢\left(C\in T\wedge D\in U\right)\to 2^{nd}\left(⟨C,D⟩\right)=D$$
11	1 2 10	syl2anc	$$⊢\phi \to 2^{nd}\left(⟨C,D⟩\right)=D$$
12	7 9 11 3 4 5	fucofvalg	Could not format ( ph -> .o. = <. ( o.func |` W ) , ( u e. W , v e. W |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. ) : No typesetting found for |- ( ph -> .o. = <. ( o.func |` W ) , ( u e. W , v e. W |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. ) with typecode |-