Metamath Proof Explorer

Theorem xpcfucco2

Description: Value of composition in the binary product of categories of functors. (Contributed by Zhi Wang, 1-Oct-2025)

Ref Expression
Hypotheses xpcfuchom2.t 
|- T = ( ( B FuncCat C ) Xc. ( D FuncCat E ) )
xpcfucco2.o 
|- O = ( comp ` T )
xpcfucco2.f 
|- ( ph -> F e. ( M ( B Nat C ) P ) )
xpcfucco2.g 
|- ( ph -> G e. ( N ( D Nat E ) Q ) )
xpcfucco2.k 
|- ( ph -> K e. ( P ( B Nat C ) R ) )
xpcfucco2.l 
|- ( ph -> L e. ( Q ( D Nat E ) S ) )
Assertion xpcfucco2 
|- ( ph -> ( <. K , L >. ( <. <. M , N >. , <. P , Q >. >. O <. R , S >. ) <. F , G >. ) = <. ( K ( <. M , P >. ( comp ` ( B FuncCat C ) ) R ) F ) , ( L ( <. N , Q >. ( comp ` ( D FuncCat E ) ) S ) G ) >. )

Proof

Step Hyp Ref Expression
1 xpcfuchom2.t 
 |-  T = ( ( B FuncCat C ) Xc. ( D FuncCat E ) )
2 xpcfucco2.o 
 |-  O = ( comp ` T )
3 xpcfucco2.f 
 |-  ( ph -> F e. ( M ( B Nat C ) P ) )
4 xpcfucco2.g 
 |-  ( ph -> G e. ( N ( D Nat E ) Q ) )
5 xpcfucco2.k 
 |-  ( ph -> K e. ( P ( B Nat C ) R ) )
6 xpcfucco2.l 
 |-  ( ph -> L e. ( Q ( D Nat E ) S ) )
7 eqid 
 |-  ( B FuncCat C ) = ( B FuncCat C )
8 7 fucbas 
 |-  ( B Func C ) = ( Base ` ( B FuncCat C ) )
9 eqid 
 |-  ( D FuncCat E ) = ( D FuncCat E )
10 9 fucbas 
 |-  ( D Func E ) = ( Base ` ( D FuncCat E ) )
11 eqid 
 |-  ( B Nat C ) = ( B Nat C )
12 7 11 fuchom 
 |-  ( B Nat C ) = ( Hom ` ( B FuncCat C ) )
13 eqid 
 |-  ( D Nat E ) = ( D Nat E )
14 9 13 fuchom 
 |-  ( D Nat E ) = ( Hom ` ( D FuncCat E ) )
15 11 natrcl 
 |-  ( F e. ( M ( B Nat C ) P ) -> ( M e. ( B Func C ) /\ P e. ( B Func C ) ) )
16 3 15 syl 
 |-  ( ph -> ( M e. ( B Func C ) /\ P e. ( B Func C ) ) )
17 16 simpld 
 |-  ( ph -> M e. ( B Func C ) )
18 13 natrcl 
 |-  ( G e. ( N ( D Nat E ) Q ) -> ( N e. ( D Func E ) /\ Q e. ( D Func E ) ) )
19 4 18 syl 
 |-  ( ph -> ( N e. ( D Func E ) /\ Q e. ( D Func E ) ) )
20 19 simpld 
 |-  ( ph -> N e. ( D Func E ) )
21 16 simprd 
 |-  ( ph -> P e. ( B Func C ) )
22 19 simprd 
 |-  ( ph -> Q e. ( D Func E ) )
23 eqid 
 |-  ( comp ` ( B FuncCat C ) ) = ( comp ` ( B FuncCat C ) )
24 eqid 
 |-  ( comp ` ( D FuncCat E ) ) = ( comp ` ( D FuncCat E ) )
25 11 natrcl 
 |-  ( K e. ( P ( B Nat C ) R ) -> ( P e. ( B Func C ) /\ R e. ( B Func C ) ) )
26 5 25 syl 
 |-  ( ph -> ( P e. ( B Func C ) /\ R e. ( B Func C ) ) )
27 26 simprd 
 |-  ( ph -> R e. ( B Func C ) )
28 13 natrcl 
 |-  ( L e. ( Q ( D Nat E ) S ) -> ( Q e. ( D Func E ) /\ S e. ( D Func E ) ) )
29 6 28 syl 
 |-  ( ph -> ( Q e. ( D Func E ) /\ S e. ( D Func E ) ) )
30 29 simprd 
 |-  ( ph -> S e. ( D Func E ) )
31 1 8 10 12 14 17 20 21 22 23 24 2 27 30 3 4 5 6 xpcco2 
 |-  ( ph -> ( <. K , L >. ( <. <. M , N >. , <. P , Q >. >. O <. R , S >. ) <. F , G >. ) = <. ( K ( <. M , P >. ( comp ` ( B FuncCat C ) ) R ) F ) , ( L ( <. N , Q >. ( comp ` ( D FuncCat E ) ) S ) G ) >. )