Theorem fucofunca

Description: The functor composition bifunctor is a functor. See also fucofunc . (Contributed by Zhi Wang, 10-Oct-2025)

	Ref	Expression
Hypotheses	fucofunca.t	$$⊢T=\left(D\mathrm{FuncCat}E\right){\times }_c\left(C\mathrm{FuncCat}D\right)$$
	fucofunca.q	$$⊢Q=C\mathrm{FuncCat}E$$
	fucofunca.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	fucofunca.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	fucofunca.e	$$⊢\phi \to E\in \mathrm{Cat}$$
Assertion	fucofunca	Could not format assertion : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) e. ( T Func Q ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fucofunca.t	$$⊢T=\left(D\mathrm{FuncCat}E\right){\times }_c\left(C\mathrm{FuncCat}D\right)$$
2		fucofunca.q	$$⊢Q=C\mathrm{FuncCat}E$$
3		fucofunca.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		fucofunca.d	$$⊢\phi \to D\in \mathrm{Cat}$$
5		fucofunca.e	$$⊢\phi \to E\in \mathrm{Cat}$$
6		eqidd	Could not format ( ph -> ( <. C , D >. o.F E ) = ( <. C , D >. o.F E ) ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = ( <. C , D >. o.F E ) ) with typecode |-
7	3 4 5 6	fucoelvv	Could not format ( ph -> ( <. C , D >. o.F E ) e. ( _V X. _V ) ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) e. ( _V X. _V ) ) with typecode |-
8		1st2nd2	Could not format ( ( <. C , D >. o.F E ) e. ( _V X. _V ) -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. ) : No typesetting found for |- ( ( <. C , D >. o.F E ) e. ( _V X. _V ) -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. ) with typecode |-
9	7 8	syl	Could not format ( ph -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. ) with typecode |-
10	1 2 9 3 4 5	fucofunc	Could not format ( ph -> ( 1st ` ( <. C , D >. o.F E ) ) ( T Func Q ) ( 2nd ` ( <. C , D >. o.F E ) ) ) : No typesetting found for |- ( ph -> ( 1st ` ( <. C , D >. o.F E ) ) ( T Func Q ) ( 2nd ` ( <. C , D >. o.F E ) ) ) with typecode |-
11		df-br	Could not format ( ( 1st ` ( <. C , D >. o.F E ) ) ( T Func Q ) ( 2nd ` ( <. C , D >. o.F E ) ) <-> <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. e. ( T Func Q ) ) : No typesetting found for |- ( ( 1st ` ( <. C , D >. o.F E ) ) ( T Func Q ) ( 2nd ` ( <. C , D >. o.F E ) ) <-> <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. e. ( T Func Q ) ) with typecode |-
12	10 11	sylib	Could not format ( ph -> <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. e. ( T Func Q ) ) : No typesetting found for |- ( ph -> <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. e. ( T Func Q ) ) with typecode |-
13	9 12	eqeltrd	Could not format ( ph -> ( <. C , D >. o.F E ) e. ( T Func Q ) ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) e. ( T Func Q ) ) with typecode |-