Theorem uptpos

Description: Rewrite the predicate of universal property in the form of opposite functor. (Contributed by Zhi Wang, 4-Nov-2025)

	Ref	Expression
Hypotheses	oppcuprcl2.x	|- ( ph -> X ( <. F , G >. ( O UP P ) W ) M )
	uptpos.h	|- ( ph -> tpos G = H )
Assertion	uptpos	|- ( ph -> X ( <. F , tpos H >. ( O UP P ) W ) M )

Proof

Step	Hyp	Ref	Expression
1		oppcuprcl2.x	|- ( ph -> X ( <. F , G >. ( O UP P ) W ) M )
2		uptpos.h	|- ( ph -> tpos G = H )
3	1 2	uptposlem	|- ( ph -> tpos H = G )
4	3	opeq2d	|- ( ph -> <. F , tpos H >. = <. F , G >. )
5	4	oveq1d	|- ( ph -> ( <. F , tpos H >. ( O UP P ) W ) = ( <. F , G >. ( O UP P ) W ) )
6	5	breqd	|- ( ph -> ( X ( <. F , tpos H >. ( O UP P ) W ) M <-> X ( <. F , G >. ( O UP P ) W ) M ) )
7	1 6	mpbird	|- ( ph -> X ( <. F , tpos H >. ( O UP P ) W ) M )