Metamath Proof Explorer

Theorem fuco23alem

Description: The naturality property ( nati ) in category E . (Contributed by Zhi Wang, 3-Oct-2025)

Ref Expression
Hypotheses fuco23a.a 
|- ( ph -> A e. ( <. F , G >. ( C Nat D ) <. M , N >. ) )
fuco23a.b 
|- ( ph -> B e. ( <. K , L >. ( D Nat E ) <. R , S >. ) )
fuco23a.x 
|- ( ph -> X e. ( Base ` C ) )
fuco23alem.o 
|- .x. = ( comp ` E )
Assertion fuco23alem 
|- ( ph -> ( ( B ` ( M ` X ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. .x. ( R ` ( M ` X ) ) ) ( ( ( F ` X ) L ( M ` X ) ) ` ( A ` X ) ) ) = ( ( ( ( F ` X ) S ( M ` X ) ) ` ( A ` X ) ) ( <. ( K ` ( F ` X ) ) , ( R ` ( F ` X ) ) >. .x. ( R ` ( M ` X ) ) ) ( B ` ( F ` X ) ) ) )

Proof

Step Hyp Ref Expression
1 fuco23a.a 
 |-  ( ph -> A e. ( <. F , G >. ( C Nat D ) <. M , N >. ) )
2 fuco23a.b 
 |-  ( ph -> B e. ( <. K , L >. ( D Nat E ) <. R , S >. ) )
3 fuco23a.x 
 |-  ( ph -> X e. ( Base ` C ) )
4 fuco23alem.o 
 |-  .x. = ( comp ` E )
5 eqid 
 |-  ( D Nat E ) = ( D Nat E )
6 eqid 
 |-  ( Base ` D ) = ( Base ` D )
7 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
8 eqid 
 |-  ( Base ` C ) = ( Base ` C )
9 eqid 
 |-  ( C Nat D ) = ( C Nat D )
10 9 1 natrcl2 
 |-  ( ph -> F ( C Func D ) G )
11 8 6 10 funcf1 
 |-  ( ph -> F : ( Base ` C ) --> ( Base ` D ) )
12 11 3 ffvelcdmd 
 |-  ( ph -> ( F ` X ) e. ( Base ` D ) )
13 9 1 natrcl3 
 |-  ( ph -> M ( C Func D ) N )
14 8 6 13 funcf1 
 |-  ( ph -> M : ( Base ` C ) --> ( Base ` D ) )
15 14 3 ffvelcdmd 
 |-  ( ph -> ( M ` X ) e. ( Base ` D ) )
16 9 1 8 7 3 natcl 
 |-  ( ph -> ( A ` X ) e. ( ( F ` X ) ( Hom ` D ) ( M ` X ) ) )
17 5 2 6 7 4 12 15 16 nati 
 |-  ( ph -> ( ( B ` ( M ` X ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. .x. ( R ` ( M ` X ) ) ) ( ( ( F ` X ) L ( M ` X ) ) ` ( A ` X ) ) ) = ( ( ( ( F ` X ) S ( M ` X ) ) ` ( A ` X ) ) ( <. ( K ` ( F ` X ) ) , ( R ` ( F ` X ) ) >. .x. ( R ` ( M ` X ) ) ) ( B ` ( F ` X ) ) ) )