Metamath Proof Explorer


Theorem idffth

Description: The identity functor is a fully faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypothesis idffth.i I = id func C
Assertion idffth C Cat I C Full C C Faith C

Proof

Step Hyp Ref Expression
1 idffth.i I = id func C
2 relfunc Rel C Func C
3 1 idfucl C Cat I C Func C
4 1st2nd Rel C Func C I C Func C I = 1 st I 2 nd I
5 2 3 4 sylancr C Cat I = 1 st I 2 nd I
6 5 3 eqeltrrd C Cat 1 st I 2 nd I C Func C
7 df-br 1 st I C Func C 2 nd I 1 st I 2 nd I C Func C
8 6 7 sylibr C Cat 1 st I C Func C 2 nd I
9 f1oi I x Hom C y : x Hom C y 1-1 onto x Hom C y
10 eqid Base C = Base C
11 simpl C Cat x Base C y Base C C Cat
12 eqid Hom C = Hom C
13 simprl C Cat x Base C y Base C x Base C
14 simprr C Cat x Base C y Base C y Base C
15 1 10 11 12 13 14 idfu2nd C Cat x Base C y Base C x 2 nd I y = I x Hom C y
16 eqidd C Cat x Base C y Base C x Hom C y = x Hom C y
17 1 10 11 13 idfu1 C Cat x Base C y Base C 1 st I x = x
18 1 10 11 14 idfu1 C Cat x Base C y Base C 1 st I y = y
19 17 18 oveq12d C Cat x Base C y Base C 1 st I x Hom C 1 st I y = x Hom C y
20 15 16 19 f1oeq123d C Cat x Base C y Base C x 2 nd I y : x Hom C y 1-1 onto 1 st I x Hom C 1 st I y I x Hom C y : x Hom C y 1-1 onto x Hom C y
21 9 20 mpbiri C Cat x Base C y Base C x 2 nd I y : x Hom C y 1-1 onto 1 st I x Hom C 1 st I y
22 21 ralrimivva C Cat x Base C y Base C x 2 nd I y : x Hom C y 1-1 onto 1 st I x Hom C 1 st I y
23 10 12 12 isffth2 1 st I C Full C C Faith C 2 nd I 1 st I C Func C 2 nd I x Base C y Base C x 2 nd I y : x Hom C y 1-1 onto 1 st I x Hom C 1 st I y
24 8 22 23 sylanbrc C Cat 1 st I C Full C C Faith C 2 nd I
25 df-br 1 st I C Full C C Faith C 2 nd I 1 st I 2 nd I C Full C C Faith C
26 24 25 sylib C Cat 1 st I 2 nd I C Full C C Faith C
27 5 26 eqeltrd C Cat I C Full C C Faith C