Metamath Proof Explorer


Theorem cofth

Description: The composition of two faithful functors is faithful. Proposition 3.30(c) in Adamek p. 35. (Contributed by Mario Carneiro, 28-Jan-2017)

Ref Expression
Hypotheses cofth.f φ F C Faith D
cofth.g φ G D Faith E
Assertion cofth φ G func F C Faith E

Proof

Step Hyp Ref Expression
1 cofth.f φ F C Faith D
2 cofth.g φ G D Faith E
3 relfunc Rel C Func E
4 fthfunc C Faith D C Func D
5 4 1 sseldi φ F C Func D
6 fthfunc D Faith E D Func E
7 6 2 sseldi φ G D Func E
8 5 7 cofucl φ G func F C Func E
9 1st2nd Rel C Func E G func F C Func E G func F = 1 st G func F 2 nd G func F
10 3 8 9 sylancr φ G func F = 1 st G func F 2 nd G func F
11 1st2ndbr Rel C Func E G func F C Func E 1 st G func F C Func E 2 nd G func F
12 3 8 11 sylancr φ 1 st G func F C Func E 2 nd G func F
13 eqid Base D = Base D
14 eqid Hom D = Hom D
15 eqid Hom E = Hom E
16 relfth Rel D Faith E
17 2 adantr φ x Base C y Base C G D Faith E
18 1st2ndbr Rel D Faith E G D Faith E 1 st G D Faith E 2 nd G
19 16 17 18 sylancr φ x Base C y Base C 1 st G D Faith E 2 nd G
20 eqid Base C = Base C
21 relfunc Rel C Func D
22 5 adantr φ x Base C y Base C F C Func D
23 1st2ndbr Rel C Func D F C Func D 1 st F C Func D 2 nd F
24 21 22 23 sylancr φ x Base C y Base C 1 st F C Func D 2 nd F
25 20 13 24 funcf1 φ x Base C y Base C 1 st F : Base C Base D
26 simprl φ x Base C y Base C x Base C
27 25 26 ffvelrnd φ x Base C y Base C 1 st F x Base D
28 simprr φ x Base C y Base C y Base C
29 25 28 ffvelrnd φ x Base C y Base C 1 st F y Base D
30 13 14 15 19 27 29 fthf1 φ x Base C y Base C 1 st F x 2 nd G 1 st F y : 1 st F x Hom D 1 st F y 1-1 1 st G 1 st F x Hom E 1 st G 1 st F y
31 eqid Hom C = Hom C
32 relfth Rel C Faith D
33 1 adantr φ x Base C y Base C F C Faith D
34 1st2ndbr Rel C Faith D F C Faith D 1 st F C Faith D 2 nd F
35 32 33 34 sylancr φ x Base C y Base C 1 st F C Faith D 2 nd F
36 20 31 14 35 26 28 fthf1 φ x Base C y Base C x 2 nd F y : x Hom C y 1-1 1 st F x Hom D 1 st F y
37 f1co 1 st F x 2 nd G 1 st F y : 1 st F x Hom D 1 st F y 1-1 1 st G 1 st F x Hom E 1 st G 1 st F y x 2 nd F y : x Hom C y 1-1 1 st F x Hom D 1 st F y 1 st F x 2 nd G 1 st F y x 2 nd F y : x Hom C y 1-1 1 st G 1 st F x Hom E 1 st G 1 st F y
38 30 36 37 syl2anc φ x Base C y Base C 1 st F x 2 nd G 1 st F y x 2 nd F y : x Hom C y 1-1 1 st G 1 st F x Hom E 1 st G 1 st F y
39 7 adantr φ x Base C y Base C G D Func E
40 20 22 39 26 28 cofu2nd φ x Base C y Base C x 2 nd G func F y = 1 st F x 2 nd G 1 st F y x 2 nd F y
41 eqidd φ x Base C y Base C x Hom C y = x Hom C y
42 20 22 39 26 cofu1 φ x Base C y Base C 1 st G func F x = 1 st G 1 st F x
43 20 22 39 28 cofu1 φ x Base C y Base C 1 st G func F y = 1 st G 1 st F y
44 42 43 oveq12d φ x Base C y Base C 1 st G func F x Hom E 1 st G func F y = 1 st G 1 st F x Hom E 1 st G 1 st F y
45 40 41 44 f1eq123d φ x Base C y Base C x 2 nd G func F y : x Hom C y 1-1 1 st G func F x Hom E 1 st G func F y 1 st F x 2 nd G 1 st F y x 2 nd F y : x Hom C y 1-1 1 st G 1 st F x Hom E 1 st G 1 st F y
46 38 45 mpbird φ x Base C y Base C x 2 nd G func F y : x Hom C y 1-1 1 st G func F x Hom E 1 st G func F y
47 46 ralrimivva φ x Base C y Base C x 2 nd G func F y : x Hom C y 1-1 1 st G func F x Hom E 1 st G func F y
48 20 31 15 isfth2 1 st G func F C Faith E 2 nd G func F 1 st G func F C Func E 2 nd G func F x Base C y Base C x 2 nd G func F y : x Hom C y 1-1 1 st G func F x Hom E 1 st G func F y
49 12 47 48 sylanbrc φ 1 st G func F C Faith E 2 nd G func F
50 df-br 1 st G func F C Faith E 2 nd G func F 1 st G func F 2 nd G func F C Faith E
51 49 50 sylib φ 1 st G func F 2 nd G func F C Faith E
52 10 51 eqeltrd φ G func F C Faith E