Theorem oppcuprcl2

Description: Reverse closure for the class of universal property in opposite categories. (Contributed by Zhi Wang, 4-Nov-2025)

	Ref	Expression
Hypotheses	oppcuprcl2.x	|- ( ph -> X ( <. F , G >. ( O UP P ) W ) M )
	oppcuprcl2.p	|- P = ( oppCat ` E )
	oppcuprcl2.o	|- O = ( oppCat ` D )
	oppcuprcl2.d	|- ( ph -> D e. U )
	oppcuprcl2.e	|- ( ph -> E e. V )
	oppcuprcl2.h	|- ( ph -> tpos G = H )
Assertion	oppcuprcl2	|- ( ph -> F ( D Func E ) H )

Proof

Step	Hyp	Ref	Expression
1		oppcuprcl2.x	|- ( ph -> X ( <. F , G >. ( O UP P ) W ) M )
2		oppcuprcl2.p	|- P = ( oppCat ` E )
3		oppcuprcl2.o	|- O = ( oppCat ` D )
4		oppcuprcl2.d	|- ( ph -> D e. U )
5		oppcuprcl2.e	|- ( ph -> E e. V )
6		oppcuprcl2.h	|- ( ph -> tpos G = H )
7	1	uprcl2	|- ( ph -> F ( O Func P ) G )
8	3 2 4 5 7	funcoppc2	|- ( ph -> F ( D Func E ) tpos G )
9	8 6	breqtrd	|- ( ph -> F ( D Func E ) H )