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 ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
oppff1.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
Assertion oppff1 ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) –1-1→ ( 𝑂 Func 𝑃 )

Proof

Step Hyp Ref Expression
1 oppff1.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 oppff1.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3 oppffn ⊢ oppFunc Fn ( V × V )
4 relfunc ⊢ Rel ( 𝐶 Func 𝐷 )
5 df-rel ⊢ ( Rel ( 𝐶 Func 𝐷 ) ↔ ( 𝐶 Func 𝐷 ) ⊆ ( V × V ) )
6 4 5 mpbi ⊢ ( 𝐶 Func 𝐷 ) ⊆ ( V × V )
7 fnssres ⊢ ( ( oppFunc Fn ( V × V ) ∧ ( 𝐶 Func 𝐷 ) ⊆ ( V × V ) ) → ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) Fn ( 𝐶 Func 𝐷 ) )
8 3 6 7 mp2an ⊢ ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) Fn ( 𝐶 Func 𝐷 )
9 fvres ⊢ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) → ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑓 ) = ( oppFunc ‘ 𝑓 ) )
10 id ⊢ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) → 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
11 1 2 10 oppfoppc2 ⊢ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) → ( oppFunc ‘ 𝑓 ) ∈ ( 𝑂 Func 𝑃 ) )
12 9 11 eqeltrd ⊢ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) → ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑓 ) ∈ ( 𝑂 Func 𝑃 ) )
13 12 rgen ⊢ ∀ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑓 ) ∈ ( 𝑂 Func 𝑃 )
14 ffnfv ⊢ ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) ⟶ ( 𝑂 Func 𝑃 ) ↔ ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) Fn ( 𝐶 Func 𝐷 ) ∧ ∀ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑓 ) ∈ ( 𝑂 Func 𝑃 ) ) )
15 8 13 14 mpbir2an ⊢ ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) ⟶ ( 𝑂 Func 𝑃 )
16 simpl ⊢ ( ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) → 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
17 16 fvresd ⊢ ( ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) → ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑓 ) = ( oppFunc ‘ 𝑓 ) )
18 simpr ⊢ ( ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) → 𝑔 ∈ ( 𝐶 Func 𝐷 ) )
19 18 fvresd ⊢ ( ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) → ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑔 ) = ( oppFunc ‘ 𝑔 ) )
20 17 19 eqeq12d ⊢ ( ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) → ( ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑓 ) = ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑔 ) ↔ ( oppFunc ‘ 𝑓 ) = ( oppFunc ‘ 𝑔 ) ) )
21 fveq2 ⊢ ( ( oppFunc ‘ 𝑓 ) = ( oppFunc ‘ 𝑔 ) → ( oppFunc ‘ ( oppFunc ‘ 𝑓 ) ) = ( oppFunc ‘ ( oppFunc ‘ 𝑔 ) ) )
22 1 2 16 oppfoppc2 ⊢ ( ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) → ( oppFunc ‘ 𝑓 ) ∈ ( 𝑂 Func 𝑃 ) )
23 relfunc ⊢ Rel ( 𝑂 Func 𝑃 )
24 eqid ⊢ ( oppFunc ‘ 𝑓 ) = ( oppFunc ‘ 𝑓 )
25 22 23 24 2oppf ⊢ ( ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) → ( oppFunc ‘ ( oppFunc ‘ 𝑓 ) ) = 𝑓 )
26 1 2 18 oppfoppc2 ⊢ ( ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) → ( oppFunc ‘ 𝑔 ) ∈ ( 𝑂 Func 𝑃 ) )
27 eqid ⊢ ( oppFunc ‘ 𝑔 ) = ( oppFunc ‘ 𝑔 )
28 26 23 27 2oppf ⊢ ( ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) → ( oppFunc ‘ ( oppFunc ‘ 𝑔 ) ) = 𝑔 )
29 25 28 eqeq12d ⊢ ( ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) → ( ( oppFunc ‘ ( oppFunc ‘ 𝑓 ) ) = ( oppFunc ‘ ( oppFunc ‘ 𝑔 ) ) ↔ 𝑓 = 𝑔 ) )
30 21 29 imbitrid ⊢ ( ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) → ( ( oppFunc ‘ 𝑓 ) = ( oppFunc ‘ 𝑔 ) → 𝑓 = 𝑔 ) )
31 20 30 sylbid ⊢ ( ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) → ( ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑓 ) = ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑔 ) → 𝑓 = 𝑔 ) )
32 31 rgen2 ⊢ ∀ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∀ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ( ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑓 ) = ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑔 ) → 𝑓 = 𝑔 )
33 dff13 ⊢ ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) –1-1→ ( 𝑂 Func 𝑃 ) ↔ ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) ⟶ ( 𝑂 Func 𝑃 ) ∧ ∀ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∀ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ( ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑓 ) = ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑔 ) → 𝑓 = 𝑔 ) ) )
34 15 32 33 mpbir2an ⊢ ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) –1-1→ ( 𝑂 Func 𝑃 )