Theorem oppcuprcl5

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)$$
	oppcuprcl5.j	$$⊢J=\mathrm{Hom}\left(E\right)$$
Assertion	oppcuprcl5	$$⊢\phi \to M\in \left(F\left(X\right)JW\right)$$

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		oppcuprcl5.j	$$⊢J=\mathrm{Hom}\left(E\right)$$
4		eqid	$$⊢\mathrm{Hom}\left(P\right)=\mathrm{Hom}\left(P\right)$$
5	1 4	uprcl5	$$⊢\phi \to M\in \left(W\mathrm{Hom}\left(P\right)F\left(X\right)\right)$$
6	3 2	oppchom	$$⊢W\mathrm{Hom}\left(P\right)F\left(X\right)=F\left(X\right)JW$$
7	5 6	eleqtrdi	$$⊢\phi \to M\in \left(F\left(X\right)JW\right)$$