Metamath Proof Explorer

Theorem funcres2c

Description: Condition for a functor to also be a functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017)

Ref Expression
Hypotheses funcres2c.a 
|- A = ( Base ` C )
funcres2c.e 
|- E = ( D |`s S )
funcres2c.d 
|- ( ph -> D e. Cat )
funcres2c.r 
|- ( ph -> S e. V )
funcres2c.1 
|- ( ph -> F : A --> S )
Assertion funcres2c 
|- ( ph -> ( F ( C Func D ) G <-> F ( C Func E ) G ) )

Proof

Step Hyp Ref Expression
1 funcres2c.a 
 |-  A = ( Base ` C )
2 funcres2c.e 
 |-  E = ( D |`s S )
3 funcres2c.d 
 |-  ( ph -> D e. Cat )
4 funcres2c.r 
 |-  ( ph -> S e. V )
5 funcres2c.1 
 |-  ( ph -> F : A --> S )
6 orc 
 |-  ( F ( C Func D ) G -> ( F ( C Func D ) G \/ F ( C Func E ) G ) )
7 6 a1i 
 |-  ( ph -> ( F ( C Func D ) G -> ( F ( C Func D ) G \/ F ( C Func E ) G ) ) )
8 olc 
 |-  ( F ( C Func E ) G -> ( F ( C Func D ) G \/ F ( C Func E ) G ) )
9 8 a1i 
 |-  ( ph -> ( F ( C Func E ) G -> ( F ( C Func D ) G \/ F ( C Func E ) G ) ) )
10 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
11 eqid 
 |-  ( Base ` D ) = ( Base ` D )
12 eqid 
 |-  ( Homf ` D ) = ( Homf ` D )
13 inss2 
 |-  ( S i^i ( Base ` D ) ) C_ ( Base ` D )
14 13 a1i 
 |-  ( ph -> ( S i^i ( Base ` D ) ) C_ ( Base ` D ) )
15 11 12 3 14 fullsubc 
 |-  ( ph -> ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) e. ( Subcat ` D ) )
16 15 adantr 
 |-  ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) -> ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) e. ( Subcat ` D ) )
17 12 11 homffn 
 |-  ( Homf ` D ) Fn ( ( Base ` D ) X. ( Base ` D ) )
18 xpss12 
 |-  ( ( ( S i^i ( Base ` D ) ) C_ ( Base ` D ) /\ ( S i^i ( Base ` D ) ) C_ ( Base ` D ) ) -> ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) C_ ( ( Base ` D ) X. ( Base ` D ) ) )
19 13 13 18 mp2an 
 |-  ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) C_ ( ( Base ` D ) X. ( Base ` D ) )
20 fnssres 
 |-  ( ( ( Homf ` D ) Fn ( ( Base ` D ) X. ( Base ` D ) ) /\ ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) C_ ( ( Base ` D ) X. ( Base ` D ) ) ) -> ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) Fn ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) )
21 17 19 20 mp2an 
 |-  ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) Fn ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) )
22 21 a1i 
 |-  ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) -> ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) Fn ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) )
23 5 adantr 
 |-  ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) -> F : A --> S )
24 23 ffnd 
 |-  ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) -> F Fn A )
25 23 frnd 
 |-  ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) -> ran F C_ S )
26 simpr 
 |-  ( ( ph /\ F ( C Func D ) G ) -> F ( C Func D ) G )
27 1 11 26 funcf1 
 |-  ( ( ph /\ F ( C Func D ) G ) -> F : A --> ( Base ` D ) )
28 27 frnd 
 |-  ( ( ph /\ F ( C Func D ) G ) -> ran F C_ ( Base ` D ) )
29 eqid 
 |-  ( Base ` E ) = ( Base ` E )
30 simpr 
 |-  ( ( ph /\ F ( C Func E ) G ) -> F ( C Func E ) G )
31 1 29 30 funcf1 
 |-  ( ( ph /\ F ( C Func E ) G ) -> F : A --> ( Base ` E ) )
32 31 frnd 
 |-  ( ( ph /\ F ( C Func E ) G ) -> ran F C_ ( Base ` E ) )
33 2 11 ressbasss 
 |-  ( Base ` E ) C_ ( Base ` D )
34 32 33 sstrdi 
 |-  ( ( ph /\ F ( C Func E ) G ) -> ran F C_ ( Base ` D ) )
35 28 34 jaodan 
 |-  ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) -> ran F C_ ( Base ` D ) )
36 25 35 ssind 
 |-  ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) -> ran F C_ ( S i^i ( Base ` D ) ) )
37 df-f 
 |-  ( F : A --> ( S i^i ( Base ` D ) ) <-> ( F Fn A /\ ran F C_ ( S i^i ( Base ` D ) ) ) )
38 24 36 37 sylanbrc 
 |-  ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) -> F : A --> ( S i^i ( Base ` D ) ) )
