Metamath Proof Explorer


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 )