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	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$$
Assertion	oppfuprcl	$$⊢\phi \to F\in \left(D\mathrm{Func}E\right)$$

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	1	uprcl2a	$$⊢\phi \to G\in \left(O\mathrm{Func}P\right)$$
8	2 7	eqeltrrid	Could not format ( ph -> ( oppFunc ` F ) e. ( O Func P ) ) : No typesetting found for |- ( ph -> ( oppFunc ` F ) e. ( O Func P ) ) with typecode |-
9	3 4 5 6 8	funcoppc5	$$⊢\phi \to F\in \left(D\mathrm{Func}E\right)$$