Theorem oppcuprcl2

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)$$
	oppcuprcl2.o	$$⊢O=\mathrm{oppCat}\left(D\right)$$
	oppcuprcl2.d	$$⊢\phi \to D\in U$$
	oppcuprcl2.e	$$⊢\phi \to E\in V$$
	oppcuprcl2.h	$$⊢\phi \to tposG=H$$
Assertion	oppcuprcl2	$$⊢\phi \to F\left(D\mathrm{Func}E\right)H$$

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		oppcuprcl2.o	$$⊢O=\mathrm{oppCat}\left(D\right)$$
4		oppcuprcl2.d	$$⊢\phi \to D\in U$$
5		oppcuprcl2.e	$$⊢\phi \to E\in V$$
6		oppcuprcl2.h	$$⊢\phi \to tposG=H$$
7	1	uprcl2	$$⊢\phi \to F\left(O\mathrm{Func}P\right)G$$
8	3 2 4 5 7	funcoppc2	$$⊢\phi \to F\left(D\mathrm{Func}E\right)tposG$$
9	8 6	breqtrd	$$⊢\phi \to F\left(D\mathrm{Func}E\right)H$$