Metamath Proof Explorer

Theorem funcres2

Description: A functor into a restricted category is also a functor into the whole category. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Assertion funcres2 
|- ( R e. ( Subcat ` D ) -> ( C Func ( D |`cat R ) ) C_ ( C Func D ) )

Proof

Step Hyp Ref Expression
1 relfunc 
 |-  Rel ( C Func ( D |`cat R ) )
2 1 a1i 
 |-  ( R e. ( Subcat ` D ) -> Rel ( C Func ( D |`cat R ) ) )
3 simpr 
 |-  ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> f ( C Func ( D |`cat R ) ) g )
4 eqid 
 |-  ( Base ` C ) = ( Base ` C )
5 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
6 simpl 
 |-  ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> R e. ( Subcat ` D ) )
7 eqidd 
 |-  ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> dom dom R = dom dom R )
8 6 7 subcfn 
 |-  ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> R Fn ( dom dom R X. dom dom R ) )
9 eqid 
 |-  ( Base ` ( D |`cat R ) ) = ( Base ` ( D |`cat R ) )
10 4 9 3 funcf1 
 |-  ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> f : ( Base ` C ) --> ( Base ` ( D |`cat R ) ) )
11 eqid 
 |-  ( D |`cat R ) = ( D |`cat R )
12 eqid 
 |-  ( Base ` D ) = ( Base ` D )
13 subcrcl 
 |-  ( R e. ( Subcat ` D ) -> D e. Cat )
14 13 adantr 
 |-  ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> D e. Cat )
15 6 8 12 subcss1 
 |-  ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> dom dom R C_ ( Base ` D ) )
16 11 12 14 8 15 rescbas 
 |-  ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> dom dom R = ( Base ` ( D |`cat R ) ) )
17 16 feq3d 
 |-  ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> ( f : ( Base ` C ) --> dom dom R <-> f : ( Base ` C ) --> ( Base ` ( D |`cat R ) ) ) )
18 10 17 mpbird 
 |-  ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> f : ( Base ` C ) --> dom dom R )
19 eqid 
 |-  ( Hom ` ( D |`cat R ) ) = ( Hom ` ( D |`cat R ) )
20 simplr 
 |-  ( ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> f ( C Func ( D |`cat R ) ) g )
21 simprl 
 |-  ( ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x e. ( Base ` C ) )
22 simprr 
 |-  ( ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> y e. ( Base ` C ) )
23 4 5 19 20 21 22 funcf2 
 |-  ( ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x g y ) : ( x ( Hom ` C ) y ) --> ( ( f ` x ) ( Hom ` ( D |`cat R ) ) ( f ` y ) ) )
24 11 12 14 8 15 reschom 
 |-  ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> R = ( Hom ` ( D |`cat R ) ) )
25 24 adantr 
 |-  ( ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> R = ( Hom ` ( D |`cat R ) ) )
26 25 oveqd 
 |-  ( ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( f ` x ) R ( f ` y ) ) = ( ( f ` x ) ( Hom ` ( D |`cat R ) ) ( f ` y ) ) )
27 26 feq3d 
 |-  ( ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( x g y ) : ( x ( Hom ` C ) y ) --> ( ( f ` x ) R ( f ` y ) ) <-> ( x g y ) : ( x ( Hom ` C ) y ) --> ( ( f ` x ) ( Hom ` ( D |`cat R ) ) ( f ` y ) ) ) )
28 23 27 mpbird 
 |-  ( ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x g y ) : ( x ( Hom ` C ) y ) --> ( ( f ` x ) R ( f ` y ) ) )
29 4 5 6 8 18 28 funcres2b 
 |-  ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> ( f ( C Func D ) g <-> f ( C Func ( D |`cat R ) ) g ) )
30 3 29 mpbird 
 |-  ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> f ( C Func D ) g )
31 30 ex 
 |-  ( R e. ( Subcat ` D ) -> ( f ( C Func ( D |`cat R ) ) g -> f ( C Func D ) g ) )
32 df-br 
 |-  ( f ( C Func ( D |`cat R ) ) g <-> <. f , g >. e. ( C Func ( D |`cat R ) ) )
33 df-br 
 |-  ( f ( C Func D ) g <-> <. f , g >. e. ( C Func D ) )
34 31 32 33 3imtr3g 
 |-  ( R e. ( Subcat ` D ) -> ( <. f , g >. e. ( C Func ( D |`cat R ) ) -> <. f , g >. e. ( C Func D ) ) )
35 2 34 relssdv 
 |-  ( R e. ( Subcat ` D ) -> ( C Func ( D |`cat R ) ) C_ ( C Func D ) )