Theorem tposideq

Description: Two ways of expressing the swap function. (Contributed by Zhi Wang, 6-Oct-2025)

	Ref	Expression
Assertion	tposideq	$$⊢\mathrm{Rel}R\to {tpos\mathrm{I}\upharpoonright }_R=\left(x\in R⟼\bigcup {\left\{x\right\}}^{-1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		tposres	$$⊢\mathrm{Rel}R\to {tpos\mathrm{I}\upharpoonright }_R=tpos\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)$$
2		relcnv	$$⊢\mathrm{Rel}{R}^{-1}$$
3		fnresi	$$⊢\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)Fn{R}^{-1}$$
4		tposfn2	$$⊢\mathrm{Rel}{R}^{-1}\to \left(\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)Fn{R}^{-1}\to tpos\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)Fn{R^{-1}}^{-1}\right)$$
5	2 3 4	mp2	$$⊢tpos\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)Fn{R^{-1}}^{-1}$$
6		dfrel2	$$⊢\mathrm{Rel}R\leftrightarrow {R^{-1}}^{-1}=R$$
7	6	biimpi	$$⊢\mathrm{Rel}R\to {R^{-1}}^{-1}=R$$
8	7	fneq2d	$$⊢\mathrm{Rel}R\to \left(tpos\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)Fn{R^{-1}}^{-1}\leftrightarrow tpos\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)FnR\right)$$
9	5 8	mpbii	$$⊢\mathrm{Rel}R\to tpos\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)FnR$$
10		vsnex	$$⊢\left\{x\right\}\in \mathrm{V}$$
11	10	cnvex	$$⊢{\left\{x\right\}}^{-1}\in \mathrm{V}$$
12	11	uniex	$$⊢\bigcup {\left\{x\right\}}^{-1}\in \mathrm{V}$$
13		eqid	$$⊢\left(x\in R⟼\bigcup {\left\{x\right\}}^{-1}\right)=\left(x\in R⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
14	12 13	fnmpti	$$⊢\left(x\in R⟼\bigcup {\left\{x\right\}}^{-1}\right)FnR$$
15	14	a1i	$$⊢\mathrm{Rel}R\to \left(x\in R⟼\bigcup {\left\{x\right\}}^{-1}\right)FnR$$
16		1st2nd	$$⊢\left(\mathrm{Rel}R\wedge y\in R\right)\to y=⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩$$
17		1st2ndb	$$⊢y\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow y=⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩$$
18	17	biimpri	$$⊢y=⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩\to y\in \left(\mathrm{V}\times \mathrm{V}\right)$$
19		2nd1st	$$⊢y\in \left(\mathrm{V}\times \mathrm{V}\right)\to \bigcup {\left\{y\right\}}^{-1}=⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩$$
20	16 18 19	3syl	$$⊢\left(\mathrm{Rel}R\wedge y\in R\right)\to \bigcup {\left\{y\right\}}^{-1}=⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩$$
21		sneq	$$⊢x=y\to \left\{x\right\}=\left\{y\right\}$$
22	21	cnveqd	$$⊢x=y\to {\left\{x\right\}}^{-1}={\left\{y\right\}}^{-1}$$
23	22	unieqd	$$⊢x=y\to \bigcup {\left\{x\right\}}^{-1}=\bigcup {\left\{y\right\}}^{-1}$$
24	23 13 12	fvmpt3i	$$⊢y\in R\to \left(x\in R⟼\bigcup {\left\{x\right\}}^{-1}\right)\left(y\right)=\bigcup {\left\{y\right\}}^{-1}$$
25	24	adantl	$$⊢\left(\mathrm{Rel}R\wedge y\in R\right)\to \left(x\in R⟼\bigcup {\left\{x\right\}}^{-1}\right)\left(y\right)=\bigcup {\left\{y\right\}}^{-1}$$
26	16	fveq2d	$$⊢\left(\mathrm{Rel}R\wedge y\in R\right)\to tpos\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)\left(y\right)=tpos\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)\left(⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩\right)$$
27		ovtpos	$$⊢1^{st}\left(y\right)tpos\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)2^{nd}\left(y\right)=2^{nd}\left(y\right)\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)1^{st}\left(y\right)$$
28		df-ov	$$⊢1^{st}\left(y\right)tpos\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)2^{nd}\left(y\right)=tpos\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)\left(⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩\right)$$
29		df-ov	$$⊢2^{nd}\left(y\right)\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)1^{st}\left(y\right)=\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)\left(⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩\right)$$
30	27 28 29	3eqtr3i	$$⊢tpos\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)\left(⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩\right)=\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)\left(⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩\right)$$
31	30	a1i	$$⊢\left(\mathrm{Rel}R\wedge y\in R\right)\to tpos\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)\left(⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩\right)=\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)\left(⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩\right)$$
32		simpr	$$⊢\left(\mathrm{Rel}R\wedge y\in R\right)\to y\in R$$
33	16 32	eqeltrrd	$$⊢\left(\mathrm{Rel}R\wedge y\in R\right)\to ⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩\in R$$
34		fvex	$$⊢2^{nd}\left(y\right)\in \mathrm{V}$$
35		fvex	$$⊢1^{st}\left(y\right)\in \mathrm{V}$$
36	34 35	opelcnv	$$⊢⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩\in R^{-1}\leftrightarrow ⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩\in R$$
37	36	biimpri	$$⊢⟨1^{st}\left(y\right),2^{nd}\left(y\right)⟩\in R\to ⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩\in R^{-1}$$
38		fvresi	$$⊢⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩\in R^{-1}\to \left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)\left(⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩\right)=⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩$$
39	33 37 38	3syl	$$⊢\left(\mathrm{Rel}R\wedge y\in R\right)\to \left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)\left(⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩\right)=⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩$$
40	26 31 39	3eqtrd	$$⊢\left(\mathrm{Rel}R\wedge y\in R\right)\to tpos\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)\left(y\right)=⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩$$
41	20 25 40	3eqtr4rd	$$⊢\left(\mathrm{Rel}R\wedge y\in R\right)\to tpos\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)\left(y\right)=\left(x\in R⟼\bigcup {\left\{x\right\}}^{-1}\right)\left(y\right)$$
42	9 15 41	eqfnfvd	$$⊢\mathrm{Rel}R\to tpos\left({\mathrm{I}\upharpoonright }_{R^{-1}}\right)=\left(x\in R⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
43	1 42	eqtrd	$$⊢\mathrm{Rel}R\to {tpos\mathrm{I}\upharpoonright }_R=\left(x\in R⟼\bigcup {\left\{x\right\}}^{-1}\right)$$