Theorem tposres3

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	tposres3	$$⊢\phi \to {tposF\upharpoonright }_R=tpos\left({F\upharpoonright }_{R^{-1}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		tposres2.1	$$⊢\phi \to \neg \varnothing \in \left(\mathrm{dom}F\cap R\right)$$
2	1	tposres2	$$⊢\phi \to {tposF\upharpoonright }_R={tposF\upharpoonright }_{{R^{-1}}^{-1}}$$
3		relcnv	$$⊢\mathrm{Rel}{\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}$$
4		cnvf1o	$$⊢\mathrm{Rel}{\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}\to \left(x\in {\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right):{\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}\underset{1-1\; onto}{⟶}{{\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}}^{-1}$$
5	3 4	ax-mp	$$⊢\left(x\in {\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right):{\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}\underset{1-1\; onto}{⟶}{{\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}}^{-1}$$
6		f1ofo	$$⊢\left(x\in {\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right):{\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}\underset{1-1\; onto}{⟶}{{\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}}^{-1}\to \left(x\in {\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right):{\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}\underset{onto}{⟶}{{\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}}^{-1}$$
7	5 6	ax-mp	$$⊢\left(x\in {\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right):{\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}\underset{onto}{⟶}{{\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}}^{-1}$$
8		forn	$$⊢\left(x\in {\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right):{\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}\underset{onto}{⟶}{{\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}}^{-1}\to \mathrm{ran}\left(x\in {\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)={{\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}}^{-1}$$
9	7 8	ax-mp	$$⊢\mathrm{ran}\left(x\in {\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)={{\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}}^{-1}$$
10		cnvcnvss	$$⊢{{\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}}^{-1}\subseteq \mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)$$
11		resdmss	$$⊢\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)\subseteq R^{-1}$$
12	10 11	sstri	$$⊢{{\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}}^{-1}\subseteq R^{-1}$$
13	9 12	eqsstri	$$⊢\mathrm{ran}\left(x\in {\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)\subseteq R^{-1}$$
14		cores	$$⊢\mathrm{ran}\left(x\in {\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)\subseteq R^{-1}\to \left({F\upharpoonright }_{R^{-1}}\right)\circ \left(x\in {\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)=F\circ \left(x\in {\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
15	13 14	ax-mp	$$⊢\left({F\upharpoonright }_{R^{-1}}\right)\circ \left(x\in {\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)=F\circ \left(x\in {\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
16		dftpos6	$$⊢tpos\left({F\upharpoonright }_{R^{-1}}\right)=\left(\left({F\upharpoonright }_{R^{-1}}\right)\circ \left(x\in {\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)\right)\cup \left(\left\{\varnothing \right\}\times \left({F\upharpoonright }_{R^{-1}}\right)\left[\left\{\varnothing \right\}\right]\right)$$
17		ressn	$$⊢{\left({F\upharpoonright }_{R^{-1}}\right)\upharpoonright }_{\left\{\varnothing \right\}}=\left\{\varnothing \right\}\times \left({F\upharpoonright }_{R^{-1}}\right)\left[\left\{\varnothing \right\}\right]$$
18		resres	$$⊢{\left({F\upharpoonright }_{R^{-1}}\right)\upharpoonright }_{\left\{\varnothing \right\}}={F\upharpoonright }_{\left(R^{-1}\cap \left\{\varnothing \right\}\right)}$$
19		relcnv	$$⊢\mathrm{Rel}{R}^{-1}$$
20		0nelrel0	$$⊢\mathrm{Rel}{R}^{-1}\to \neg \varnothing \in R^{-1}$$
21	19 20	ax-mp	$$⊢\neg \varnothing \in R^{-1}$$
22		disjsn	$$⊢R^{-1}\cap \left\{\varnothing \right\}=\varnothing \leftrightarrow \neg \varnothing \in R^{-1}$$
23	21 22	mpbir	$$⊢R^{-1}\cap \left\{\varnothing \right\}=\varnothing$$
24	23	reseq2i	$$⊢{F\upharpoonright }_{\left(R^{-1}\cap \left\{\varnothing \right\}\right)}={F\upharpoonright }_{\varnothing }$$
25		res0	$$⊢{F\upharpoonright }_{\varnothing }=\varnothing$$
26	18 24 25	3eqtri	$$⊢{\left({F\upharpoonright }_{R^{-1}}\right)\upharpoonright }_{\left\{\varnothing \right\}}=\varnothing$$
27	17 26	eqtr3i	$$⊢\left\{\varnothing \right\}\times \left({F\upharpoonright }_{R^{-1}}\right)\left[\left\{\varnothing \right\}\right]=\varnothing$$
28	27	uneq2i	$$⊢\left(\left({F\upharpoonright }_{R^{-1}}\right)\circ \left(x\in {\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)\right)\cup \left(\left\{\varnothing \right\}\times \left({F\upharpoonright }_{R^{-1}}\right)\left[\left\{\varnothing \right\}\right]\right)=\left(\left({F\upharpoonright }_{R^{-1}}\right)\circ \left(x\in {\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)\right)\cup \varnothing$$
29		un0	$$⊢\left(\left({F\upharpoonright }_{R^{-1}}\right)\circ \left(x\in {\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)\right)\cup \varnothing =\left({F\upharpoonright }_{R^{-1}}\right)\circ \left(x\in {\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
30	16 28 29	3eqtri	$$⊢tpos\left({F\upharpoonright }_{R^{-1}}\right)=\left({F\upharpoonright }_{R^{-1}}\right)\circ \left(x\in {\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
31		tposrescnv	$$⊢{tposF\upharpoonright }_{{R^{-1}}^{-1}}=F\circ \left(x\in {\mathrm{dom}\left({F\upharpoonright }_{R^{-1}}\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
32	15 30 31	3eqtr4ri	$$⊢{tposF\upharpoonright }_{{R^{-1}}^{-1}}=tpos\left({F\upharpoonright }_{R^{-1}}\right)$$
33	2 32	eqtrdi	$$⊢\phi \to {tposF\upharpoonright }_R=tpos\left({F\upharpoonright }_{R^{-1}}\right)$$