Theorem tposrescnv

Description: The transposition restricted to a converse is the transposition of the restricted class, with the empty set removed from the domain. Note that the right hand side is a more useful form of ` ( tpos ( F |`` R ) |`( _V \ { (/) } ) ) by df-tpos . (Contributed by Zhi Wang, 6-Oct-2025)

	Ref	Expression
Assertion	tposrescnv	$$⊢{tposF\upharpoonright }_{R^{-1}}=F\circ \left(x\in {\mathrm{dom}\left({F\upharpoonright }_R\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-tpos	$$⊢tposF=F\circ \left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
2	1	reseq1i	$$⊢{tposF\upharpoonright }_{R^{-1}}={\left(F\circ \left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\right)\upharpoonright }_{R^{-1}}$$
3		resco	$$⊢{\left(F\circ \left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\right)\upharpoonright }_{R^{-1}}=F\circ \left({\left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\upharpoonright }_{R^{-1}}\right)$$
4		resmpt3	$$⊢{\left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\upharpoonright }_{R^{-1}}=\left(x\in \left(\left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)\cap R^{-1}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
5		cnvin	$$⊢{\left(R\cap \mathrm{dom}F\right)}^{-1}=R^{-1}\cap {\mathrm{dom}F}^{-1}$$
6		dmres	$$⊢\mathrm{dom}\left({F\upharpoonright }_R\right)=R\cap \mathrm{dom}F$$
7	6	cnveqi	$$⊢{\mathrm{dom}\left({F\upharpoonright }_R\right)}^{-1}={\left(R\cap \mathrm{dom}F\right)}^{-1}$$
8		incom	$$⊢\left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)\cap R^{-1}=R^{-1}\cap \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)$$
9		indi	$$⊢R^{-1}\cap \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)=\left(R^{-1}\cap {\mathrm{dom}F}^{-1}\right)\cup \left(R^{-1}\cap \left\{\varnothing \right\}\right)$$
10		relcnv	$$⊢\mathrm{Rel}{R}^{-1}$$
11		0nelrel0	$$⊢\mathrm{Rel}{R}^{-1}\to \neg \varnothing \in R^{-1}$$
12	10 11	ax-mp	$$⊢\neg \varnothing \in R^{-1}$$
13		disjsn	$$⊢R^{-1}\cap \left\{\varnothing \right\}=\varnothing \leftrightarrow \neg \varnothing \in R^{-1}$$
14	12 13	mpbir	$$⊢R^{-1}\cap \left\{\varnothing \right\}=\varnothing$$
15	14	uneq2i	$$⊢\left(R^{-1}\cap {\mathrm{dom}F}^{-1}\right)\cup \left(R^{-1}\cap \left\{\varnothing \right\}\right)=\left(R^{-1}\cap {\mathrm{dom}F}^{-1}\right)\cup \varnothing$$
16		un0	$$⊢\left(R^{-1}\cap {\mathrm{dom}F}^{-1}\right)\cup \varnothing =R^{-1}\cap {\mathrm{dom}F}^{-1}$$
17	15 16	eqtri	$$⊢\left(R^{-1}\cap {\mathrm{dom}F}^{-1}\right)\cup \left(R^{-1}\cap \left\{\varnothing \right\}\right)=R^{-1}\cap {\mathrm{dom}F}^{-1}$$
18	8 9 17	3eqtri	$$⊢\left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)\cap R^{-1}=R^{-1}\cap {\mathrm{dom}F}^{-1}$$
19	5 7 18	3eqtr4ri	$$⊢\left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)\cap R^{-1}={\mathrm{dom}\left({F\upharpoonright }_R\right)}^{-1}$$
20	19	mpteq1i	$$⊢\left(x\in \left(\left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)\cap R^{-1}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)=\left(x\in {\mathrm{dom}\left({F\upharpoonright }_R\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
21	4 20	eqtri	$$⊢{\left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\upharpoonright }_{R^{-1}}=\left(x\in {\mathrm{dom}\left({F\upharpoonright }_R\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
22	21	coeq2i	$$⊢F\circ \left({\left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\upharpoonright }_{R^{-1}}\right)=F\circ \left(x\in {\mathrm{dom}\left({F\upharpoonright }_R\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
23	2 3 22	3eqtri	$$⊢{tposF\upharpoonright }_{R^{-1}}=F\circ \left(x\in {\mathrm{dom}\left({F\upharpoonright }_R\right)}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)$$