Theorem uptposlem

Description: Lemma for uptpos . (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	uptposlem	|- ( ph -> tpos H = G )

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	2	tposeqd	|- ( ph -> tpos tpos G = tpos H )
4		eqid	|- ( Base ` O ) = ( Base ` O )
5	1	uprcl2	|- ( ph -> F ( O Func P ) G )
6	4 5	funcfn2	|- ( ph -> G Fn ( ( Base ` O ) X. ( Base ` O ) ) )
7		fnrel	|- ( G Fn ( ( Base ` O ) X. ( Base ` O ) ) -> Rel G )
8	6 7	syl	|- ( ph -> Rel G )
9		relxp	|- Rel ( ( Base ` O ) X. ( Base ` O ) )
10	6	fndmd	|- ( ph -> dom G = ( ( Base ` O ) X. ( Base ` O ) ) )
11	10	releqd	|- ( ph -> ( Rel dom G <-> Rel ( ( Base ` O ) X. ( Base ` O ) ) ) )
12	9 11	mpbiri	|- ( ph -> Rel dom G )
13		tpostpos2	|- ( ( Rel G /\ Rel dom G ) -> tpos tpos G = G )
14	8 12 13	syl2anc	|- ( ph -> tpos tpos G = G )
15	3 14	eqtr3d	|- ( ph -> tpos H = G )