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	No typesetting found for |- ( ph -> X ( G ( O UP P ) W ) M ) with typecode |-
	oppfuprcl.g	No typesetting found for |- G = ( oppFunc ` F ) with typecode |-
	oppfuprcl.o	$$⊢O=\mathrm{oppCat}\left(D\right)$$
	oppfuprcl.p	$$⊢P=\mathrm{oppCat}\left(E\right)$$
	oppfuprcl.d	$$⊢\phi \to D\in U$$
	oppfuprcl.e	$$⊢\phi \to E\in V$$
	oppfuprcl2.f	$$⊢\phi \to F=⟨A,B⟩$$
Assertion	oppfuprcl2	$$⊢\phi \to A\left(D\mathrm{Func}E\right)B$$

Proof

Step	Hyp	Ref	Expression
1		uprcl2a.x	Could not format ( ph -> X ( G ( O UP P ) W ) M ) : No typesetting found for |- ( ph -> X ( G ( O UP P ) W ) M ) with typecode |-
2		oppfuprcl.g	Could not format G = ( oppFunc ` F ) : No typesetting found for |- G = ( oppFunc ` F ) with typecode |-
3		oppfuprcl.o	$$⊢O=\mathrm{oppCat}\left(D\right)$$
4		oppfuprcl.p	$$⊢P=\mathrm{oppCat}\left(E\right)$$
5		oppfuprcl.d	$$⊢\phi \to D\in U$$
6		oppfuprcl.e	$$⊢\phi \to E\in V$$
7		oppfuprcl2.f	$$⊢\phi \to F=⟨A,B⟩$$
8	1 2 3 4 5 6	oppfuprcl	$$⊢\phi \to F\in \left(D\mathrm{Func}E\right)$$
9	7 8	eqeltrrd	$$⊢\phi \to ⟨A,B⟩\in \left(D\mathrm{Func}E\right)$$
10		df-br	$$⊢A\left(D\mathrm{Func}E\right)B\leftrightarrow ⟨A,B⟩\in \left(D\mathrm{Func}E\right)$$
11	9 10	sylibr	$$⊢\phi \to A\left(D\mathrm{Func}E\right)B$$