Theorem tposres2

Description: The transposition restricted to a set. (Contributed by Zhi Wang, 6-Oct-2025)

	Ref	Expression
Hypothesis	tposres2.1	$$⊢\phi \to \neg \varnothing \in \left(\mathrm{dom}F\cap R\right)$$
Assertion	tposres2	$$⊢\phi \to {tposF\upharpoonright }_R={tposF\upharpoonright }_{{R^{-1}}^{-1}}$$

Proof

Step	Hyp	Ref	Expression
1		tposres2.1	$$⊢\phi \to \neg \varnothing \in \left(\mathrm{dom}F\cap R\right)$$
2		tposresg	$$⊢{tposF\upharpoonright }_R=\left({tposF\upharpoonright }_{{R^{-1}}^{-1}}\right)\cup \left({F\upharpoonright }_{\left(R\cap \left\{\varnothing \right\}\right)}\right)$$
3		resinsn	$$⊢{F\upharpoonright }_{\left(R\cap \left\{\varnothing \right\}\right)}=\varnothing \leftrightarrow \neg \varnothing \in \left(\mathrm{dom}F\cap R\right)$$
4	1 3	sylibr	$$⊢\phi \to {F\upharpoonright }_{\left(R\cap \left\{\varnothing \right\}\right)}=\varnothing$$
5	4	uneq2d	$$⊢\phi \to \left({tposF\upharpoonright }_{{R^{-1}}^{-1}}\right)\cup \left({F\upharpoonright }_{\left(R\cap \left\{\varnothing \right\}\right)}\right)=\left({tposF\upharpoonright }_{{R^{-1}}^{-1}}\right)\cup \varnothing$$
6	2 5	eqtrid	$$⊢\phi \to {tposF\upharpoonright }_R=\left({tposF\upharpoonright }_{{R^{-1}}^{-1}}\right)\cup \varnothing$$
7		un0	$$⊢\left({tposF\upharpoonright }_{{R^{-1}}^{-1}}\right)\cup \varnothing ={tposF\upharpoonright }_{{R^{-1}}^{-1}}$$
8	6 7	eqtrdi	$$⊢\phi \to {tposF\upharpoonright }_R={tposF\upharpoonright }_{{R^{-1}}^{-1}}$$