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 φ A F G N K L
natixp.b B = Base C
Assertion natfn φ A Fn B

Proof

Step Hyp Ref Expression
1 natrcl.1 N = C Nat D
2 natixp.2 φ A F G N K L
3 natixp.b B = Base C
4 eqid Hom D = Hom D
5 1 2 3 4 natixp φ A x B F x Hom D K x
6 ixpfn A x B F x Hom D K x A Fn B
7 5 6 syl φ A Fn B