Theorem fthpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same faithful functors. (Contributed by Mario Carneiro, 27-Jan-2017)

	Ref	Expression
Hypotheses	fullpropd.1	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(A\right)={\mathrm{Hom}}_{𝑓}\left(B\right)$$
	fullpropd.2	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(A\right)={\mathrm{comp}}_{𝑓}\left(B\right)$$
	fullpropd.3	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
	fullpropd.4	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
	fullpropd.a	$$⊢\phi \to A\in V$$
	fullpropd.b	$$⊢\phi \to B\in V$$
	fullpropd.c	$$⊢\phi \to C\in V$$
	fullpropd.d	$$⊢\phi \to D\in V$$
Assertion	fthpropd	$$⊢\phi \to A\mathrm{Faith}C=B\mathrm{Faith}D$$

Proof

Step	Hyp	Ref	Expression
1		fullpropd.1	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(A\right)={\mathrm{Hom}}_{𝑓}\left(B\right)$$
2		fullpropd.2	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(A\right)={\mathrm{comp}}_{𝑓}\left(B\right)$$
3		fullpropd.3	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
4		fullpropd.4	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
5		fullpropd.a	$$⊢\phi \to A\in V$$
6		fullpropd.b	$$⊢\phi \to B\in V$$
7		fullpropd.c	$$⊢\phi \to C\in V$$
8		fullpropd.d	$$⊢\phi \to D\in V$$
9		relfth	$$⊢\mathrm{Rel}\left(A\mathrm{Faith}C\right)$$
10		relfth	$$⊢\mathrm{Rel}\left(B\mathrm{Faith}D\right)$$
11	1 2 3 4 5 6 7 8	funcpropd	$$⊢\phi \to A\mathrm{Func}C=B\mathrm{Func}D$$
12	11	breqd	$$⊢\phi \to \left(f\left(A\mathrm{Func}C\right)g\leftrightarrow f\left(B\mathrm{Func}D\right)g\right)$$
13	1	homfeqbas	$$⊢\phi \to {\mathrm{Base}}_A={\mathrm{Base}}_B$$
14	13	raleqdv	$$⊢\phi \to \left(\forall y\in {\mathrm{Base}}_A\mathrm{Fun}{\left(xgy\right)}^{-1}\leftrightarrow \forall y\in {\mathrm{Base}}_B\mathrm{Fun}{\left(xgy\right)}^{-1}\right)$$
15	13 14	raleqbidv	$$⊢\phi \to \left(\forall x\in {\mathrm{Base}}_A\forall y\in {\mathrm{Base}}_A\mathrm{Fun}{\left(xgy\right)}^{-1}\leftrightarrow \forall x\in {\mathrm{Base}}_B\forall y\in {\mathrm{Base}}_B\mathrm{Fun}{\left(xgy\right)}^{-1}\right)$$
16	12 15	anbi12d	$$⊢\phi \to \left(\left(f\left(A\mathrm{Func}C\right)g\wedge \forall x\in {\mathrm{Base}}_A\forall y\in {\mathrm{Base}}_A\mathrm{Fun}{\left(xgy\right)}^{-1}\right)\leftrightarrow \left(f\left(B\mathrm{Func}D\right)g\wedge \forall x\in {\mathrm{Base}}_B\forall y\in {\mathrm{Base}}_B\mathrm{Fun}{\left(xgy\right)}^{-1}\right)\right)$$
17		eqid	$$⊢{\mathrm{Base}}_A={\mathrm{Base}}_A$$
18	17	isfth	$$⊢f\left(A\mathrm{Faith}C\right)g\leftrightarrow \left(f\left(A\mathrm{Func}C\right)g\wedge \forall x\in {\mathrm{Base}}_A\forall y\in {\mathrm{Base}}_A\mathrm{Fun}{\left(xgy\right)}^{-1}\right)$$
19		eqid	$$⊢{\mathrm{Base}}_B={\mathrm{Base}}_B$$
20	19	isfth	$$⊢f\left(B\mathrm{Faith}D\right)g\leftrightarrow \left(f\left(B\mathrm{Func}D\right)g\wedge \forall x\in {\mathrm{Base}}_B\forall y\in {\mathrm{Base}}_B\mathrm{Fun}{\left(xgy\right)}^{-1}\right)$$
21	16 18 20	3bitr4g	$$⊢\phi \to \left(f\left(A\mathrm{Faith}C\right)g\leftrightarrow f\left(B\mathrm{Faith}D\right)g\right)$$
22	9 10 21	eqbrrdiv	$$⊢\phi \to A\mathrm{Faith}C=B\mathrm{Faith}D$$