Theorem oppfuprcl2

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	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
	oppfuprcl2.f	⊢ ( 𝜑 → 𝐹 = ⟨ 𝐴 , 𝐵 ⟩ )
Assertion	oppfuprcl2	⊢ ( 𝜑 → 𝐴 ( 𝐷 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		oppfuprcl2.f	⊢ ( 𝜑 → 𝐹 = ⟨ 𝐴 , 𝐵 ⟩ )
8	1 2 3 4 5 6	oppfuprcl	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
9	7 8	eqeltrrd	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
10		df-br	⊢ ( 𝐴 ( 𝐷 Func 𝐸 ) 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
11	9 10	sylibr	⊢ ( 𝜑 → 𝐴 ( 𝐷 Func 𝐸 ) 𝐵 )