concl

Description: A natural transformation from a constant functor of an object maps to morphisms whose domain is the object. Therefore, the range of the second component of a cone are morphisms with a common domain. (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	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	concl.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	concl.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐾 𝑁 𝐹 ) )
Assertion	concl	⊢ ( 𝜑 → ( 𝑅 ‘ 𝑌 ) ∈ ( 𝑋 𝐻 ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) )

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		concl.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
9		concl.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐾 𝑁 𝐹 ) )
10	3 9	nat1st2nd	⊢ ( 𝜑 → 𝑅 ∈ ( ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ) )
11	3 10 4 8 7	natcl	⊢ ( 𝜑 → ( 𝑅 ‘ 𝑌 ) ∈ ( ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) 𝐻 ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) )
12	3 10	natrcl3	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐷 Func 𝐶 ) ( 2^nd ‘ 𝐹 ) )
13	12	funcrcl3	⊢ ( 𝜑 → 𝐶 ∈ Cat )
14	12	funcrcl2	⊢ ( 𝜑 → 𝐷 ∈ Cat )
15	1 13 14 2 6 5 4 7	diag11	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) = 𝑋 )
16	15	oveq1d	⊢ ( 𝜑 → ( ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) 𝐻 ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) = ( 𝑋 𝐻 ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) )
17	11 16	eleqtrd	⊢ ( 𝜑 → ( 𝑅 ‘ 𝑌 ) ∈ ( 𝑋 𝐻 ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) )

Metamath Proof Explorer

Theorem concl

Proof