Theorem funcoppc4

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

	Ref	Expression
Hypotheses	funcoppc2.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	funcoppc2.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
	funcoppc2.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	funcoppc2.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
	funcoppc4.f	⊢ ( 𝜑 → ( 𝐹 oppFunc 𝐺 ) ∈ ( 𝑂 Func 𝑃 ) )
Assertion	funcoppc4	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		funcoppc2.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		funcoppc2.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3		funcoppc2.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4		funcoppc2.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
5		funcoppc4.f	⊢ ( 𝜑 → ( 𝐹 oppFunc 𝐺 ) ∈ ( 𝑂 Func 𝑃 ) )
6	5	func1st2nd	⊢ ( 𝜑 → ( 1st ‘ ( 𝐹 oppFunc 𝐺 ) ) ( 𝑂 Func 𝑃 ) ( 2nd ‘ ( 𝐹 oppFunc 𝐺 ) ) )
7	1 2 3 4 6	funcoppc2	⊢ ( 𝜑 → ( 1st ‘ ( 𝐹 oppFunc 𝐺 ) ) ( 𝐶 Func 𝐷 ) tpos ( 2nd ‘ ( 𝐹 oppFunc 𝐺 ) ) )
8		relfunc	⊢ Rel ( 𝑂 Func 𝑃 )
9		df-ov	⊢ ( 𝐹 oppFunc 𝐺 ) = ( oppFunc ‘ ⟨ 𝐹 , 𝐺 ⟩ )
10		eqidd	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ = ⟨ 𝐹 , 𝐺 ⟩ )
11	5 8 9 10	oppf1st2nd	⊢ ( 𝜑 → ( ( 𝐹 oppFunc 𝐺 ) ∈ ( V × V ) ∧ ( ( 1st ‘ ( 𝐹 oppFunc 𝐺 ) ) = 𝐹 ∧ ( 2nd ‘ ( 𝐹 oppFunc 𝐺 ) ) = tpos 𝐺 ) ) )
12	11	simprld	⊢ ( 𝜑 → ( 1st ‘ ( 𝐹 oppFunc 𝐺 ) ) = 𝐹 )
13	11	simprrd	⊢ ( 𝜑 → ( 2nd ‘ ( 𝐹 oppFunc 𝐺 ) ) = tpos 𝐺 )
14	13	tposeqd	⊢ ( 𝜑 → tpos ( 2nd ‘ ( 𝐹 oppFunc 𝐺 ) ) = tpos tpos 𝐺 )
15	5 8 9 10	oppfrcl3	⊢ ( 𝜑 → ( Rel 𝐺 ∧ Rel dom 𝐺 ) )
16		tpostpos2	⊢ ( ( Rel 𝐺 ∧ Rel dom 𝐺 ) → tpos tpos 𝐺 = 𝐺 )
17	15 16	syl	⊢ ( 𝜑 → tpos tpos 𝐺 = 𝐺 )
18	14 17	eqtrd	⊢ ( 𝜑 → tpos ( 2nd ‘ ( 𝐹 oppFunc 𝐺 ) ) = 𝐺 )
19	7 12 18	3brtr3d	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )