| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ffthres2c.a |
|- A = ( Base ` C ) |
| 2 |
|
ffthres2c.e |
|- E = ( D |`s S ) |
| 3 |
|
ffthres2c.d |
|- ( ph -> D e. Cat ) |
| 4 |
|
ffthres2c.r |
|- ( ph -> S e. V ) |
| 5 |
|
ffthres2c.1 |
|- ( ph -> F : A --> S ) |
| 6 |
1 2 3 4 5
|
funcres2c |
|- ( ph -> ( F ( C Func D ) G <-> F ( C Func E ) G ) ) |
| 7 |
|
eqid |
|- ( Hom ` D ) = ( Hom ` D ) |
| 8 |
2 7
|
resshom |
|- ( S e. V -> ( Hom ` D ) = ( Hom ` E ) ) |
| 9 |
4 8
|
syl |
|- ( ph -> ( Hom ` D ) = ( Hom ` E ) ) |
| 10 |
9
|
oveqd |
|- ( ph -> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) = ( ( F ` x ) ( Hom ` E ) ( F ` y ) ) ) |
| 11 |
10
|
eqeq2d |
|- ( ph -> ( ran ( x G y ) = ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) <-> ran ( x G y ) = ( ( F ` x ) ( Hom ` E ) ( F ` y ) ) ) ) |
| 12 |
11
|
2ralbidv |
|- ( ph -> ( A. x e. A A. y e. A ran ( x G y ) = ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) <-> A. x e. A A. y e. A ran ( x G y ) = ( ( F ` x ) ( Hom ` E ) ( F ` y ) ) ) ) |
| 13 |
6 12
|
anbi12d |
|- ( ph -> ( ( F ( C Func D ) G /\ A. x e. A A. y e. A ran ( x G y ) = ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) ) <-> ( F ( C Func E ) G /\ A. x e. A A. y e. A ran ( x G y ) = ( ( F ` x ) ( Hom ` E ) ( F ` y ) ) ) ) ) |
| 14 |
1 7
|
isfull |
|- ( F ( C Full D ) G <-> ( F ( C Func D ) G /\ A. x e. A A. y e. A ran ( x G y ) = ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) ) ) |
| 15 |
|
eqid |
|- ( Hom ` E ) = ( Hom ` E ) |
| 16 |
1 15
|
isfull |
|- ( F ( C Full E ) G <-> ( F ( C Func E ) G /\ A. x e. A A. y e. A ran ( x G y ) = ( ( F ` x ) ( Hom ` E ) ( F ` y ) ) ) ) |
| 17 |
13 14 16
|
3bitr4g |
|- ( ph -> ( F ( C Full D ) G <-> F ( C Full E ) G ) ) |