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 ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
oppff1.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
oppff1o.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
oppff1o.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
Assertion oppff1o ( 𝜑 → ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) –1-1-onto→ ( 𝑂 Func 𝑃 ) )

Proof

Step Hyp Ref Expression
1 oppff1.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 oppff1.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3 oppff1o.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4 oppff1o.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
5 1 2 oppff1 ⊢ ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) –1-1→ ( 𝑂 Func 𝑃 )
6 5 a1i ⊢ ( 𝜑 → ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) –1-1→ ( 𝑂 Func 𝑃 ) )
7 f1f ⊢ ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) –1-1→ ( 𝑂 Func 𝑃 ) → ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) ⟶ ( 𝑂 Func 𝑃 ) )
8 6 7 syl ⊢ ( 𝜑 → ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) ⟶ ( 𝑂 Func 𝑃 ) )
9 fveq2 ⊢ ( 𝑔 = ( oppFunc ‘ 𝑓 ) → ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑔 ) = ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ ( oppFunc ‘ 𝑓 ) ) )
10 9 eqeq2d ⊢ ( 𝑔 = ( oppFunc ‘ 𝑓 ) → ( 𝑓 = ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑔 ) ↔ 𝑓 = ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ ( oppFunc ‘ 𝑓 ) ) ) )
11 3 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑂 Func 𝑃 ) ) → 𝐶 ∈ 𝑉 )
12 4 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑂 Func 𝑃 ) ) → 𝐷 ∈ 𝑊 )
13 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑂 Func 𝑃 ) ) → 𝑓 ∈ ( 𝑂 Func 𝑃 ) )
14 1 2 11 12 13 2oppffunc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑂 Func 𝑃 ) ) → ( oppFunc ‘ 𝑓 ) ∈ ( 𝐶 Func 𝐷 ) )
15 14 fvresd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑂 Func 𝑃 ) ) → ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ ( oppFunc ‘ 𝑓 ) ) = ( oppFunc ‘ ( oppFunc ‘ 𝑓 ) ) )
16 relfunc ⊢ Rel ( 𝐶 Func 𝐷 )
17 eqid ⊢ ( oppFunc ‘ 𝑓 ) = ( oppFunc ‘ 𝑓 )
18 14 16 17 2oppf ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑂 Func 𝑃 ) ) → ( oppFunc ‘ ( oppFunc ‘ 𝑓 ) ) = 𝑓 )
19 15 18 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑂 Func 𝑃 ) ) → 𝑓 = ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ ( oppFunc ‘ 𝑓 ) ) )
20 10 14 19 rspcedvdw ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑂 Func 𝑃 ) ) → ∃ 𝑔 ∈ ( 𝐶 Func 𝐷 ) 𝑓 = ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑔 ) )
21 20 ralrimiva ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( 𝑂 Func 𝑃 ) ∃ 𝑔 ∈ ( 𝐶 Func 𝐷 ) 𝑓 = ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑔 ) )
22 dffo3 ⊢ ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) –onto→ ( 𝑂 Func 𝑃 ) ↔ ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) ⟶ ( 𝑂 Func 𝑃 ) ∧ ∀ 𝑓 ∈ ( 𝑂 Func 𝑃 ) ∃ 𝑔 ∈ ( 𝐶 Func 𝐷 ) 𝑓 = ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑔 ) ) )
23 8 21 22 sylanbrc ⊢ ( 𝜑 → ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) –onto→ ( 𝑂 Func 𝑃 ) )
24 df-f1o ⊢ ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) –1-1-onto→ ( 𝑂 Func 𝑃 ) ↔ ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) –1-1→ ( 𝑂 Func 𝑃 ) ∧ ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) –onto→ ( 𝑂 Func 𝑃 ) ) )
25 6 23 24 sylanbrc ⊢ ( 𝜑 → ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) –1-1-onto→ ( 𝑂 Func 𝑃 ) )