39 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
40 simpr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ F ( C Func D ) G ) -> F ( C Func D ) G )
41 simplrl 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ F ( C Func D ) G ) -> x e. A )
42 simplrr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ F ( C Func D ) G ) -> y e. A )
43 1 10 39 40 41 42 funcf2 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ F ( C Func D ) G ) -> ( x G y ) : ( x ( Hom ` C ) y ) --> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) )
44 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
45 simpr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ F ( C Func E ) G ) -> F ( C Func E ) G )
46 simplrl 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ F ( C Func E ) G ) -> x e. A )
47 simplrr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ F ( C Func E ) G ) -> y e. A )
48 1 10 44 45 46 47 funcf2 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ F ( C Func E ) G ) -> ( x G y ) : ( x ( Hom ` C ) y ) --> ( ( F ` x ) ( Hom ` E ) ( F ` y ) ) )
49 2 39 resshom 
 |-  ( S e. V -> ( Hom ` D ) = ( Hom ` E ) )
50 4 49 syl 
 |-  ( ph -> ( Hom ` D ) = ( Hom ` E ) )
51 50 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ F ( C Func E ) G ) -> ( Hom ` D ) = ( Hom ` E ) )
52 51 oveqd 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ F ( C Func E ) G ) -> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) = ( ( F ` x ) ( Hom ` E ) ( F ` y ) ) )
53 52 feq3d 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ F ( C Func E ) G ) -> ( ( x G y ) : ( x ( Hom ` C ) y ) --> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) <-> ( x G y ) : ( x ( Hom ` C ) y ) --> ( ( F ` x ) ( Hom ` E ) ( F ` y ) ) ) )
54 48 53 mpbird 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ F ( C Func E ) G ) -> ( x G y ) : ( x ( Hom ` C ) y ) --> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) )
55 43 54 jaodan 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) -> ( x G y ) : ( x ( Hom ` C ) y ) --> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) )
56 55 an32s 
 |-  ( ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) /\ ( x e. A /\ y e. A ) ) -> ( x G y ) : ( x ( Hom ` C ) y ) --> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) )
57 38 adantr 
 |-  ( ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) /\ ( x e. A /\ y e. A ) ) -> F : A --> ( S i^i ( Base ` D ) ) )
58 simprl 
 |-  ( ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) /\ ( x e. A /\ y e. A ) ) -> x e. A )
59 57 58 ffvelcdmd 
 |-  ( ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) /\ ( x e. A /\ y e. A ) ) -> ( F ` x ) e. ( S i^i ( Base ` D ) ) )
60 simprr 
 |-  ( ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) /\ ( x e. A /\ y e. A ) ) -> y e. A )
61 57 60 ffvelcdmd 
 |-  ( ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) /\ ( x e. A /\ y e. A ) ) -> ( F ` y ) e. ( S i^i ( Base ` D ) ) )
62 59 61 ovresd 
 |-  ( ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) /\ ( x e. A /\ y e. A ) ) -> ( ( F ` x ) ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) ( F ` y ) ) = ( ( F ` x ) ( Homf ` D ) ( F ` y ) ) )
63 59 elin2d 
 |-  ( ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) /\ ( x e. A /\ y e. A ) ) -> ( F ` x ) e. ( Base ` D ) )
64 61 elin2d 
 |-  ( ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) /\ ( x e. A /\ y e. A ) ) -> ( F ` y ) e. ( Base ` D ) )
65 12 11 39 63 64 homfval 
 |-  ( ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) /\ ( x e. A /\ y e. A ) ) -> ( ( F ` x ) ( Homf ` D ) ( F ` y ) ) = ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) )
66 62 65 eqtrd 
 |-  ( ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) /\ ( x e. A /\ y e. A ) ) -> ( ( F ` x ) ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) ( F ` y ) ) = ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) )
67 66 feq3d 
 |-  ( ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) /\ ( x e. A /\ y e. A ) ) -> ( ( x G y ) : ( x ( Hom ` C ) y ) --> ( ( F ` x ) ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) ( F ` y ) ) <-> ( x G y ) : ( x ( Hom ` C ) y ) --> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) ) )
68 56 67 mpbird 
 |-  ( ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) /\ ( x e. A /\ y e. A ) ) -> ( x G y ) : ( x ( Hom ` C ) y ) --> ( ( F ` x ) ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) ( F ` y ) ) )
