Metamath Proof Explorer

Theorem fuchom

Description: The morphisms in the functor category are natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses fucbas.q 
|- Q = ( C FuncCat D )
fuchom.n 
|- N = ( C Nat D )
Assertion fuchom 
|- N = ( Hom ` Q )

Proof

Step Hyp Ref Expression
1 fucbas.q 
 |-  Q = ( C FuncCat D )
2 fuchom.n 
 |-  N = ( C Nat D )
3 eqid 
 |-  ( C Func D ) = ( C Func D )
4 eqid 
 |-  ( Base ` C ) = ( Base ` C )
5 eqid 
 |-  ( comp ` D ) = ( comp ` D )
6 simpl 
 |-  ( ( C e. Cat /\ D e. Cat ) -> C e. Cat )
7 simpr 
 |-  ( ( C e. Cat /\ D e. Cat ) -> D e. Cat )
8 eqid 
 |-  ( comp ` Q ) = ( comp ` Q )
9 1 3 2 4 5 6 7 8 fuccofval 
 |-  ( ( C e. Cat /\ D e. Cat ) -> ( comp ` Q ) = ( v e. ( ( C Func D ) X. ( C Func D ) ) , h e. ( C Func D ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g N h ) , a e. ( f N g ) |-> ( x e. ( Base ` C ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` D ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) )
10 1 3 2 4 5 6 7 9 fucval 
 |-  ( ( C e. Cat /\ D e. Cat ) -> Q = { <. ( Base ` ndx ) , ( C Func D ) >. , <. ( Hom ` ndx ) , N >. , <. ( comp ` ndx ) , ( comp ` Q ) >. } )
11 catstr 
 |-  { <. ( Base ` ndx ) , ( C Func D ) >. , <. ( Hom ` ndx ) , N >. , <. ( comp ` ndx ) , ( comp ` Q ) >. } Struct <. 1 , ; 1 5 >.
12 homid 
 |-  Hom = Slot ( Hom ` ndx )
13 snsstp2 
 |-  { <. ( Hom ` ndx ) , N >. } C_ { <. ( Base ` ndx ) , ( C Func D ) >. , <. ( Hom ` ndx ) , N >. , <. ( comp ` ndx ) , ( comp ` Q ) >. }
14 2 ovexi 
 |-  N e. _V
15 14 a1i 
 |-  ( ( C e. Cat /\ D e. Cat ) -> N e. _V )
16 eqid 
 |-  ( Hom ` Q ) = ( Hom ` Q )
17 10 11 12 13 15 16 strfv3 
 |-  ( ( C e. Cat /\ D e. Cat ) -> ( Hom ` Q ) = N )
18 17 eqcomd 
 |-  ( ( C e. Cat /\ D e. Cat ) -> N = ( Hom ` Q ) )
19 df-hom 
 |-  Hom = Slot ; 1 4
20 19 str0 
 |-  (/) = ( Hom ` (/) )
21 2 natffn 
 |-  N Fn ( ( C Func D ) X. ( C Func D ) )
22 funcrcl 
 |-  ( f e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
23 22 con3i 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> -. f e. ( C Func D ) )
24 23 eq0rdv 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> ( C Func D ) = (/) )
25 24 xpeq2d 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> ( ( C Func D ) X. ( C Func D ) ) = ( ( C Func D ) X. (/) ) )
26 xp0 
 |-  ( ( C Func D ) X. (/) ) = (/)
27 25 26 eqtrdi 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> ( ( C Func D ) X. ( C Func D ) ) = (/) )
28 27 fneq2d 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> ( N Fn ( ( C Func D ) X. ( C Func D ) ) <-> N Fn (/) ) )
29 21 28 mpbii 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> N Fn (/) )
30 fn0 
 |-  ( N Fn (/) <-> N = (/) )
31 29 30 sylib 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> N = (/) )
32 fnfuc 
 |-  FuncCat Fn ( Cat X. Cat )
33 32 fndmi 
 |-  dom FuncCat = ( Cat X. Cat )
34 33 ndmov 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> ( C FuncCat D ) = (/) )
35 1 34 syl5eq 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> Q = (/) )
36 35 fveq2d 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> ( Hom ` Q ) = ( Hom ` (/) ) )
37 20 31 36 3eqtr4a 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> N = ( Hom ` Q ) )
38 18 37 pm2.61i 
 |-  N = ( Hom ` Q )