Theorem ffthf1o

Description: The morphism map of a fully faithful functor is a bijection. (Contributed by Mario Carneiro, 29-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)$$
	ffthf1o.f	$$⊢\phi \to F\left(\left(C\mathrm{Full}D\right)\cap \left(C\mathrm{Faith}D\right)\right)G$$
	ffthf1o.x	$$⊢\phi \to X\in B$$
	ffthf1o.y	$$⊢\phi \to Y\in B$$
Assertion	ffthf1o	$$⊢\phi \to \left(XGY\right):XHY\underset{1-1\; onto}{⟶}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		ffthf1o.f	$$⊢\phi \to F\left(\left(C\mathrm{Full}D\right)\cap \left(C\mathrm{Faith}D\right)\right)G$$
5		ffthf1o.x	$$⊢\phi \to X\in B$$
6		ffthf1o.y	$$⊢\phi \to Y\in B$$
7		brin	$$⊢F\left(\left(C\mathrm{Full}D\right)\cap \left(C\mathrm{Faith}D\right)\right)G\leftrightarrow \left(F\left(C\mathrm{Full}D\right)G\wedge F\left(C\mathrm{Faith}D\right)G\right)$$
8	4 7	sylib	$$⊢\phi \to \left(F\left(C\mathrm{Full}D\right)G\wedge F\left(C\mathrm{Faith}D\right)G\right)$$
9	8	simprd	$$⊢\phi \to F\left(C\mathrm{Faith}D\right)G$$
10	1 2 3 9 5 6	fthf1	$$⊢\phi \to \left(XGY\right):XHY\underset{1-1}{⟶}F\left(X\right)JF\left(Y\right)$$
11	8	simpld	$$⊢\phi \to F\left(C\mathrm{Full}D\right)G$$
12	1 3 2 11 5 6	fullfo	$$⊢\phi \to \left(XGY\right):XHY\underset{onto}{⟶}F\left(X\right)JF\left(Y\right)$$
13		df-f1o	$$⊢\left(XGY\right):XHY\underset{1-1\; onto}{⟶}F\left(X\right)JF\left(Y\right)\leftrightarrow \left(\left(XGY\right):XHY\underset{1-1}{⟶}F\left(X\right)JF\left(Y\right)\wedge \left(XGY\right):XHY\underset{onto}{⟶}F\left(X\right)JF\left(Y\right)\right)$$
14	10 12 13	sylanbrc	$$⊢\phi \to \left(XGY\right):XHY\underset{1-1\; onto}{⟶}F\left(X\right)JF\left(Y\right)$$