Description: The opposite functor of an opposite functor is a functor on the original categories. (Contributed by Zhi Wang, 14-Nov-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | funcoppc2.o | ⊢ 𝑂 = ( oppCat ‘ 𝐶 ) | |
| funcoppc2.p | ⊢ 𝑃 = ( oppCat ‘ 𝐷 ) | ||
| funcoppc2.c | ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 ) | ||
| funcoppc2.d | ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 ) | ||
| 2oppffunc.f | ⊢ 𝐺 = ( oppFunc ‘ 𝐹 ) | ||
| 2oppffunc.g | ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑂 Func 𝑃 ) ) | ||
| Assertion | 2oppffunc | ⊢ ( 𝜑 → ( oppFunc ‘ 𝐺 ) ∈ ( 𝐶 Func 𝐷 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | funcoppc2.o | ⊢ 𝑂 = ( oppCat ‘ 𝐶 ) | |
| 2 | funcoppc2.p | ⊢ 𝑃 = ( oppCat ‘ 𝐷 ) | |
| 3 | funcoppc2.c | ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 ) | |
| 4 | funcoppc2.d | ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 ) | |
| 5 | 2oppffunc.f | ⊢ 𝐺 = ( oppFunc ‘ 𝐹 ) | |
| 6 | 2oppffunc.g | ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑂 Func 𝑃 ) ) | |
| 7 | relfunc | ⊢ Rel ( 𝑂 Func 𝑃 ) | |
| 8 | 6 7 5 | 2oppf | ⊢ ( 𝜑 → ( oppFunc ‘ 𝐺 ) = 𝐹 ) |
| 9 | 5 6 | eqeltrrid | ⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) ∈ ( 𝑂 Func 𝑃 ) ) |
| 10 | 1 2 3 4 9 | funcoppc5 | ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) |
| 11 | 8 10 | eqeltrd | ⊢ ( 𝜑 → ( oppFunc ‘ 𝐺 ) ∈ ( 𝐶 Func 𝐷 ) ) |