Theorem oppfuprcl

Description: Reverse closure for the class of universal property for opposite functors. (Contributed by Zhi Wang, 14-Nov-2025)

	Ref	Expression
Hypotheses	uprcl2a.x	⊢ ( 𝜑 → 𝑋 ( 𝐺 ( 𝑂 UP 𝑃 ) 𝑊 ) 𝑀 )
	oppfuprcl.g	⊢ 𝐺 = ( oppFunc ‘ 𝐹 )
	oppfuprcl.o	⊢ 𝑂 = ( oppCat ‘ 𝐷 )
	oppfuprcl.p	⊢ 𝑃 = ( oppCat ‘ 𝐸 )
	oppfuprcl.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
	oppfuprcl.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
Assertion	oppfuprcl	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		uprcl2a.x	⊢ ( 𝜑 → 𝑋 ( 𝐺 ( 𝑂 UP 𝑃 ) 𝑊 ) 𝑀 )
2		oppfuprcl.g	⊢ 𝐺 = ( oppFunc ‘ 𝐹 )
3		oppfuprcl.o	⊢ 𝑂 = ( oppCat ‘ 𝐷 )
4		oppfuprcl.p	⊢ 𝑃 = ( oppCat ‘ 𝐸 )
5		oppfuprcl.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
6		oppfuprcl.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
7	1	uprcl2a	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑂 Func 𝑃 ) )
8	2 7	eqeltrrid	⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) ∈ ( 𝑂 Func 𝑃 ) )
9	3 4 5 6 8	funcoppc5	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )