Metamath Proof Explorer

Theorem cofull

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

Ref Expression
Hypotheses cofull.f 
|- ( ph -> F e. ( C Full D ) )
cofull.g 
|- ( ph -> G e. ( D Full E ) )
Assertion cofull 
|- ( ph -> ( G o.func F ) e. ( C Full E ) )

Proof

Step Hyp Ref Expression
1 cofull.f 
 |-  ( ph -> F e. ( C Full D ) )
2 cofull.g 
 |-  ( ph -> G e. ( D Full E ) )
3 relfunc 
 |-  Rel ( C Func E )
4 fullfunc 
 |-  ( C Full D ) C_ ( C Func D )
5 4 1 sseldi 
 |-  ( ph -> F e. ( C Func D ) )
6 fullfunc 
 |-  ( D Full 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 ` E ) = ( Hom ` E )
15 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
16 relfull 
 |-  Rel ( D Full E )
17 2 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> G e. ( D Full E ) )
18 1st2ndbr 
 |-  ( ( Rel ( D Full E ) /\ G e. ( D Full E ) ) -> ( 1st ` G ) ( D Full E ) ( 2nd ` G ) )
19 16 17 18 sylancr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( 1st ` G ) ( D Full 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 fullfo 
 |-  ( ( 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 ) ) -onto-> ( ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) ( Hom ` E ) ( ( 1st ` G ) ` ( ( 1st ` F ) ` y ) ) ) )
31 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
32 relfull 
 |-  Rel ( C Full D )
33 1 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> F e. ( C Full D ) )
34 1st2ndbr 
 |-  ( ( Rel ( C Full D ) /\ F e. ( C Full D ) ) -> ( 1st ` F ) ( C Full D ) ( 2nd ` F ) )
35 32 33 34 sylancr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( 1st ` F ) ( C Full D ) ( 2nd ` F ) )
36 20 15 31 35 26 28 fullfo 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` F ) y ) : ( x ( Hom ` C ) y ) -onto-> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
37 foco 
 |-  ( ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) : ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) -onto-> ( ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) ( Hom ` E ) ( ( 1st ` G ) ` ( ( 1st ` F ) ` y ) ) ) /\ ( x ( 2nd ` F ) y ) : ( x ( Hom ` C ) y ) -onto-> ( ( ( 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 ) -onto-> ( ( ( 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 ) -onto-> ( ( ( 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 foeq123d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( x ( 2nd ` ( G o.func F ) ) y ) : ( x ( Hom ` C ) y ) -onto-> ( ( ( 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 ) -onto-> ( ( ( 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 ) -onto-> ( ( ( 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 ) -onto-> ( ( ( 1st ` ( G o.func F ) ) ` x ) ( Hom ` E ) ( ( 1st ` ( G o.func F ) ) ` y ) ) )
48 20 14 31 isfull2 
 |-  ( ( 1st ` ( G o.func F ) ) ( C Full 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 ) -onto-> ( ( ( 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 Full E ) ( 2nd ` ( G o.func F ) ) )
50 df-br 
 |-  ( ( 1st ` ( G o.func F ) ) ( C Full E ) ( 2nd ` ( G o.func F ) ) <-> <. ( 1st ` ( G o.func F ) ) , ( 2nd ` ( G o.func F ) ) >. e. ( C Full E ) )
51 49 50 sylib 
 |-  ( ph -> <. ( 1st ` ( G o.func F ) ) , ( 2nd ` ( G o.func F ) ) >. e. ( C Full E ) )
52 10 51 eqeltrd 
 |-  ( ph -> ( G o.func F ) e. ( C Full E ) )