Metamath Proof Explorer

Theorem xpcfuccocl

Description: The composition of two natural transformations is a natural transformation. (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 xpcfuccocl 
|- ( ph -> ( <. K , L >. ( <. <. M , N >. , <. P , Q >. >. O <. R , S >. ) <. F , G >. ) e. ( ( M ( B Nat C ) R ) X. ( N ( D Nat E ) S ) ) )

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 1 2 3 4 5 6 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 ) >. )
8 eqid 
 |-  ( B FuncCat C ) = ( B FuncCat C )
9 eqid 
 |-  ( B Nat C ) = ( B Nat C )
10 eqid 
 |-  ( comp ` ( B FuncCat C ) ) = ( comp ` ( B FuncCat C ) )
11 8 9 10 3 5 fuccocl 
 |-  ( ph -> ( K ( <. M , P >. ( comp ` ( B FuncCat C ) ) R ) F ) e. ( M ( B Nat C ) R ) )
12 eqid 
 |-  ( D FuncCat E ) = ( D FuncCat E )
13 eqid 
 |-  ( D Nat E ) = ( D Nat E )
14 eqid 
 |-  ( comp ` ( D FuncCat E ) ) = ( comp ` ( D FuncCat E ) )
15 12 13 14 4 6 fuccocl 
 |-  ( ph -> ( L ( <. N , Q >. ( comp ` ( D FuncCat E ) ) S ) G ) e. ( N ( D Nat E ) S ) )
16 11 15 opelxpd 
 |-  ( ph -> <. ( K ( <. M , P >. ( comp ` ( B FuncCat C ) ) R ) F ) , ( L ( <. N , Q >. ( comp ` ( D FuncCat E ) ) S ) G ) >. e. ( ( M ( B Nat C ) R ) X. ( N ( D Nat E ) S ) ) )
17 7 16 eqeltrd 
 |-  ( ph -> ( <. K , L >. ( <. <. M , N >. , <. P , Q >. >. O <. R , S >. ) <. F , G >. ) e. ( ( M ( B Nat C ) R ) X. ( N ( D Nat E ) S ) ) )