Metamath Proof Explorer

Theorem fuco112

Description: The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the morphism part of the composed functor. (Contributed by Zhi Wang, 3-Oct-2025)

Ref Expression
Hypotheses fuco11.o 
|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
fuco11.f 
|- ( ph -> F ( C Func D ) G )
fuco11.k 
|- ( ph -> K ( D Func E ) L )
fuco11.u 
|- ( ph -> U = <. <. K , L >. , <. F , G >. >. )
fuco11a.b 
|- B = ( Base ` C )
Assertion fuco112 
|- ( ph -> ( 2nd ` ( O ` U ) ) = ( x e. B , y e. B |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) )

Proof

Step Hyp Ref Expression
1 fuco11.o 
 |-  ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
2 fuco11.f 
 |-  ( ph -> F ( C Func D ) G )
3 fuco11.k 
 |-  ( ph -> K ( D Func E ) L )
4 fuco11.u 
 |-  ( ph -> U = <. <. K , L >. , <. F , G >. >. )
5 fuco11a.b 
 |-  B = ( Base ` C )
6 1 2 3 4 5 fuco11a 
 |-  ( ph -> ( O ` U ) = <. ( K o. F ) , ( x e. B , y e. B |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) >. )
7 6 fveq2d 
 |-  ( ph -> ( 2nd ` ( O ` U ) ) = ( 2nd ` <. ( K o. F ) , ( x e. B , y e. B |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) >. ) )
8 relfunc 
 |-  Rel ( D Func E )
9 8 brrelex1i 
 |-  ( K ( D Func E ) L -> K e. _V )
10 3 9 syl 
 |-  ( ph -> K e. _V )
11 relfunc 
 |-  Rel ( C Func D )
12 11 brrelex1i 
 |-  ( F ( C Func D ) G -> F e. _V )
13 2 12 syl 
 |-  ( ph -> F e. _V )
14 10 13 coexd 
 |-  ( ph -> ( K o. F ) e. _V )
15 5 fvexi 
 |-  B e. _V
16 15 15 mpoex 
 |-  ( x e. B , y e. B |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) e. _V
17 op2ndg 
 |-  ( ( ( K o. F ) e. _V /\ ( x e. B , y e. B |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) e. _V ) -> ( 2nd ` <. ( K o. F ) , ( x e. B , y e. B |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) >. ) = ( x e. B , y e. B |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) )
18 14 16 17 sylancl 
 |-  ( ph -> ( 2nd ` <. ( K o. F ) , ( x e. B , y e. B |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) >. ) = ( x e. B , y e. B |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) )
19 7 18 eqtrd 
 |-  ( ph -> ( 2nd ` ( O ` U ) ) = ( x e. B , y e. B |-> ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ) )