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

Metamath Proof Explorer

Theorem natffn

Description: The natural transformation set operation is a well-defined function. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypothesis natrcl.1 
|- N = ( C Nat D )
Assertion natffn 
|- N Fn ( ( C Func D ) X. ( C Func D ) )

Proof

Step Hyp Ref Expression
1 natrcl.1 
 |-  N = ( C Nat D )
2 eqid 
 |-  ( Base ` C ) = ( Base ` C )
3 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
4 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
5 eqid 
 |-  ( comp ` D ) = ( comp ` D )
6 1 2 3 4 5 natfval 
 |-  N = ( f e. ( C Func D ) , g e. ( C Func D ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. h e. ( x ( Hom ` C ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } )
7 ovex 
 |-  ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) e. _V
8 7 rgenw 
 |-  A. x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) e. _V
9 ixpexg 
 |-  ( A. x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) e. _V -> X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) e. _V )
10 8 9 ax-mp 
 |-  X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) e. _V
11 10 rabex 
 |-  { a e. X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. h e. ( x ( Hom ` C ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } e. _V
12 11 csbex 
 |-  [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. h e. ( x ( Hom ` C ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } e. _V
13 12 csbex 
 |-  [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. h e. ( x ( Hom ` C ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } e. _V
14 6 13 fnmpoi 
 |-  N Fn ( ( C Func D ) X. ( C Func D ) )