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

Proof

Step	Hyp	Ref	Expression
1		funcoppc2.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		funcoppc2.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3		funcoppc2.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4		funcoppc2.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
5		funcoppc2.f	⊢ ( 𝜑 → 𝐹 ( 𝑂 Func 𝑃 ) 𝐺 )
6		eqid	⊢ ( oppCat ‘ 𝑂 ) = ( oppCat ‘ 𝑂 )
7		eqid	⊢ ( oppCat ‘ 𝑃 ) = ( oppCat ‘ 𝑃 )
8	6 7 5	funcoppc	⊢ ( 𝜑 → 𝐹 ( ( oppCat ‘ 𝑂 ) Func ( oppCat ‘ 𝑃 ) ) tpos 𝐺 )
9	1	2oppchomf	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) )
10	9	a1i	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) ) )
11	1	2oppccomf	⊢ ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) )
12	11	a1i	⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) ) )
13	2	2oppchomf	⊢ ( Homf ‘ 𝐷 ) = ( Homf ‘ ( oppCat ‘ 𝑃 ) )
14	13	a1i	⊢ ( 𝜑 → ( Homf ‘ 𝐷 ) = ( Homf ‘ ( oppCat ‘ 𝑃 ) ) )
15	2	2oppccomf	⊢ ( compf ‘ 𝐷 ) = ( compf ‘ ( oppCat ‘ 𝑃 ) )
16	15	a1i	⊢ ( 𝜑 → ( compf ‘ 𝐷 ) = ( compf ‘ ( oppCat ‘ 𝑃 ) ) )
17	3	elexd	⊢ ( 𝜑 → 𝐶 ∈ V )
18		fvexd	⊢ ( 𝜑 → ( oppCat ‘ 𝑂 ) ∈ V )
19	4	elexd	⊢ ( 𝜑 → 𝐷 ∈ V )
20		fvexd	⊢ ( 𝜑 → ( oppCat ‘ 𝑃 ) ∈ V )
21	10 12 14 16 17 18 19 20	funcpropd	⊢ ( 𝜑 → ( 𝐶 Func 𝐷 ) = ( ( oppCat ‘ 𝑂 ) Func ( oppCat ‘ 𝑃 ) ) )
22	21	breqd	⊢ ( 𝜑 → ( 𝐹 ( 𝐶 Func 𝐷 ) tpos 𝐺 ↔ 𝐹 ( ( oppCat ‘ 𝑂 ) Func ( oppCat ‘ 𝑃 ) ) tpos 𝐺 ) )
23	8 22	mpbird	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) tpos 𝐺 )