Theorem thincfth

Description: A functor from a thin category is faithful. (Contributed by Zhi Wang, 1-Oct-2024)

	Ref	Expression
Hypotheses	thincfth.c	No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-
	thincfth.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
Assertion	thincfth	$$⊢\phi \to F\left(C\mathrm{Faith}D\right)G$$

Proof

Step	Hyp	Ref	Expression
1		thincfth.c	Could not format ( ph -> C e. ThinCat ) : No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-
2		thincfth.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
3	1	adantr	Could not format ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> C e. ThinCat ) : No typesetting found for |- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> C e. ThinCat ) with typecode |-
4		simprl	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\to x\in {\mathrm{Base}}_C$$
5		simprr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\to y\in {\mathrm{Base}}_C$$
6		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
7		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
8	3 4 5 6 7	thincmo	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\to {\exists }^{*}ff\in \left(x\mathrm{Hom}\left(C\right)y\right)$$
9		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
10	2	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\to F\left(C\mathrm{Func}D\right)G$$
11	6 7 9 10 4 5	funcf2	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\to \left(xGy\right):x\mathrm{Hom}\left(C\right)y⟶F\left(x\right)\mathrm{Hom}\left(D\right)F\left(y\right)$$
12		f1mo	$$⊢\left({\exists }^{*}ff\in \left(x\mathrm{Hom}\left(C\right)y\right)\wedge \left(xGy\right):x\mathrm{Hom}\left(C\right)y⟶F\left(x\right)\mathrm{Hom}\left(D\right)F\left(y\right)\right)\to \left(xGy\right):x\mathrm{Hom}\left(C\right)y\underset{1-1}{⟶}F\left(x\right)\mathrm{Hom}\left(D\right)F\left(y\right)$$
13	8 11 12	syl2anc	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\to \left(xGy\right):x\mathrm{Hom}\left(C\right)y\underset{1-1}{⟶}F\left(x\right)\mathrm{Hom}\left(D\right)F\left(y\right)$$
14	13	ralrimivva	$$⊢\phi \to \forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\left(xGy\right):x\mathrm{Hom}\left(C\right)y\underset{1-1}{⟶}F\left(x\right)\mathrm{Hom}\left(D\right)F\left(y\right)$$
15	6 7 9	isfth2	$$⊢F\left(C\mathrm{Faith}D\right)G\leftrightarrow \left(F\left(C\mathrm{Func}D\right)G\wedge \forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\left(xGy\right):x\mathrm{Hom}\left(C\right)y\underset{1-1}{⟶}F\left(x\right)\mathrm{Hom}\left(D\right)F\left(y\right)\right)$$
16	2 14 15	sylanbrc	$$⊢\phi \to F\left(C\mathrm{Faith}D\right)G$$