This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ph -> A e. ( <. F , G >. N <. K , L >. ) )
natixp.b 
|- B = ( Base ` C )
natixp.j 
|- J = ( Hom ` D )
Assertion natixp 
|- ( ph -> A e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) )

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 natixp.j 
 |-  J = ( Hom ` D )
5 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
6 eqid 
 |-  ( comp ` D ) = ( comp ` D )
7 1 natrcl 
 |-  ( A e. ( <. F , G >. N <. K , L >. ) -> ( <. F , G >. e. ( C Func D ) /\ <. K , L >. e. ( C Func D ) ) )
8 2 7 syl 
 |-  ( ph -> ( <. F , G >. e. ( C Func D ) /\ <. K , L >. e. ( C Func D ) ) )
9 8 simpld 
 |-  ( ph -> <. F , G >. e. ( C Func D ) )
10 df-br 
 |-  ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
11 9 10 sylibr 
 |-  ( ph -> F ( C Func D ) G )
12 8 simprd 
 |-  ( ph -> <. K , L >. e. ( C Func D ) )
13 df-br 
 |-  ( K ( C Func D ) L <-> <. K , L >. e. ( C Func D ) )
14 12 13 sylibr 
 |-  ( ph -> K ( C Func D ) L )
15 1 3 5 4 6 11 14 isnat 
 |-  ( ph -> ( A e. ( <. F , G >. N <. K , L >. ) <-> ( A e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) /\ A. x e. B A. y e. B A. z e. ( 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 
 |-  ( ph -> ( A e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) /\ A. x e. B A. y e. B A. z e. ( 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 
 |-  ( ph -> A e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) )