Theorem natfn

Description: A natural transformation is a function on the objects of C . (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 )
Assertion	natfn	|- ( ph -> A Fn B )

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		eqid	|- ( Hom ` D ) = ( Hom ` D )
5	1 2 3 4	natixp	|- ( ph -> A e. X_ x e. B ( ( F ` x ) ( Hom ` D ) ( K ` x ) ) )
6		ixpfn	|- ( A e. X_ x e. B ( ( F ` x ) ( Hom ` D ) ( K ` x ) ) -> A Fn B )
7	5 6	syl	|- ( ph -> A Fn B )