Theorem fthf1

Description: The morphism map of a faithful functor is an injection. (Contributed by Mario Carneiro, 27-Jan-2017)

	Ref	Expression
Hypotheses	isfth.b	$$⊢B={\mathrm{Base}}_C$$
	isfth.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	isfth.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
	fthf1.f	$$⊢\phi \to F\left(C\mathrm{Faith}D\right)G$$
	fthf1.x	$$⊢\phi \to X\in B$$
	fthf1.y	$$⊢\phi \to Y\in B$$
Assertion	fthf1	$$⊢\phi \to \left(XGY\right):XHY\underset{1-1}{⟶}F\left(X\right)JF\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		isfth.b	$$⊢B={\mathrm{Base}}_C$$
2		isfth.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
3		isfth.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
4		fthf1.f	$$⊢\phi \to F\left(C\mathrm{Faith}D\right)G$$
5		fthf1.x	$$⊢\phi \to X\in B$$
6		fthf1.y	$$⊢\phi \to Y\in B$$
7	1 2 3	isfth2	$$⊢F\left(C\mathrm{Faith}D\right)G\leftrightarrow \left(F\left(C\mathrm{Func}D\right)G\wedge \forall x\in B\forall y\in B\left(xGy\right):xHy\underset{1-1}{⟶}F\left(x\right)JF\left(y\right)\right)$$
8	7	simprbi	$$⊢F\left(C\mathrm{Faith}D\right)G\to \forall x\in B\forall y\in B\left(xGy\right):xHy\underset{1-1}{⟶}F\left(x\right)JF\left(y\right)$$
9	4 8	syl	$$⊢\phi \to \forall x\in B\forall y\in B\left(xGy\right):xHy\underset{1-1}{⟶}F\left(x\right)JF\left(y\right)$$
10	6	adantr	$$⊢\left(\phi \wedge x=X\right)\to Y\in B$$
11		simplr	$$⊢\left(\left(\phi \wedge x=X\right)\wedge y=Y\right)\to x=X$$
12		simpr	$$⊢\left(\left(\phi \wedge x=X\right)\wedge y=Y\right)\to y=Y$$
13	11 12	oveq12d	$$⊢\left(\left(\phi \wedge x=X\right)\wedge y=Y\right)\to xGy=XGY$$
14	11 12	oveq12d	$$⊢\left(\left(\phi \wedge x=X\right)\wedge y=Y\right)\to xHy=XHY$$
15	11	fveq2d	$$⊢\left(\left(\phi \wedge x=X\right)\wedge y=Y\right)\to F\left(x\right)=F\left(X\right)$$
16	12	fveq2d	$$⊢\left(\left(\phi \wedge x=X\right)\wedge y=Y\right)\to F\left(y\right)=F\left(Y\right)$$
17	15 16	oveq12d	$$⊢\left(\left(\phi \wedge x=X\right)\wedge y=Y\right)\to F\left(x\right)JF\left(y\right)=F\left(X\right)JF\left(Y\right)$$
18	13 14 17	f1eq123d	$$⊢\left(\left(\phi \wedge x=X\right)\wedge y=Y\right)\to \left(\left(xGy\right):xHy\underset{1-1}{⟶}F\left(x\right)JF\left(y\right)\leftrightarrow \left(XGY\right):XHY\underset{1-1}{⟶}F\left(X\right)JF\left(Y\right)\right)$$
19	10 18	rspcdv	$$⊢\left(\phi \wedge x=X\right)\to \left(\forall y\in B\left(xGy\right):xHy\underset{1-1}{⟶}F\left(x\right)JF\left(y\right)\to \left(XGY\right):XHY\underset{1-1}{⟶}F\left(X\right)JF\left(Y\right)\right)$$
20	5 19	rspcimdv	$$⊢\phi \to \left(\forall x\in B\forall y\in B\left(xGy\right):xHy\underset{1-1}{⟶}F\left(x\right)JF\left(y\right)\to \left(XGY\right):XHY\underset{1-1}{⟶}F\left(X\right)JF\left(Y\right)\right)$$
21	9 20	mpd	$$⊢\phi \to \left(XGY\right):XHY\underset{1-1}{⟶}F\left(X\right)JF\left(Y\right)$$