Theorem oppcuprcl4

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 )
	oppcuprcl4.o	|- O = ( oppCat ` D )
	oppcuprcl4.b	|- B = ( Base ` D )
Assertion	oppcuprcl4	|- ( ph -> X e. B )

Proof

Step	Hyp	Ref	Expression
1		oppcuprcl2.x	|- ( ph -> X ( <. F , G >. ( O UP P ) W ) M )
2		oppcuprcl4.o	|- O = ( oppCat ` D )
3		oppcuprcl4.b	|- B = ( Base ` D )
4	2 3	oppcbas	|- B = ( Base ` O )
5	1 4	uprcl4	|- ( ph -> X e. B )