Theorem fulloppc

Description: The opposite functor of a full functor is also full. Proposition 3.43(d) in Adamek p. 39. (Contributed by Mario Carneiro, 27-Jan-2017)

	Ref	Expression
Hypotheses	fulloppc.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	fulloppc.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
	fulloppc.f	$$⊢\phi \to F\left(C\mathrm{Full}D\right)G$$
Assertion	fulloppc	$$⊢\phi \to F\left(O\mathrm{Full}P\right)tposG$$

Proof

Step	Hyp	Ref	Expression
1		fulloppc.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		fulloppc.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
3		fulloppc.f	$$⊢\phi \to F\left(C\mathrm{Full}D\right)G$$
4		fullfunc	$$⊢C\mathrm{Full}D\subseteq C\mathrm{Func}D$$
5	4	ssbri	$$⊢F\left(C\mathrm{Full}D\right)G\to F\left(C\mathrm{Func}D\right)G$$
6	3 5	syl	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
7	1 2 6	funcoppc	$$⊢\phi \to F\left(O\mathrm{Func}P\right)tposG$$
8		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
9		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
10		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
11	3	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\to F\left(C\mathrm{Full}D\right)G$$
12		simprr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\to y\in {\mathrm{Base}}_C$$
13		simprl	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\to x\in {\mathrm{Base}}_C$$
14	8 9 10 11 12 13	fullfo	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\to \left(yGx\right):y\mathrm{Hom}\left(C\right)x\underset{onto}{⟶}F\left(y\right)\mathrm{Hom}\left(D\right)F\left(x\right)$$
15		forn	$$⊢\left(yGx\right):y\mathrm{Hom}\left(C\right)x\underset{onto}{⟶}F\left(y\right)\mathrm{Hom}\left(D\right)F\left(x\right)\to \mathrm{ran}\left(yGx\right)=F\left(y\right)\mathrm{Hom}\left(D\right)F\left(x\right)$$
16	14 15	syl	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\to \mathrm{ran}\left(yGx\right)=F\left(y\right)\mathrm{Hom}\left(D\right)F\left(x\right)$$
17		ovtpos	$$⊢xtposGy=yGx$$
18	17	rneqi	$$⊢\mathrm{ran}\left(xtposGy\right)=\mathrm{ran}\left(yGx\right)$$
19	9 2	oppchom	$$⊢F\left(x\right)\mathrm{Hom}\left(P\right)F\left(y\right)=F\left(y\right)\mathrm{Hom}\left(D\right)F\left(x\right)$$
20	16 18 19	3eqtr4g	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\to \mathrm{ran}\left(xtposGy\right)=F\left(x\right)\mathrm{Hom}\left(P\right)F\left(y\right)$$
21	20	ralrimivva	$$⊢\phi \to \forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\mathrm{ran}\left(xtposGy\right)=F\left(x\right)\mathrm{Hom}\left(P\right)F\left(y\right)$$
22	1 8	oppcbas	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_O$$
23		eqid	$$⊢\mathrm{Hom}\left(P\right)=\mathrm{Hom}\left(P\right)$$
24	22 23	isfull	$$⊢F\left(O\mathrm{Full}P\right)tposG\leftrightarrow \left(F\left(O\mathrm{Func}P\right)tposG\wedge \forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\mathrm{ran}\left(xtposGy\right)=F\left(x\right)\mathrm{Hom}\left(P\right)F\left(y\right)\right)$$
25	7 21 24	sylanbrc	$$⊢\phi \to F\left(O\mathrm{Full}P\right)tposG$$