Metamath Proof Explorer

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 = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
fucofunca.q 
|- Q = ( C FuncCat E )
fucofunca.c 
|- ( ph -> C e. Cat )
fucofunca.d 
|- ( ph -> D e. Cat )
fucofunca.e 
|- ( ph -> E e. Cat )
Assertion fucofunca 
|- ( ph -> ( <. C , D >. o.F E ) e. ( T Func Q ) )

Proof

Step Hyp Ref Expression
1 fucofunca.t 
 |-  T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
2 fucofunca.q 
 |-  Q = ( C FuncCat E )
3 fucofunca.c 
 |-  ( ph -> C e. Cat )
4 fucofunca.d 
 |-  ( ph -> D e. Cat )
5 fucofunca.e 
 |-  ( ph -> E e. Cat )
6 eqidd 
 |-  ( ph -> ( <. C , D >. o.F E ) = ( <. C , D >. o.F E ) )
7 3 4 5 6 fucoelvv 
 |-  ( ph -> ( <. C , D >. o.F E ) e. ( _V X. _V ) )
8 1st2nd2 
 |-  ( ( <. 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 ) ) >. )
9 7 8 syl 
 |-  ( ph -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. )
10 1 2 9 3 4 5 fucofunc 
 |-  ( ph -> ( 1st ` ( <. C , D >. o.F E ) ) ( T Func Q ) ( 2nd ` ( <. C , D >. o.F E ) ) )
11 df-br 
 |-  ( ( 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 ) )
12 10 11 sylib 
 |-  ( ph -> <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. e. ( T Func Q ) )
13 9 12 eqeltrd 
 |-  ( ph -> ( <. C , D >. o.F E ) e. ( T Func Q ) )