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 ) |
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 ) |