Metamath Proof Explorer


Theorem natixp

Description: A natural transformation is a function from the objects of C to homomorphisms from F ( x ) to G ( x ) . (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
natixp.j J = Hom D
Assertion natixp φ A x B F x J K x

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 natixp.j J = Hom D
5 eqid Hom C = Hom C
6 eqid comp D = comp D
7 1 natrcl A F G N K L F G C Func D K L C Func D
8 2 7 syl φ F G C Func D K L C Func D
9 8 simpld φ F G C Func D
10 df-br F C Func D G F G C Func D
11 9 10 sylibr φ F C Func D G
12 8 simprd φ K L C Func D
13 df-br K C Func D L K L C Func D
14 12 13 sylibr φ K C Func D L
15 1 3 5 4 6 11 14 isnat φ A F G N K L A x B F x J K x x B y B z x Hom C y A y F x F y comp D K y x G y z = x L y z F x K x comp D K y A x
16 2 15 mpbid φ A x B F x J K x x B y B z x Hom C y A y F x F y comp D K y x G y z = x L y z F x K x comp D K y A x
17 16 simpld φ A x B F x J K x