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

Metamath Proof Explorer

Theorem oppff1

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

Ref Expression
Hypotheses oppff1.o 
|- O = ( oppCat ` C )
oppff1.p 
|- P = ( oppCat ` D )
Assertion oppff1 
|- ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P )

Proof

Step Hyp Ref Expression
1 oppff1.o 
 |-  O = ( oppCat ` C )
2 oppff1.p 
 |-  P = ( oppCat ` D )
3 oppffn 
 |-  oppFunc Fn ( _V X. _V )
4 relfunc 
 |-  Rel ( C Func D )
5 df-rel 
 |-  ( Rel ( C Func D ) <-> ( C Func D ) C_ ( _V X. _V ) )
6 4 5 mpbi 
 |-  ( C Func D ) C_ ( _V X. _V )
7 fnssres 
 |-  ( ( oppFunc Fn ( _V X. _V ) /\ ( C Func D ) C_ ( _V X. _V ) ) -> ( oppFunc |` ( C Func D ) ) Fn ( C Func D ) )
8 3 6 7 mp2an 
 |-  ( oppFunc |` ( C Func D ) ) Fn ( C Func D )
9 fvres 
 |-  ( f e. ( C Func D ) -> ( ( oppFunc |` ( C Func D ) ) ` f ) = ( oppFunc ` f ) )
10 id 
 |-  ( f e. ( C Func D ) -> f e. ( C Func D ) )
11 1 2 10 oppfoppc2 
 |-  ( f e. ( C Func D ) -> ( oppFunc ` f ) e. ( O Func P ) )
12 9 11 eqeltrd 
 |-  ( f e. ( C Func D ) -> ( ( oppFunc |` ( C Func D ) ) ` f ) e. ( O Func P ) )
13 12 rgen 
 |-  A. f e. ( C Func D ) ( ( oppFunc |` ( C Func D ) ) ` f ) e. ( O Func P )
14 ffnfv 
 |-  ( ( oppFunc |` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) <-> ( ( oppFunc |` ( C Func D ) ) Fn ( C Func D ) /\ A. f e. ( C Func D ) ( ( oppFunc |` ( C Func D ) ) ` f ) e. ( O Func P ) ) )
15 8 13 14 mpbir2an 
 |-  ( oppFunc |` ( C Func D ) ) : ( C Func D ) --> ( O Func P )
16 simpl 
 |-  ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> f e. ( C Func D ) )
17 16 fvresd 
 |-  ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( ( oppFunc |` ( C Func D ) ) ` f ) = ( oppFunc ` f ) )
18 simpr 
 |-  ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> g e. ( C Func D ) )
19 18 fvresd 
 |-  ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( ( oppFunc |` ( C Func D ) ) ` g ) = ( oppFunc ` g ) )
20 17 19 eqeq12d 
 |-  ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( ( ( oppFunc |` ( C Func D ) ) ` f ) = ( ( oppFunc |` ( C Func D ) ) ` g ) <-> ( oppFunc ` f ) = ( oppFunc ` g ) ) )
21 fveq2 
 |-  ( ( oppFunc ` f ) = ( oppFunc ` g ) -> ( oppFunc ` ( oppFunc ` f ) ) = ( oppFunc ` ( oppFunc ` g ) ) )
22 1 2 16 oppfoppc2 
 |-  ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( oppFunc ` f ) e. ( O Func P ) )
23 relfunc 
 |-  Rel ( O Func P )
24 eqid 
 |-  ( oppFunc ` f ) = ( oppFunc ` f )
25 22 23 24 2oppf 
 |-  ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( oppFunc ` ( oppFunc ` f ) ) = f )
26 1 2 18 oppfoppc2 
 |-  ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( oppFunc ` g ) e. ( O Func P ) )
27 eqid 
 |-  ( oppFunc ` g ) = ( oppFunc ` g )
28 26 23 27 2oppf 
 |-  ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( oppFunc ` ( oppFunc ` g ) ) = g )
29 25 28 eqeq12d 
 |-  ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( ( oppFunc ` ( oppFunc ` f ) ) = ( oppFunc ` ( oppFunc ` g ) ) <-> f = g ) )
30 21 29 imbitrid 
 |-  ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( ( oppFunc ` f ) = ( oppFunc ` g ) -> f = g ) )
31 20 30 sylbid 
 |-  ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( ( ( oppFunc |` ( C Func D ) ) ` f ) = ( ( oppFunc |` ( C Func D ) ) ` g ) -> f = g ) )
32 31 rgen2 
 |-  A. f e. ( C Func D ) A. g e. ( C Func D ) ( ( ( oppFunc |` ( C Func D ) ) ` f ) = ( ( oppFunc |` ( C Func D ) ) ` g ) -> f = g )
33 dff13 
 |-  ( ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P ) <-> ( ( oppFunc |` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) /\ A. f e. ( C Func D ) A. g e. ( C Func D ) ( ( ( oppFunc |` ( C Func D ) ) ` f ) = ( ( oppFunc |` ( C Func D ) ) ` g ) -> f = g ) ) )
34 15 32 33 mpbir2an 
 |-  ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P )