Metamath Proof Explorer


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 φ F C Full D C Faith D G
ffthf1o.x φ X B
ffthf1o.y φ Y B
Assertion ffthf1o φ 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 φ F C Full D C Faith D G
5 ffthf1o.x φ X B
6 ffthf1o.y φ Y B
7 brin F C Full D C Faith D G F C Full D G F C Faith D G
8 4 7 sylib φ F C Full D G F C Faith D G
9 8 simprd φ F C Faith D G
10 1 2 3 9 5 6 fthf1 φ X G Y : X H Y 1-1 F X J F Y
11 8 simpld φ F C Full D G
12 1 3 2 11 5 6 fullfo φ 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 φ X G Y : X H Y 1-1 onto F X J F Y