69 1 10 16 22 38 68 funcres2b 
 |-  ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) -> ( F ( C Func D ) G <-> F ( C Func ( D |`cat ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) ) ) G ) )
70 eqidd 
 |-  ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) -> ( Homf ` C ) = ( Homf ` C ) )
71 eqidd 
 |-  ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) -> ( comf ` C ) = ( comf ` C ) )
72 11 ressinbas 
 |-  ( S e. V -> ( D |`s S ) = ( D |`s ( S i^i ( Base ` D ) ) ) )
73 4 72 syl 
 |-  ( ph -> ( D |`s S ) = ( D |`s ( S i^i ( Base ` D ) ) ) )
74 2 73 eqtrid 
 |-  ( ph -> E = ( D |`s ( S i^i ( Base ` D ) ) ) )
75 74 fveq2d 
 |-  ( ph -> ( Homf ` E ) = ( Homf ` ( D |`s ( S i^i ( Base ` D ) ) ) ) )
76 eqid 
 |-  ( D |`s ( S i^i ( Base ` D ) ) ) = ( D |`s ( S i^i ( Base ` D ) ) )
77 eqid 
 |-  ( D |`cat ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) ) = ( D |`cat ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) )
78 11 12 3 14 76 77 fullresc 
 |-  ( ph -> ( ( Homf ` ( D |`s ( S i^i ( Base ` D ) ) ) ) = ( Homf ` ( D |`cat ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) ) ) /\ ( comf ` ( D |`s ( S i^i ( Base ` D ) ) ) ) = ( comf ` ( D |`cat ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) ) ) ) )
79 78 simpld 
 |-  ( ph -> ( Homf ` ( D |`s ( S i^i ( Base ` D ) ) ) ) = ( Homf ` ( D |`cat ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) ) ) )
80 75 79 eqtrd 
 |-  ( ph -> ( Homf ` E ) = ( Homf ` ( D |`cat ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) ) ) )
81 80 adantr 
 |-  ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) -> ( Homf ` E ) = ( Homf ` ( D |`cat ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) ) ) )
82 74 fveq2d 
 |-  ( ph -> ( comf ` E ) = ( comf ` ( D |`s ( S i^i ( Base ` D ) ) ) ) )
83 78 simprd 
 |-  ( ph -> ( comf ` ( D |`s ( S i^i ( Base ` D ) ) ) ) = ( comf ` ( D |`cat ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) ) ) )
84 82 83 eqtrd 
 |-  ( ph -> ( comf ` E ) = ( comf ` ( D |`cat ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) ) ) )
85 84 adantr 
 |-  ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) -> ( comf ` E ) = ( comf ` ( D |`cat ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) ) ) )
86 df-br 
 |-  ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
87 funcrcl 
 |-  ( <. F , G >. e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
88 86 87 sylbi 
 |-  ( F ( C Func D ) G -> ( C e. Cat /\ D e. Cat ) )
89 88 simpld 
 |-  ( F ( C Func D ) G -> C e. Cat )
90 df-br 
 |-  ( F ( C Func E ) G <-> <. F , G >. e. ( C Func E ) )
91 funcrcl 
 |-  ( <. F , G >. e. ( C Func E ) -> ( C e. Cat /\ E e. Cat ) )
92 90 91 sylbi 
 |-  ( F ( C Func E ) G -> ( C e. Cat /\ E e. Cat ) )
93 92 simpld 
 |-  ( F ( C Func E ) G -> C e. Cat )
94 89 93 jaoi 
 |-  ( ( F ( C Func D ) G \/ F ( C Func E ) G ) -> C e. Cat )
95 94 elexd 
 |-  ( ( F ( C Func D ) G \/ F ( C Func E ) G ) -> C e. _V )
96 95 adantl 
 |-  ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) -> C e. _V )
97 2 ovexi 
 |-  E e. _V
98 97 a1i 
 |-  ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) -> E e. _V )
99 ovexd 
 |-  ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) -> ( D |`cat ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) ) e. _V )
100 70 71 81 85 96 96 98 99 funcpropd 
 |-  ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) -> ( C Func E ) = ( C Func ( D |`cat ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) ) ) )
101 100 breqd 
 |-  ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) -> ( F ( C Func E ) G <-> F ( C Func ( D |`cat ( ( Homf ` D ) |` ( ( S i^i ( Base ` D ) ) X. ( S i^i ( Base ` D ) ) ) ) ) ) G ) )
102 69 101 bitr4d 
 |-  ( ( ph /\ ( F ( C Func D ) G \/ F ( C Func E ) G ) ) -> ( F ( C Func D ) G <-> F ( C Func E ) G ) )
103 102 ex 
 |-  ( ph -> ( ( F ( C Func D ) G \/ F ( C Func E ) G ) -> ( F ( C Func D ) G <-> F ( C Func E ) G ) ) )
104 7 9 103 pm5.21ndd 
 |-  ( ph -> ( F ( C Func D ) G <-> F ( C Func E ) G ) )