Theorem fthoppc

Description: The opposite functor of a faithful functor is also faithful. Proposition 3.43(c) 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)$$
	fthoppc.f	$$⊢\phi \to F\left(C\mathrm{Faith}D\right)G$$
Assertion	fthoppc	$$⊢\phi \to F\left(O\mathrm{Faith}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		fthoppc.f	$$⊢\phi \to F\left(C\mathrm{Faith}D\right)G$$
4		fthfunc	$$⊢C\mathrm{Faith}D\subseteq C\mathrm{Func}D$$
5	4	ssbri	$$⊢F\left(C\mathrm{Faith}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(C\right)=\mathrm{Hom}\left(C\right)$$
10		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\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{Faith}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	fthf1	$$⊢\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{1-1}{⟶}F\left(y\right)\mathrm{Hom}\left(D\right)F\left(x\right)$$
15		df-f1	$$⊢\left(yGx\right):y\mathrm{Hom}\left(C\right)x\underset{1-1}{⟶}F\left(y\right)\mathrm{Hom}\left(D\right)F\left(x\right)\leftrightarrow \left(\left(yGx\right):y\mathrm{Hom}\left(C\right)x⟶F\left(y\right)\mathrm{Hom}\left(D\right)F\left(x\right)\wedge \mathrm{Fun}{\left(yGx\right)}^{-1}\right)$$
16	15	simprbi	$$⊢\left(yGx\right):y\mathrm{Hom}\left(C\right)x\underset{1-1}{⟶}F\left(y\right)\mathrm{Hom}\left(D\right)F\left(x\right)\to \mathrm{Fun}{\left(yGx\right)}^{-1}$$
17	14 16	syl	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\to \mathrm{Fun}{\left(yGx\right)}^{-1}$$
18		ovtpos	$$⊢xtposGy=yGx$$
19	18	cnveqi	$$⊢{\left(xtposGy\right)}^{-1}={\left(yGx\right)}^{-1}$$
20	19	funeqi	$$⊢\mathrm{Fun}{\left(xtposGy\right)}^{-1}\leftrightarrow \mathrm{Fun}{\left(yGx\right)}^{-1}$$
21	17 20	sylibr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\to \mathrm{Fun}{\left(xtposGy\right)}^{-1}$$
22	21	ralrimivva	$$⊢\phi \to \forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\mathrm{Fun}{\left(xtposGy\right)}^{-1}$$
23	1 8	oppcbas	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_O$$
24	23	isfth	$$⊢F\left(O\mathrm{Faith}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{Fun}{\left(xtposGy\right)}^{-1}\right)$$
25	7 22 24	sylanbrc	$$⊢\phi \to F\left(O\mathrm{Faith}P\right)tposG$$