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 = ( Base ` C )
	isfth.h	|- H = ( Hom ` C )
	isfth.j	|- J = ( Hom ` D )
	ffthf1o.f	|- ( ph -> F ( ( C Full D ) i^i ( C Faith D ) ) G )
	ffthf1o.x	|- ( ph -> X e. B )
	ffthf1o.y	|- ( ph -> Y e. B )
Assertion	ffthf1o	|- ( ph -> ( X G Y ) : ( X H Y ) -1-1-onto-> ( ( F ` X ) J ( F ` Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		isfth.b	|- B = ( Base ` C )
2		isfth.h	|- H = ( Hom ` C )
3		isfth.j	|- J = ( Hom ` D )
4		ffthf1o.f	|- ( ph -> F ( ( C Full D ) i^i ( C Faith D ) ) G )
5		ffthf1o.x	|- ( ph -> X e. B )
6		ffthf1o.y	|- ( ph -> Y e. B )
7		brin	|- ( F ( ( C Full D ) i^i ( C Faith D ) ) G <-> ( F ( C Full D ) G /\ F ( C Faith D ) G ) )
8	4 7	sylib	|- ( ph -> ( F ( C Full D ) G /\ F ( C Faith D ) G ) )
9	8	simprd	|- ( ph -> F ( C Faith D ) G )
10	1 2 3 9 5 6	fthf1	|- ( ph -> ( X G Y ) : ( X H Y ) -1-1-> ( ( F ` X ) J ( F ` Y ) ) )
11	8	simpld	|- ( ph -> F ( C Full D ) G )
12	1 3 2 11 5 6	fullfo	|- ( ph -> ( X G Y ) : ( X H Y ) -onto-> ( ( F ` X ) J ( F ` Y ) ) )
13		df-f1o	|- ( ( X G Y ) : ( X H Y ) -1-1-onto-> ( ( F ` X ) J ( F ` Y ) ) <-> ( ( X G Y ) : ( X H Y ) -1-1-> ( ( F ` X ) J ( F ` Y ) ) /\ ( X G Y ) : ( X H Y ) -onto-> ( ( F ` X ) J ( F ` Y ) ) ) )
14	10 12 13	sylanbrc	|- ( ph -> ( X G Y ) : ( X H Y ) -1-1-onto-> ( ( F ` X ) J ( F ` Y ) ) )