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 
|- ( ph -> F e. ( C Faith D ) )
cofth.g 
|- ( ph -> G e. ( D Faith E ) )
Assertion cofth 
|- ( ph -> ( G o.func F ) e. ( C Faith E ) )

Proof

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