Metamath Proof Explorer

Theorem fucof21

Description: The morphism part of the functor composition bifunctor maps a hom-set of the product category into a set of natural transformations. (Contributed by Zhi Wang, 30-Sep-2025)

Ref Expression
Hypotheses fucof21.o 
|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
fucof21.t 
|- T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
fucof21.j 
|- J = ( Hom ` T )
fucof21.w 
|- ( ph -> W = ( ( D Func E ) X. ( C Func D ) ) )
fucof21.u 
|- ( ph -> U e. W )
fucof21.v 
|- ( ph -> V e. W )
Assertion fucof21 
|- ( ph -> ( U P V ) : ( U J V ) --> ( ( O ` U ) ( C Nat E ) ( O ` V ) ) )

Proof

Step Hyp Ref Expression
1 fucof21.o 
 |-  ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
2 fucof21.t 
 |-  T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
3 fucof21.j 
 |-  J = ( Hom ` T )
4 fucof21.w 
 |-  ( ph -> W = ( ( D Func E ) X. ( C Func D ) ) )
5 fucof21.u 
 |-  ( ph -> U e. W )
6 fucof21.v 
 |-  ( ph -> V e. W )
7 relfunc 
 |-  Rel ( D Func E )
8 relfunc 
 |-  Rel ( C Func D )
9 4 5 7 8 fuco2eld3 
 |-  ( ph -> ( ( 1st ` ( 1st ` U ) ) ( D Func E ) ( 2nd ` ( 1st ` U ) ) /\ ( 1st ` ( 2nd ` U ) ) ( C Func D ) ( 2nd ` ( 2nd ` U ) ) ) )
10 9 simprd 
 |-  ( ph -> ( 1st ` ( 2nd ` U ) ) ( C Func D ) ( 2nd ` ( 2nd ` U ) ) )
11 9 simpld 
 |-  ( ph -> ( 1st ` ( 1st ` U ) ) ( D Func E ) ( 2nd ` ( 1st ` U ) ) )
12 4 5 7 8 fuco2eld2 
 |-  ( ph -> U = <. <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. , <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. >. )
13 4 6 7 8 fuco2eld3 
 |-  ( ph -> ( ( 1st ` ( 1st ` V ) ) ( D Func E ) ( 2nd ` ( 1st ` V ) ) /\ ( 1st ` ( 2nd ` V ) ) ( C Func D ) ( 2nd ` ( 2nd ` V ) ) ) )
14 13 simprd 
 |-  ( ph -> ( 1st ` ( 2nd ` V ) ) ( C Func D ) ( 2nd ` ( 2nd ` V ) ) )
15 13 simpld 
 |-  ( ph -> ( 1st ` ( 1st ` V ) ) ( D Func E ) ( 2nd ` ( 1st ` V ) ) )
16 4 6 7 8 fuco2eld2 
 |-  ( ph -> V = <. <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. , <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. >. )
17 1 10 11 12 14 15 16 fuco21 
 |-  ( ph -> ( U P V ) = ( b e. ( <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. ( D Nat E ) <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. ) , a e. ( <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. ( C Nat D ) <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( ( 1st ` ( 2nd ` V ) ) ` x ) ) ( <. ( ( 1st ` ( 1st ` U ) ) ` ( ( 1st ` ( 2nd ` U ) ) ` x ) ) , ( ( 1st ` ( 1st ` U ) ) ` ( ( 1st ` ( 2nd ` V ) ) ` x ) ) >. ( comp ` E ) ( ( 1st ` ( 1st ` V ) ) ` ( ( 1st ` ( 2nd ` V ) ) ` x ) ) ) ( ( ( ( 1st ` ( 2nd ` U ) ) ` x ) ( 2nd ` ( 1st ` U ) ) ( ( 1st ` ( 2nd ` V ) ) ` x ) ) ` ( a ` x ) ) ) ) ) )
18 1 adantr 
 |-  ( ( ph /\ ( b e. ( <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. ( D Nat E ) <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. ) /\ a e. ( <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. ( C Nat D ) <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. ) ) ) -> ( <. C , D >. o.F E ) = <. O , P >. )
19 12 adantr 
 |-  ( ( ph /\ ( b e. ( <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. ( D Nat E ) <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. ) /\ a e. ( <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. ( C Nat D ) <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. ) ) ) -> U = <. <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. , <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. >. )
20 16 adantr 
 |-  ( ( ph /\ ( b e. ( <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. ( D Nat E ) <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. ) /\ a e. ( <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. ( C Nat D ) <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. ) ) ) -> V = <. <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. , <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. >. )
21 simprr 
 |-  ( ( ph /\ ( b e. ( <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. ( D Nat E ) <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. ) /\ a e. ( <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. ( C Nat D ) <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. ) ) ) -> a e. ( <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. ( C Nat D ) <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. ) )
22 simprl 
 |-  ( ( ph /\ ( b e. ( <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. ( D Nat E ) <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. ) /\ a e. ( <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. ( C Nat D ) <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. ) ) ) -> b e. ( <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. ( D Nat E ) <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. ) )
