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 𝐷 ) 𝐺 )