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	\|- 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 )
	concl.h	\|- H = ( Hom ` C )
	concl.r	\|- ( ph -> R e. ( K N F ) )
Assertion	concl	\|- ( ph -> ( R ` Y ) e. ( X H ( ( 1st ` F ) ` Y ) ) )

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		concl.h	\|- H = ( Hom ` C )
9		concl.r	\|- ( ph -> R e. ( K N F ) )
10	3 9	nat1st2nd	\|- ( ph -> R e. ( <. ( 1st ` K ) , ( 2nd ` K ) >. N <. ( 1st ` F ) , ( 2nd ` F ) >. ) )
11	3 10 4 8 7	natcl	\|- ( ph -> ( R ` Y ) e. ( ( ( 1st ` K ) ` Y ) H ( ( 1st ` F ) ` Y ) ) )
12	3 10	natrcl3	\|- ( ph -> ( 1st ` F ) ( D Func C ) ( 2nd ` F ) )
13	12	funcrcl3	\|- ( ph -> C e. Cat )
14	12	funcrcl2	\|- ( ph -> D e. Cat )
15	1 13 14 2 6 5 4 7	diag11	\|- ( ph -> ( ( 1st ` K ) ` Y ) = X )
16	15	oveq1d	\|- ( ph -> ( ( ( 1st ` K ) ` Y ) H ( ( 1st ` F ) ` Y ) ) = ( X H ( ( 1st ` F ) ` Y ) ) )
17	11 16	eleqtrd	\|- ( ph -> ( R ` Y ) e. ( X H ( ( 1st ` F ) ` Y ) ) )

Metamath Proof Explorer

Theorem concl

Proof