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

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	$⊢ φ \to tpos G = H$
3	1 2	uptposlem	$⊢ φ \to tpos H = G$
4	3	opeq2d	$⊢ φ \to ⟨F, tpos H⟩ = ⟨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 \|-

Metamath Proof Explorer