Metamath Proof Explorer

Theorem fucofn22

Description: The morphism part of the functor composition bifunctor maps two natural transformations to a function on a base set. (Contributed by Zhi Wang, 30-Sep-2025)

Ref Expression
Hypotheses fuco22.o 
|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
fuco22.u 
|- ( ph -> U = <. <. K , L >. , <. F , G >. >. )
fuco22.v 
|- ( ph -> V = <. <. R , S >. , <. M , N >. >. )
fuco22.a 
|- ( ph -> A e. ( <. F , G >. ( C Nat D ) <. M , N >. ) )
fuco22.b 
|- ( ph -> B e. ( <. K , L >. ( D Nat E ) <. R , S >. ) )
Assertion fucofn22 
|- ( ph -> ( B ( U P V ) A ) Fn ( Base ` C ) )

Proof

Step Hyp Ref Expression
1 fuco22.o 
 |-  ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
2 fuco22.u 
 |-  ( ph -> U = <. <. K , L >. , <. F , G >. >. )
3 fuco22.v 
 |-  ( ph -> V = <. <. R , S >. , <. M , N >. >. )
4 fuco22.a 
 |-  ( ph -> A e. ( <. F , G >. ( C Nat D ) <. M , N >. ) )
5 fuco22.b 
 |-  ( ph -> B e. ( <. K , L >. ( D Nat E ) <. R , S >. ) )
6 ovex 
 |-  ( ( B ` ( M ` x ) ) ( <. ( K ` ( F ` x ) ) , ( K ` ( M ` x ) ) >. ( comp ` E ) ( R ` ( M ` x ) ) ) ( ( ( F ` x ) L ( M ` x ) ) ` ( A ` x ) ) ) e. _V
7 eqid 
 |-  ( 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 ) ) ) ) = ( 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 ) ) ) )
8 6 7 fnmpti 
 |-  ( 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 ) ) ) ) Fn ( Base ` C )
9 1 2 3 4 5 fuco22 
 |-  ( ph -> ( B ( U P V ) A ) = ( 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 ) ) ) ) )
10 9 fneq1d 
 |-  ( ph -> ( ( B ( U P V ) A ) Fn ( Base ` C ) <-> ( 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 ) ) ) ) Fn ( Base ` C ) ) )
11 8 10 mpbiri 
 |-  ( ph -> ( B ( U P V ) A ) Fn ( Base ` C ) )