coccom

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

	Ref	Expression
Hypotheses	islmd.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
	islmd.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	islmd.n	⊢ 𝑁 = ( 𝐷 Nat 𝐶 )
	islmd.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	concl.k	⊢ 𝐾 = ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 )
	concl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	concl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	concom.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	concom.m	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑌 𝐽 𝑍 ) )
	concom.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
	concom.o	⊢ · = ( comp ‘ 𝐶 )
	coccom.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 𝑁 𝐾 ) )
Assertion	coccom	⊢ ( 𝜑 → ( 𝑅 ‘ 𝑌 ) = ( ( 𝑅 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ · 𝑋 ) ( ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ 𝑀 ) ) )

Proof

Step	Hyp	Ref	Expression
1		islmd.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
2		islmd.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
3		islmd.n	⊢ 𝑁 = ( 𝐷 Nat 𝐶 )
4		islmd.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
5		concl.k	⊢ 𝐾 = ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 )
6		concl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
7		concl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8		concom.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
9		concom.m	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑌 𝐽 𝑍 ) )
10		concom.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
11		concom.o	⊢ · = ( comp ‘ 𝐶 )
12		coccom.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 𝑁 𝐾 ) )
13	3 12	nat1st2nd	⊢ ( 𝜑 → 𝑅 ∈ ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ ) )
14	3 13 4 10 11 7 8 9	nati	⊢ ( 𝜑 → ( ( 𝑅 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ · ( ( 1^st ‘ 𝐾 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ 𝑀 ) ) = ( ( ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑍 ) ‘ 𝑀 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ⟩ · ( ( 1^st ‘ 𝐾 ) ‘ 𝑍 ) ) ( 𝑅 ‘ 𝑌 ) ) )
15	3 13	natrcl2	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐷 Func 𝐶 ) ( 2^nd ‘ 𝐹 ) )
16	15	funcrcl3	⊢ ( 𝜑 → 𝐶 ∈ Cat )
17	15	funcrcl2	⊢ ( 𝜑 → 𝐷 ∈ Cat )
18	1 16 17 2 6 5 4 8	diag11	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) ‘ 𝑍 ) = 𝑋 )
19	18	oveq2d	⊢ ( 𝜑 → ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ · ( ( 1^st ‘ 𝐾 ) ‘ 𝑍 ) ) = ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ · 𝑋 ) )
20	19	oveqd	⊢ ( 𝜑 → ( ( 𝑅 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ · ( ( 1^st ‘ 𝐾 ) ‘ 𝑍 ) ) ( ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ 𝑀 ) ) = ( ( 𝑅 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ · 𝑋 ) ( ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ 𝑀 ) ) )
21	1 16 17 2 6 5 4 7	diag11	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) = 𝑋 )
22	21	opeq2d	⊢ ( 𝜑 → ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ⟩ = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , 𝑋 ⟩ )
23	22 18	oveq12d	⊢ ( 𝜑 → ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ⟩ · ( ( 1^st ‘ 𝐾 ) ‘ 𝑍 ) ) = ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , 𝑋 ⟩ · 𝑋 ) )
24		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
25	1 16 17 2 6 5 4 7 10 24 8 9	diag12	⊢ ( 𝜑 → ( ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑍 ) ‘ 𝑀 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) )
26		eqidd	⊢ ( 𝜑 → ( 𝑅 ‘ 𝑌 ) = ( 𝑅 ‘ 𝑌 ) )
27	23 25 26	oveq123d	⊢ ( 𝜑 → ( ( ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑍 ) ‘ 𝑀 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ⟩ · ( ( 1^st ‘ 𝐾 ) ‘ 𝑍 ) ) ( 𝑅 ‘ 𝑌 ) ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , 𝑋 ⟩ · 𝑋 ) ( 𝑅 ‘ 𝑌 ) ) )
28		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
29	4 2 15	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ 𝐴 )
30	29 7	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ∈ 𝐴 )
31	1 2 3 4 5 6 7 28 12	coccl	⊢ ( 𝜑 → ( 𝑅 ‘ 𝑌 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ( Hom ‘ 𝐶 ) 𝑋 ) )
32	2 28 24 16 30 11 6 31	catlid	⊢ ( 𝜑 → ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , 𝑋 ⟩ · 𝑋 ) ( 𝑅 ‘ 𝑌 ) ) = ( 𝑅 ‘ 𝑌 ) )
33	27 32	eqtrd	⊢ ( 𝜑 → ( ( ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑍 ) ‘ 𝑀 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ⟩ · ( ( 1^st ‘ 𝐾 ) ‘ 𝑍 ) ) ( 𝑅 ‘ 𝑌 ) ) = ( 𝑅 ‘ 𝑌 ) )
34	14 20 33	3eqtr3rd	⊢ ( 𝜑 → ( 𝑅 ‘ 𝑌 ) = ( ( 𝑅 ‘ 𝑍 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ⟩ · 𝑋 ) ( ( 𝑌 ( 2^nd ‘ 𝐹 ) 𝑍 ) ‘ 𝑀 ) ) )

Metamath Proof Explorer

Theorem coccom

Proof