Metamath Proof Explorer

Theorem oppff1o

Description: The operation generating opposite functors is bijective. (Contributed by Zhi Wang, 17-Nov-2025)

Ref Expression
Hypotheses oppff1.o 
|- O = ( oppCat ` C )
oppff1.p 
|- P = ( oppCat ` D )
oppff1o.c 
|- ( ph -> C e. V )
oppff1o.d 
|- ( ph -> D e. W )
Assertion oppff1o 
|- ( ph -> ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-onto-> ( O Func P ) )

Proof

Step Hyp Ref Expression
1 oppff1.o 
 |-  O = ( oppCat ` C )
2 oppff1.p 
 |-  P = ( oppCat ` D )
3 oppff1o.c 
 |-  ( ph -> C e. V )
4 oppff1o.d 
 |-  ( ph -> D e. W )
5 1 2 oppff1 
 |-  ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P )
6 5 a1i 
 |-  ( ph -> ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P ) )
7 f1f 
 |-  ( ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P ) -> ( oppFunc |` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) )
8 6 7 syl 
 |-  ( ph -> ( oppFunc |` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) )
9 fveq2 
 |-  ( g = ( oppFunc ` f ) -> ( ( oppFunc |` ( C Func D ) ) ` g ) = ( ( oppFunc |` ( C Func D ) ) ` ( oppFunc ` f ) ) )
10 9 eqeq2d 
 |-  ( g = ( oppFunc ` f ) -> ( f = ( ( oppFunc |` ( C Func D ) ) ` g ) <-> f = ( ( oppFunc |` ( C Func D ) ) ` ( oppFunc ` f ) ) ) )
11 3 adantr 
 |-  ( ( ph /\ f e. ( O Func P ) ) -> C e. V )
12 4 adantr 
 |-  ( ( ph /\ f e. ( O Func P ) ) -> D e. W )
13 simpr 
 |-  ( ( ph /\ f e. ( O Func P ) ) -> f e. ( O Func P ) )
14 1 2 11 12 13 2oppffunc 
 |-  ( ( ph /\ f e. ( O Func P ) ) -> ( oppFunc ` f ) e. ( C Func D ) )
15 14 fvresd 
 |-  ( ( ph /\ f e. ( O Func P ) ) -> ( ( oppFunc |` ( C Func D ) ) ` ( oppFunc ` f ) ) = ( oppFunc ` ( oppFunc ` f ) ) )
16 relfunc 
 |-  Rel ( C Func D )
17 eqid 
 |-  ( oppFunc ` f ) = ( oppFunc ` f )
18 14 16 17 2oppf 
 |-  ( ( ph /\ f e. ( O Func P ) ) -> ( oppFunc ` ( oppFunc ` f ) ) = f )
19 15 18 eqtr2d 
 |-  ( ( ph /\ f e. ( O Func P ) ) -> f = ( ( oppFunc |` ( C Func D ) ) ` ( oppFunc ` f ) ) )
20 10 14 19 rspcedvdw 
 |-  ( ( ph /\ f e. ( O Func P ) ) -> E. g e. ( C Func D ) f = ( ( oppFunc |` ( C Func D ) ) ` g ) )
21 20 ralrimiva 
 |-  ( ph -> A. f e. ( O Func P ) E. g e. ( C Func D ) f = ( ( oppFunc |` ( C Func D ) ) ` g ) )
22 dffo3 
 |-  ( ( oppFunc |` ( C Func D ) ) : ( C Func D ) -onto-> ( O Func P ) <-> ( ( oppFunc |` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) /\ A. f e. ( O Func P ) E. g e. ( C Func D ) f = ( ( oppFunc |` ( C Func D ) ) ` g ) ) )
23 8 21 22 sylanbrc 
 |-  ( ph -> ( oppFunc |` ( C Func D ) ) : ( C Func D ) -onto-> ( O Func P ) )
24 df-f1o 
 |-  ( ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-onto-> ( O Func P ) <-> ( ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P ) /\ ( oppFunc |` ( C Func D ) ) : ( C Func D ) -onto-> ( O Func P ) ) )
25 6 23 24 sylanbrc 
 |-  ( ph -> ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-onto-> ( O Func P ) )