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	|- ( ph -> X ( <. F , G >. ( O UP P ) W ) M )
	oppcuprcl2.p	|- P = ( oppCat ` E )
	oppcuprcl5.j	|- J = ( Hom ` E )
Assertion	oppcuprcl5	|- ( ph -> M e. ( ( F ` X ) J W ) )

Proof

Step	Hyp	Ref	Expression
1		oppcuprcl2.x	|- ( ph -> X ( <. F , G >. ( O UP P ) W ) M )
2		oppcuprcl2.p	|- P = ( oppCat ` E )
3		oppcuprcl5.j	|- J = ( Hom ` E )
4		eqid	|- ( Hom ` P ) = ( Hom ` P )
5	1 4	uprcl5	|- ( ph -> M e. ( W ( Hom ` P ) ( F ` X ) ) )
6	3 2	oppchom	|- ( W ( Hom ` P ) ( F ` X ) ) = ( ( F ` X ) J W )
7	5 6	eleqtrdi	|- ( ph -> M e. ( ( F ` X ) J W ) )