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={\mathrm{Base}}_C$$
	ffthres2c.e	$$⊢E=D{\upharpoonright }_{𝑠}S$$
	ffthres2c.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	ffthres2c.r	$$⊢\phi \to S\in V$$
	ffthres2c.1	$$⊢\phi \to F:A⟶S$$
Assertion	fullres2c	$$⊢\phi \to \left(F\left(C\mathrm{Full}D\right)G\leftrightarrow F\left(C\mathrm{Full}E\right)G\right)$$

Proof

Step	Hyp	Ref	Expression
1		ffthres2c.a	$$⊢A={\mathrm{Base}}_C$$
2		ffthres2c.e	$$⊢E=D{\upharpoonright }_{𝑠}S$$
3		ffthres2c.d	$$⊢\phi \to D\in \mathrm{Cat}$$
4		ffthres2c.r	$$⊢\phi \to S\in V$$
5		ffthres2c.1	$$⊢\phi \to F:A⟶S$$
6	1 2 3 4 5	funcres2c	$$⊢\phi \to \left(F\left(C\mathrm{Func}D\right)G\leftrightarrow F\left(C\mathrm{Func}E\right)G\right)$$
7		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
8	2 7	resshom	$$⊢S\in V\to \mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(E\right)$$
9	4 8	syl	$$⊢\phi \to \mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(E\right)$$
10	9	oveqd	$$⊢\phi \to F\left(x\right)\mathrm{Hom}\left(D\right)F\left(y\right)=F\left(x\right)\mathrm{Hom}\left(E\right)F\left(y\right)$$
11	10	eqeq2d	$$⊢\phi \to \left(\mathrm{ran}\left(xGy\right)=F\left(x\right)\mathrm{Hom}\left(D\right)F\left(y\right)\leftrightarrow \mathrm{ran}\left(xGy\right)=F\left(x\right)\mathrm{Hom}\left(E\right)F\left(y\right)\right)$$
12	11	2ralbidv	$$⊢\phi \to \left(\forall x\in A\forall y\in A\mathrm{ran}\left(xGy\right)=F\left(x\right)\mathrm{Hom}\left(D\right)F\left(y\right)\leftrightarrow \forall x\in A\forall y\in A\mathrm{ran}\left(xGy\right)=F\left(x\right)\mathrm{Hom}\left(E\right)F\left(y\right)\right)$$
13	6 12	anbi12d	$$⊢\phi \to \left(\left(F\left(C\mathrm{Func}D\right)G\wedge \forall x\in A\forall y\in A\mathrm{ran}\left(xGy\right)=F\left(x\right)\mathrm{Hom}\left(D\right)F\left(y\right)\right)\leftrightarrow \left(F\left(C\mathrm{Func}E\right)G\wedge \forall x\in A\forall y\in A\mathrm{ran}\left(xGy\right)=F\left(x\right)\mathrm{Hom}\left(E\right)F\left(y\right)\right)\right)$$
14	1 7	isfull	$$⊢F\left(C\mathrm{Full}D\right)G\leftrightarrow \left(F\left(C\mathrm{Func}D\right)G\wedge \forall x\in A\forall y\in A\mathrm{ran}\left(xGy\right)=F\left(x\right)\mathrm{Hom}\left(D\right)F\left(y\right)\right)$$
15		eqid	$$⊢\mathrm{Hom}\left(E\right)=\mathrm{Hom}\left(E\right)$$
16	1 15	isfull	$$⊢F\left(C\mathrm{Full}E\right)G\leftrightarrow \left(F\left(C\mathrm{Func}E\right)G\wedge \forall x\in A\forall y\in A\mathrm{ran}\left(xGy\right)=F\left(x\right)\mathrm{Hom}\left(E\right)F\left(y\right)\right)$$
17	13 14 16	3bitr4g	$$⊢\phi \to \left(F\left(C\mathrm{Full}D\right)G\leftrightarrow F\left(C\mathrm{Full}E\right)G\right)$$