Metamath Proof Explorer

Theorem fucbas

Description: The objects of the functor category are functors from C to D . (Contributed by Mario Carneiro, 6-Jan-2017) (Revised by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypothesis fucbas.q 
|- Q = ( C FuncCat D )
Assertion fucbas 
|- ( C Func D ) = ( Base ` Q )

Proof

Step Hyp Ref Expression
1 fucbas.q 
 |-  Q = ( C FuncCat D )
2 eqid 
 |-  ( C Func D ) = ( C Func D )
3 eqid 
 |-  ( C Nat D ) = ( C Nat 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 2 3 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 ( C Nat D ) h ) , a e. ( f ( C Nat D ) g ) |-> ( x e. ( Base ` C ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` D ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) )
10 1 2 3 4 5 6 7 9 fucval 
 |-  ( ( C e. Cat /\ D e. Cat ) -> Q = { <. ( Base ` ndx ) , ( C Func D ) >. , <. ( Hom ` ndx ) , ( C Nat D ) >. , <. ( comp ` ndx ) , ( comp ` Q ) >. } )
11 catstr 
 |-  { <. ( Base ` ndx ) , ( C Func D ) >. , <. ( Hom ` ndx ) , ( C Nat D ) >. , <. ( comp ` ndx ) , ( comp ` Q ) >. } Struct <. 1 , ; 1 5 >.
12 baseid 
 |-  Base = Slot ( Base ` ndx )
13 snsstp1 
 |-  { <. ( Base ` ndx ) , ( C Func D ) >. } C_ { <. ( Base ` ndx ) , ( C Func D ) >. , <. ( Hom ` ndx ) , ( C Nat D ) >. , <. ( comp ` ndx ) , ( comp ` Q ) >. }
14 ovexd 
 |-  ( ( C e. Cat /\ D e. Cat ) -> ( C Func D ) e. _V )
15 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
16 10 11 12 13 14 15 strfv3 
 |-  ( ( C e. Cat /\ D e. Cat ) -> ( Base ` Q ) = ( C Func D ) )
17 16 eqcomd 
 |-  ( ( C e. Cat /\ D e. Cat ) -> ( C Func D ) = ( Base ` Q ) )
18 base0 
 |-  (/) = ( Base ` (/) )
19 funcrcl 
 |-  ( f e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
20 19 con3i 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> -. f e. ( C Func D ) )
21 20 eq0rdv 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> ( C Func D ) = (/) )
22 fnfuc 
 |-  FuncCat Fn ( Cat X. Cat )
23 22 fndmi 
 |-  dom FuncCat = ( Cat X. Cat )
24 23 ndmov 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> ( C FuncCat D ) = (/) )
25 1 24 eqtrid 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> Q = (/) )
26 25 fveq2d 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> ( Base ` Q ) = ( Base ` (/) ) )
27 18 21 26 3eqtr4a 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> ( C Func D ) = ( Base ` Q ) )
28 17 27 pm2.61i 
 |-  ( C Func D ) = ( Base ` Q )