Theorem fullres2c

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

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

Proof

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 ) )