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	No typesetting found for |- ( ph -> X ( <. F , G >. ( O UP P ) W ) M ) with typecode |-
	uptpos.h	$$⊢\phi \to tposG=H$$
Assertion	uptpos	Could not format assertion : No typesetting found for |- ( ph -> X ( <. F , tpos H >. ( O UP P ) W ) M ) with typecode |-

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		uptpos.h	$$⊢\phi \to tposG=H$$
3	1 2	uptposlem	$$⊢\phi \to tposH=G$$
4	3	opeq2d	$$⊢\phi \to ⟨F,tposH⟩=⟨F,G⟩$$
5	4	oveq1d	Could not format ( ph -> ( <. F , tpos H >. ( O UP P ) W ) = ( <. F , G >. ( O UP P ) W ) ) : No typesetting found for |- ( ph -> ( <. F , tpos H >. ( O UP P ) W ) = ( <. F , G >. ( O UP P ) W ) ) with typecode |-
6	5	breqd	Could not format ( ph -> ( X ( <. F , tpos H >. ( O UP P ) W ) M <-> X ( <. F , G >. ( O UP P ) W ) M ) ) : No typesetting found for |- ( ph -> ( X ( <. F , tpos H >. ( O UP P ) W ) M <-> X ( <. F , G >. ( O UP P ) W ) M ) ) with typecode |-
7	1 6	mpbird	Could not format ( ph -> X ( <. F , tpos H >. ( O UP P ) W ) M ) : No typesetting found for |- ( ph -> X ( <. F , tpos H >. ( O UP P ) W ) M ) with typecode |-