23 18 19 20 21 22 fuco22 
 |-  ( ( ph /\ ( b e. ( <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. ( D Nat E ) <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. ) /\ a e. ( <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. ( C Nat D ) <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. ) ) ) -> ( b ( U P V ) a ) = ( x e. ( Base ` C ) |-> ( ( b ` ( ( 1st ` ( 2nd ` V ) ) ` x ) ) ( <. ( ( 1st ` ( 1st ` U ) ) ` ( ( 1st ` ( 2nd ` U ) ) ` x ) ) , ( ( 1st ` ( 1st ` U ) ) ` ( ( 1st ` ( 2nd ` V ) ) ` x ) ) >. ( comp ` E ) ( ( 1st ` ( 1st ` V ) ) ` ( ( 1st ` ( 2nd ` V ) ) ` x ) ) ) ( ( ( ( 1st ` ( 2nd ` U ) ) ` x ) ( 2nd ` ( 1st ` U ) ) ( ( 1st ` ( 2nd ` V ) ) ` x ) ) ` ( a ` x ) ) ) ) )
24 18 21 22 19 20 fuco22nat 
 |-  ( ( ph /\ ( b e. ( <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. ( D Nat E ) <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. ) /\ a e. ( <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. ( C Nat D ) <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. ) ) ) -> ( b ( U P V ) a ) e. ( ( O ` U ) ( C Nat E ) ( O ` V ) ) )
25 23 24 eqeltrrd 
 |-  ( ( ph /\ ( b e. ( <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. ( D Nat E ) <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. ) /\ a e. ( <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. ( C Nat D ) <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. ) ) ) -> ( x e. ( Base ` C ) |-> ( ( b ` ( ( 1st ` ( 2nd ` V ) ) ` x ) ) ( <. ( ( 1st ` ( 1st ` U ) ) ` ( ( 1st ` ( 2nd ` U ) ) ` x ) ) , ( ( 1st ` ( 1st ` U ) ) ` ( ( 1st ` ( 2nd ` V ) ) ` x ) ) >. ( comp ` E ) ( ( 1st ` ( 1st ` V ) ) ` ( ( 1st ` ( 2nd ` V ) ) ` x ) ) ) ( ( ( ( 1st ` ( 2nd ` U ) ) ` x ) ( 2nd ` ( 1st ` U ) ) ( ( 1st ` ( 2nd ` V ) ) ` x ) ) ` ( a ` x ) ) ) ) e. ( ( O ` U ) ( C Nat E ) ( O ` V ) ) )
26 2 xpcfucbas 
 |-  ( ( D Func E ) X. ( C Func D ) ) = ( Base ` T )
27 5 4 eleqtrd 
 |-  ( ph -> U e. ( ( D Func E ) X. ( C Func D ) ) )
28 6 4 eleqtrd 
 |-  ( ph -> V e. ( ( D Func E ) X. ( C Func D ) ) )
29 2 26 3 27 28 xpcfuchom 
 |-  ( ph -> ( U J V ) = ( ( ( 1st ` U ) ( D Nat E ) ( 1st ` V ) ) X. ( ( 2nd ` U ) ( C Nat D ) ( 2nd ` V ) ) ) )
30 12 fveq2d 
 |-  ( ph -> ( 1st ` U ) = ( 1st ` <. <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. , <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. >. ) )
31 opex 
 |-  <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. e. _V
32 opex 
 |-  <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. e. _V
33 31 32 op1st 
 |-  ( 1st ` <. <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. , <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. >. ) = <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >.
34 30 33 eqtrdi 
 |-  ( ph -> ( 1st ` U ) = <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. )
35 16 fveq2d 
 |-  ( ph -> ( 1st ` V ) = ( 1st ` <. <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. , <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. >. ) )
36 opex 
 |-  <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. e. _V
37 opex 
 |-  <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. e. _V
38 36 37 op1st 
 |-  ( 1st ` <. <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. , <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. >. ) = <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >.
39 35 38 eqtrdi 
 |-  ( ph -> ( 1st ` V ) = <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. )
40 34 39 oveq12d 
 |-  ( ph -> ( ( 1st ` U ) ( D Nat E ) ( 1st ` V ) ) = ( <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. ( D Nat E ) <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. ) )
41 12 fveq2d 
 |-  ( ph -> ( 2nd ` U ) = ( 2nd ` <. <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. , <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. >. ) )
42 31 32 op2nd 
 |-  ( 2nd ` <. <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. , <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. >. ) = <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >.
43 41 42 eqtrdi 
 |-  ( ph -> ( 2nd ` U ) = <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. )
44 16 fveq2d 
 |-  ( ph -> ( 2nd ` V ) = ( 2nd ` <. <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. , <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. >. ) )
45 36 37 op2nd 
 |-  ( 2nd ` <. <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. , <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. >. ) = <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >.
46 44 45 eqtrdi 
 |-  ( ph -> ( 2nd ` V ) = <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. )
47 43 46 oveq12d 
 |-  ( ph -> ( ( 2nd ` U ) ( C Nat D ) ( 2nd ` V ) ) = ( <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. ( C Nat D ) <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. ) )
48 40 47 xpeq12d 
 |-  ( ph -> ( ( ( 1st ` U ) ( D Nat E ) ( 1st ` V ) ) X. ( ( 2nd ` U ) ( C Nat D ) ( 2nd ` V ) ) ) = ( ( <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. ( D Nat E ) <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. ) X. ( <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. ( C Nat D ) <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. ) ) )
49 29 48 eqtrd 
 |-  ( ph -> ( U J V ) = ( ( <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. ( D Nat E ) <. ( 1st ` ( 1st ` V ) ) , ( 2nd ` ( 1st ` V ) ) >. ) X. ( <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. ( C Nat D ) <. ( 1st ` ( 2nd ` V ) ) , ( 2nd ` ( 2nd ` V ) ) >. ) ) )
50 17 25 49 fmpodg 
 |-  ( ph -> ( U P V ) : ( U J V ) --> ( ( O ` U ) ( C Nat E ) ( O ` V ) ) )