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

Metamath Proof Explorer

Theorem funcoppc3

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
funcoppc3.f ⊢ φ → F O Func P tpos G
funcoppc3.g ⊢ φ → G Fn A × B
Assertion funcoppc3 ⊢ φ → F C Func D 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 funcoppc3.f ⊢ φ → F O Func P tpos G
6 funcoppc3.g ⊢ φ → G Fn A × B
7 1 2 3 4 5 funcoppc2 ⊢ φ → F C Func D tpos tpos G
8 fnrel ⊢ G Fn A × B → Rel ⁡ G
9 6 8 syl ⊢ φ → Rel ⁡ G
10 relxp ⊢ Rel ⁡ A × B
11 6 fndmd ⊢ φ → dom ⁡ G = A × B
12 11 releqd ⊢ φ → Rel ⁡ dom ⁡ G ↔ Rel ⁡ A × B
13 10 12 mpbiri ⊢ φ → Rel ⁡ dom ⁡ G
14 tpostpos2 ⊢ Rel ⁡ G ∧ Rel ⁡ dom ⁡ G → tpos tpos G = G
15 9 13 14 syl2anc ⊢ φ → tpos tpos G = G
16 7 15 breqtrd ⊢ φ → F C Func D G