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	No typesetting found for |- ( ph -> X ( <. F , G >. ( O UP P ) W ) M ) with typecode |-
	oppcuprcl2.p	$$⊢P=\mathrm{oppCat}\left(E\right)$$
	oppcuprcl3.c	$$⊢C={\mathrm{Base}}_E$$
Assertion	oppcuprcl3	$$⊢\phi \to W\in C$$

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		oppcuprcl2.p	$$⊢P=\mathrm{oppCat}\left(E\right)$$
3		oppcuprcl3.c	$$⊢C={\mathrm{Base}}_E$$
4	2 3	oppcbas	$$⊢C={\mathrm{Base}}_P$$
5	1 4	uprcl3	$$⊢\phi \to W\in C$$