Metamath Proof Explorer

Theorem fulloppc

Description: The opposite functor of a full functor is also full. Proposition 3.43(d) in Adamek p. 39. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses fulloppc.o 
|- O = ( oppCat ` C )
fulloppc.p 
|- P = ( oppCat ` D )
fulloppc.f 
|- ( ph -> F ( C Full D ) G )
Assertion fulloppc 
|- ( ph -> F ( O Full P ) tpos G )

Proof

Step Hyp Ref Expression
1 fulloppc.o 
 |-  O = ( oppCat ` C )
2 fulloppc.p 
 |-  P = ( oppCat ` D )
3 fulloppc.f 
 |-  ( ph -> F ( C Full D ) G )
4 fullfunc 
 |-  ( C Full D ) C_ ( C Func D )
5 4 ssbri 
 |-  ( F ( C Full D ) G -> F ( C Func D ) G )
6 3 5 syl 
 |-  ( ph -> F ( C Func D ) G )
7 1 2 6 funcoppc 
 |-  ( ph -> F ( O Func P ) tpos G )
8 eqid 
 |-  ( Base ` C ) = ( Base ` C )
9 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
10 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
11 3 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> F ( C Full D ) G )
12 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> y e. ( Base ` C ) )
13 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x e. ( Base ` C ) )
14 8 9 10 11 12 13 fullfo 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( y G x ) : ( y ( Hom ` C ) x ) -onto-> ( ( F ` y ) ( Hom ` D ) ( F ` x ) ) )
15 forn 
 |-  ( ( y G x ) : ( y ( Hom ` C ) x ) -onto-> ( ( F ` y ) ( Hom ` D ) ( F ` x ) ) -> ran ( y G x ) = ( ( F ` y ) ( Hom ` D ) ( F ` x ) ) )
16 14 15 syl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ran ( y G x ) = ( ( F ` y ) ( Hom ` D ) ( F ` x ) ) )
17 ovtpos 
 |-  ( x tpos G y ) = ( y G x )
18 17 rneqi 
 |-  ran ( x tpos G y ) = ran ( y G x )
19 9 2 oppchom 
 |-  ( ( F ` x ) ( Hom ` P ) ( F ` y ) ) = ( ( F ` y ) ( Hom ` D ) ( F ` x ) )
20 16 18 19 3eqtr4g 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ran ( x tpos G y ) = ( ( F ` x ) ( Hom ` P ) ( F ` y ) ) )
21 20 ralrimivva 
 |-  ( ph -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) ran ( x tpos G y ) = ( ( F ` x ) ( Hom ` P ) ( F ` y ) ) )
22 1 8 oppcbas 
 |-  ( Base ` C ) = ( Base ` O )
23 eqid 
 |-  ( Hom ` P ) = ( Hom ` P )
24 22 23 isfull 
 |-  ( F ( O Full P ) tpos G <-> ( F ( O Func P ) tpos G /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) ran ( x tpos G y ) = ( ( F ` x ) ( Hom ` P ) ( F ` y ) ) ) )
25 7 21 24 sylanbrc 
 |-  ( ph -> F ( O Full P ) tpos G )