Metamath Proof Explorer

Theorem coccom

Description: A co-cone to a diagram commutes with the diagram. (Contributed by Zhi Wang, 13-Nov-2025)

Ref Expression
Hypotheses islmd.l 
|- L = ( C DiagFunc D )
islmd.a 
|- A = ( Base ` C )
islmd.n 
|- N = ( D Nat C )
islmd.b 
|- B = ( Base ` D )
concl.k 
|- K = ( ( 1st ` L ) ` X )
concl.x 
|- ( ph -> X e. A )
concl.y 
|- ( ph -> Y e. B )
concom.z 
|- ( ph -> Z e. B )
concom.m 
|- ( ph -> M e. ( Y J Z ) )
concom.j 
|- J = ( Hom ` D )
concom.o 
|- .x. = ( comp ` C )
coccom.r 
|- ( ph -> R e. ( F N K ) )
Assertion coccom 
|- ( ph -> ( R ` Y ) = ( ( R ` Z ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` F ) ` Z ) >. .x. X ) ( ( Y ( 2nd ` F ) Z ) ` M ) ) )

Proof

Step Hyp Ref Expression
1 islmd.l 
 |-  L = ( C DiagFunc D )
2 islmd.a 
 |-  A = ( Base ` C )
3 islmd.n 
 |-  N = ( D Nat C )
4 islmd.b 
 |-  B = ( Base ` D )
5 concl.k 
 |-  K = ( ( 1st ` L ) ` X )
6 concl.x 
 |-  ( ph -> X e. A )
7 concl.y 
 |-  ( ph -> Y e. B )
8 concom.z 
 |-  ( ph -> Z e. B )
9 concom.m 
 |-  ( ph -> M e. ( Y J Z ) )
10 concom.j 
 |-  J = ( Hom ` D )
11 concom.o 
 |-  .x. = ( comp ` C )
12 coccom.r 
 |-  ( ph -> R e. ( F N K ) )
13 3 12 nat1st2nd 
 |-  ( ph -> R e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` K ) , ( 2nd ` K ) >. ) )
14 3 13 4 10 11 7 8 9 nati 
 |-  ( ph -> ( ( R ` Z ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` F ) ` Z ) >. .x. ( ( 1st ` K ) ` Z ) ) ( ( Y ( 2nd ` F ) Z ) ` M ) ) = ( ( ( Y ( 2nd ` K ) Z ) ` M ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` K ) ` Y ) >. .x. ( ( 1st ` K ) ` Z ) ) ( R ` Y ) ) )
15 3 13 natrcl2 
 |-  ( ph -> ( 1st ` F ) ( D Func C ) ( 2nd ` F ) )
16 15 funcrcl3 
 |-  ( ph -> C e. Cat )
17 15 funcrcl2 
 |-  ( ph -> D e. Cat )
18 1 16 17 2 6 5 4 8 diag11 
 |-  ( ph -> ( ( 1st ` K ) ` Z ) = X )
19 18 oveq2d 
 |-  ( ph -> ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` F ) ` Z ) >. .x. ( ( 1st ` K ) ` Z ) ) = ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` F ) ` Z ) >. .x. X ) )
20 19 oveqd 
 |-  ( ph -> ( ( R ` Z ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` F ) ` Z ) >. .x. ( ( 1st ` K ) ` Z ) ) ( ( Y ( 2nd ` F ) Z ) ` M ) ) = ( ( R ` Z ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` F ) ` Z ) >. .x. X ) ( ( Y ( 2nd ` F ) Z ) ` M ) ) )
21 1 16 17 2 6 5 4 7 diag11 
 |-  ( ph -> ( ( 1st ` K ) ` Y ) = X )
22 21 opeq2d 
 |-  ( ph -> <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` K ) ` Y ) >. = <. ( ( 1st ` F ) ` Y ) , X >. )
23 22 18 oveq12d 
 |-  ( ph -> ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` K ) ` Y ) >. .x. ( ( 1st ` K ) ` Z ) ) = ( <. ( ( 1st ` F ) ` Y ) , X >. .x. X ) )
24 eqid 
 |-  ( Id ` C ) = ( Id ` C )
25 1 16 17 2 6 5 4 7 10 24 8 9 diag12 
 |-  ( ph -> ( ( Y ( 2nd ` K ) Z ) ` M ) = ( ( Id ` C ) ` X ) )
26 eqidd 
 |-  ( ph -> ( R ` Y ) = ( R ` Y ) )
27 23 25 26 oveq123d 
 |-  ( ph -> ( ( ( Y ( 2nd ` K ) Z ) ` M ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` K ) ` Y ) >. .x. ( ( 1st ` K ) ` Z ) ) ( R ` Y ) ) = ( ( ( Id ` C ) ` X ) ( <. ( ( 1st ` F ) ` Y ) , X >. .x. X ) ( R ` Y ) ) )
28 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
29 4 2 15 funcf1 
 |-  ( ph -> ( 1st ` F ) : B --> A )
30 29 7 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` F ) ` Y ) e. A )
31 1 2 3 4 5 6 7 28 12 coccl 
 |-  ( ph -> ( R ` Y ) e. ( ( ( 1st ` F ) ` Y ) ( Hom ` C ) X ) )
32 2 28 24 16 30 11 6 31 catlid 
 |-  ( ph -> ( ( ( Id ` C ) ` X ) ( <. ( ( 1st ` F ) ` Y ) , X >. .x. X ) ( R ` Y ) ) = ( R ` Y ) )
33 27 32 eqtrd 
 |-  ( ph -> ( ( ( Y ( 2nd ` K ) Z ) ` M ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` K ) ` Y ) >. .x. ( ( 1st ` K ) ` Z ) ) ( R ` Y ) ) = ( R ` Y ) )
34 14 20 33 3eqtr3rd 
 |-  ( ph -> ( R ` Y ) = ( ( R ` Z ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` F ) ` Z ) >. .x. X ) ( ( Y ( 2nd ` F ) Z ) ` M ) ) )