Theorem oppcuprcl3

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 )
	oppcuprcl3.c	|- C = ( Base ` E )
Assertion	oppcuprcl3	|- ( ph -> W e. C )

Proof

Step	Hyp	Ref	Expression
1		oppcuprcl2.x	|- ( ph -> X ( <. F , G >. ( O UP P ) W ) M )
2		oppcuprcl2.p	|- P = ( oppCat ` E )
3		oppcuprcl3.c	|- C = ( Base ` E )
4	2 3	oppcbas	|- C = ( Base ` P )
5	1 4	uprcl3	|- ( ph -> W e. C )