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	No typesetting found for |- ( ph -> X ( <. F , G >. ( O UP P ) W ) M ) with typecode |-
	oppcuprcl4.o	$$⊢O=\mathrm{oppCat}\left(D\right)$$
	oppcuprcl4.b	$$⊢B={\mathrm{Base}}_D$$
Assertion	oppcuprcl4	$$⊢\phi \to X\in B$$

Proof

Step	Hyp	Ref	Expression
1		oppcuprcl2.x	Could not format ( ph -> X ( <. F , G >. ( O UP P ) W ) M ) : No typesetting found for |- ( ph -> X ( <. F , G >. ( O UP P ) W ) M ) with typecode |-
2		oppcuprcl4.o	$$⊢O=\mathrm{oppCat}\left(D\right)$$
3		oppcuprcl4.b	$$⊢B={\mathrm{Base}}_D$$
4	2 3	oppcbas	$$⊢B={\mathrm{Base}}_O$$
5	1 4	uprcl4	$$⊢\phi \to X\in B$$