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 ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
funcoppc2.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
funcoppc2.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
funcoppc2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
funcoppc3.f ⊢ ( 𝜑 → 𝐹 ( 𝑂 Func 𝑃 ) tpos 𝐺 )
funcoppc3.g ⊢ ( 𝜑 → 𝐺 Fn ( 𝐴 × 𝐵 ) )
Assertion funcoppc3 ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )

Proof

Step Hyp Ref Expression
1 funcoppc2.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 funcoppc2.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3 funcoppc2.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4 funcoppc2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
5 funcoppc3.f ⊢ ( 𝜑 → 𝐹 ( 𝑂 Func 𝑃 ) tpos 𝐺 )
6 funcoppc3.g ⊢ ( 𝜑 → 𝐺 Fn ( 𝐴 × 𝐵 ) )
7 1 2 3 4 5 funcoppc2 ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) tpos tpos 𝐺 )
8 fnrel ⊢ ( 𝐺 Fn ( 𝐴 × 𝐵 ) → Rel 𝐺 )
9 6 8 syl ⊢ ( 𝜑 → Rel 𝐺 )
10 relxp ⊢ Rel ( 𝐴 × 𝐵 )
11 6 fndmd ⊢ ( 𝜑 → dom 𝐺 = ( 𝐴 × 𝐵 ) )
12 11 releqd ⊢ ( 𝜑 → ( Rel dom 𝐺 ↔ Rel ( 𝐴 × 𝐵 ) ) )
13 10 12 mpbiri ⊢ ( 𝜑 → Rel dom 𝐺 )
14 tpostpos2 ⊢ ( ( Rel 𝐺 ∧ Rel dom 𝐺 ) → tpos tpos 𝐺 = 𝐺 )
15 9 13 14 syl2anc ⊢ ( 𝜑 → tpos tpos 𝐺 = 𝐺 )
16 7 15 breqtrd ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )