Theorem natcl

Description: A component of a natural transformation is a morphism. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	natrcl.1	|- N = ( C Nat D )
	natixp.2	|- ( ph -> A e. ( <. F , G >. N <. K , L >. ) )
	natixp.b	|- B = ( Base ` C )
	natixp.j	|- J = ( Hom ` D )
	natcl.1	|- ( ph -> X e. B )
Assertion	natcl	|- ( ph -> ( A ` X ) e. ( ( F ` X ) J ( K ` X ) ) )

Proof

Step	Hyp	Ref	Expression
1		natrcl.1	|- N = ( C Nat D )
2		natixp.2	|- ( ph -> A e. ( <. F , G >. N <. K , L >. ) )
3		natixp.b	|- B = ( Base ` C )
4		natixp.j	|- J = ( Hom ` D )
5		natcl.1	|- ( ph -> X e. B )
6	1 2 3 4	natixp	|- ( ph -> A e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) )
7		fveq2	|- ( x = X -> ( F ` x ) = ( F ` X ) )
8		fveq2	|- ( x = X -> ( K ` x ) = ( K ` X ) )
9	7 8	oveq12d	|- ( x = X -> ( ( F ` x ) J ( K ` x ) ) = ( ( F ` X ) J ( K ` X ) ) )
10	9	fvixp	|- ( ( A e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) /\ X e. B ) -> ( A ` X ) e. ( ( F ` X ) J ( K ` X ) ) )
11	6 5 10	syl2anc	|- ( ph -> ( A ` X ) e. ( ( F ` X ) J ( K ` X ) ) )