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	|- ( 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 )
	oppfuprcl2.f	|- ( ph -> F = <. A , B >. )
Assertion	oppfuprcl2	|- ( ph -> A ( D Func E ) B )

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		oppfuprcl2.f	|- ( ph -> F = <. A , B >. )
8	1 2 3 4 5 6	oppfuprcl	|- ( ph -> F e. ( D Func E ) )
9	7 8	eqeltrrd	|- ( ph -> <. A , B >. e. ( D Func E ) )
10		df-br	|- ( A ( D Func E ) B <-> <. A , B >. e. ( D Func E ) )
11	9 10	sylibr	|- ( ph -> A ( D Func E ) B )