Theorem uptposlem

Description: Lemma for uptpos . (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	uptposlem	$$⊢\phi \to tposH=G$$

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	2	tposeqd	$$⊢\phi \to tpostposG=tposH$$
4		eqid	$$⊢{\mathrm{Base}}_O={\mathrm{Base}}_O$$
5	1	uprcl2	$$⊢\phi \to F\left(O\mathrm{Func}P\right)G$$
6	4 5	funcfn2	$$⊢\phi \to GFn\left({\mathrm{Base}}_O\times {\mathrm{Base}}_O\right)$$
7		fnrel	$$⊢GFn\left({\mathrm{Base}}_O\times {\mathrm{Base}}_O\right)\to \mathrm{Rel}G$$
8	6 7	syl	$$⊢\phi \to \mathrm{Rel}G$$
9		relxp	$$⊢\mathrm{Rel}\left({\mathrm{Base}}_O\times {\mathrm{Base}}_O\right)$$
10	6	fndmd	$$⊢\phi \to \mathrm{dom}G={\mathrm{Base}}_O\times {\mathrm{Base}}_O$$
11	10	releqd	$$⊢\phi \to \left(\mathrm{Rel}\mathrm{dom}G\leftrightarrow \mathrm{Rel}\left({\mathrm{Base}}_O\times {\mathrm{Base}}_O\right)\right)$$
12	9 11	mpbiri	$$⊢\phi \to \mathrm{Rel}\mathrm{dom}G$$
13		tpostpos2	$$⊢\left(\mathrm{Rel}G\wedge \mathrm{Rel}\mathrm{dom}G\right)\to tpostposG=G$$
14	8 12 13	syl2anc	$$⊢\phi \to tpostposG=G$$
15	3 14	eqtr3d	$$⊢\phi \to tposH=G$$