Metamath Proof Explorer

Theorem funcoppc2

Description: A functor on opposite categories yields a functor on the original categories. (Contributed by Zhi Wang, 4-Nov-2025)

Ref Expression
Hypotheses funcoppc2.o ⊢ O = oppCat ⁡ C
funcoppc2.p ⊢ P = oppCat ⁡ D
funcoppc2.c ⊢ φ → C ∈ V
funcoppc2.d ⊢ φ → D ∈ W
funcoppc2.f ⊢ φ → F O Func P G
Assertion funcoppc2 ⊢ φ → F C Func D tpos G

Proof

Step Hyp Ref Expression
1 funcoppc2.o ⊢ O = oppCat ⁡ C
2 funcoppc2.p ⊢ P = oppCat ⁡ D
3 funcoppc2.c ⊢ φ → C ∈ V
4 funcoppc2.d ⊢ φ → D ∈ W
5 funcoppc2.f ⊢ φ → F O Func P G
6 eqid ⊢ oppCat ⁡ O = oppCat ⁡ O
7 eqid ⊢ oppCat ⁡ P = oppCat ⁡ P
8 6 7 5 funcoppc ⊢ φ → F oppCat ⁡ O Func oppCat ⁡ P tpos G
9 1 2oppchomf ⊢ Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ oppCat ⁡ O
10 9 a1i ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ oppCat ⁡ O
11 1 2oppccomf ⊢ comp 𝑓 ⁡ C = comp 𝑓 ⁡ oppCat ⁡ O
12 11 a1i ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ oppCat ⁡ O
13 2 2oppchomf ⊢ Hom 𝑓 ⁡ D = Hom 𝑓 ⁡ oppCat ⁡ P
14 13 a1i ⊢ φ → Hom 𝑓 ⁡ D = Hom 𝑓 ⁡ oppCat ⁡ P
15 2 2oppccomf ⊢ comp 𝑓 ⁡ D = comp 𝑓 ⁡ oppCat ⁡ P
16 15 a1i ⊢ φ → comp 𝑓 ⁡ D = comp 𝑓 ⁡ oppCat ⁡ P
17 3 elexd ⊢ φ → C ∈ V
18 fvexd ⊢ φ → oppCat ⁡ O ∈ V
19 4 elexd ⊢ φ → D ∈ V
20 fvexd ⊢ φ → oppCat ⁡ P ∈ V
21 10 12 14 16 17 18 19 20 funcpropd ⊢ φ → C Func D = oppCat ⁡ O Func oppCat ⁡ P
22 21 breqd ⊢ φ → F C Func D tpos G ↔ F oppCat ⁡ O Func oppCat ⁡ P tpos G
23 8 22 mpbird ⊢ φ → F C Func D tpos G