This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fulloppf

Description: The opposite functor of a full functor is also full. Proposition 3.43(d) in Adamek p. 39. (Contributed by Zhi Wang, 26-Nov-2025)

Ref Expression
Hypotheses fulloppf.o 
|- O = ( oppCat ` C )
fulloppf.p 
|- P = ( oppCat ` D )
fulloppf.f 
|- ( ph -> F e. ( C Full D ) )
Assertion fulloppf 
|- ( ph -> ( oppFunc ` F ) e. ( O Full P ) )

Proof

Step Hyp Ref Expression
1 fulloppf.o 
 |-  O = ( oppCat ` C )
2 fulloppf.p 
 |-  P = ( oppCat ` D )
3 fulloppf.f 
 |-  ( ph -> F e. ( C Full D ) )
4 fullfunc 
 |-  ( C Full D ) C_ ( C Func D )
5 4 sseli 
 |-  ( F e. ( C Full D ) -> F e. ( C Func D ) )
6 oppfval2 
 |-  ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. )
7 3 5 6 3syl 
 |-  ( ph -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. )
8 relfull 
 |-  Rel ( C Full D )
9 1st2ndbr 
 |-  ( ( Rel ( C Full D ) /\ F e. ( C Full D ) ) -> ( 1st ` F ) ( C Full D ) ( 2nd ` F ) )
10 8 3 9 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Full D ) ( 2nd ` F ) )
11 1 2 10 fulloppc 
 |-  ( ph -> ( 1st ` F ) ( O Full P ) tpos ( 2nd ` F ) )
12 df-br 
 |-  ( ( 1st ` F ) ( O Full P ) tpos ( 2nd ` F ) <-> <. ( 1st ` F ) , tpos ( 2nd ` F ) >. e. ( O Full P ) )
13 11 12 sylib 
 |-  ( ph -> <. ( 1st ` F ) , tpos ( 2nd ` F ) >. e. ( O Full P ) )
14 7 13 eqeltrd 
 |-  ( ph -> ( oppFunc ` F ) e. ( O Full P ) )