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	|- ( ph -> X ( G ( O UP P ) W ) M )
	oppfuprcl.g	|- G = ( oppFunc ` F )
	oppfuprcl.o	|- O = ( oppCat ` D )
	oppfuprcl.p	|- P = ( oppCat ` E )
	oppfuprcl.d	|- ( ph -> D e. U )
	oppfuprcl.e	|- ( ph -> E e. V )
Assertion	oppfuprcl	|- ( ph -> F e. ( D Func E ) )

Proof

Step	Hyp	Ref	Expression
1		uprcl2a.x	|- ( ph -> X ( G ( O UP P ) W ) M )
2		oppfuprcl.g	|- G = ( oppFunc ` F )
3		oppfuprcl.o	|- O = ( oppCat ` D )
4		oppfuprcl.p	|- P = ( oppCat ` E )
5		oppfuprcl.d	|- ( ph -> D e. U )
6		oppfuprcl.e	|- ( ph -> E e. V )
7	1	uprcl2a	|- ( ph -> G e. ( O Func P ) )
8	2 7	eqeltrrid	|- ( ph -> ( oppFunc ` F ) e. ( O Func P ) )
9	3 4 5 6 8	funcoppc5	|- ( ph -> F e. ( D Func E ) )