Theorem pmtrprfvalrn

Description: The range of the transpositions on a pair is actually a singleton: the transposition of the two elements of the pair. (Contributed by AV, 9-Dec-2018)

	Ref	Expression
Assertion	pmtrprfvalrn	$$⊢\mathrm{ran}\mathrm{pmTrsp}\left(\left\{1,2\right\}\right)=\left\{\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		pmtrprfval	$$⊢\mathrm{pmTrsp}\left(\left\{1,2\right\}\right)=\left(p\in \left\{\left\{1,2\right\}\right\}⟼\left(z\in \left\{1,2\right\}⟼if\left(z=1,2,1\right)\right)\right)$$
2	1	rneqi	$$⊢\mathrm{ran}\mathrm{pmTrsp}\left(\left\{1,2\right\}\right)=\mathrm{ran}\left(p\in \left\{\left\{1,2\right\}\right\}⟼\left(z\in \left\{1,2\right\}⟼if\left(z=1,2,1\right)\right)\right)$$
3		eqid	$$⊢\left(p\in \left\{\left\{1,2\right\}\right\}⟼\left(z\in \left\{1,2\right\}⟼if\left(z=1,2,1\right)\right)\right)=\left(p\in \left\{\left\{1,2\right\}\right\}⟼\left(z\in \left\{1,2\right\}⟼if\left(z=1,2,1\right)\right)\right)$$
4	3	rnmpt	$$⊢\mathrm{ran}\left(p\in \left\{\left\{1,2\right\}\right\}⟼\left(z\in \left\{1,2\right\}⟼if\left(z=1,2,1\right)\right)\right)=\left\{t|\exists p\in \left\{\left\{1,2\right\}\right\}t=\left(z\in \left\{1,2\right\}⟼if\left(z=1,2,1\right)\right)\right\}$$
5		1ex	$$⊢1\in \mathrm{V}$$
6		id	$$⊢1\in \mathrm{V}\to 1\in \mathrm{V}$$
7		2nn	$$⊢2\in \mathbb{N}$$
8	7	a1i	$$⊢1\in \mathrm{V}\to 2\in \mathbb{N}$$
9		iftrue	$$⊢z=1\to if\left(z=1,2,1\right)=2$$
10	9	adantl	$$⊢\left(1\in \mathrm{V}\wedge z=1\right)\to if\left(z=1,2,1\right)=2$$
11		1ne2	$$⊢1\ne 2$$
12	11	nesymi	$$⊢\neg 2=1$$
13		eqeq1	$$⊢z=2\to \left(z=1\leftrightarrow 2=1\right)$$
14	12 13	mtbiri	$$⊢z=2\to \neg z=1$$
15	14	iffalsed	$$⊢z=2\to if\left(z=1,2,1\right)=1$$
16	15	adantl	$$⊢\left(1\in \mathrm{V}\wedge z=2\right)\to if\left(z=1,2,1\right)=1$$
17	6 8 8 6 10 16	fmptpr	$$⊢1\in \mathrm{V}\to \left\{⟨1,2⟩,⟨2,1⟩\right\}=\left(z\in \left\{1,2\right\}⟼if\left(z=1,2,1\right)\right)$$
18	17	eqeq2d	$$⊢1\in \mathrm{V}\to \left(t=\left\{⟨1,2⟩,⟨2,1⟩\right\}\leftrightarrow t=\left(z\in \left\{1,2\right\}⟼if\left(z=1,2,1\right)\right)\right)$$
19	5 18	ax-mp	$$⊢t=\left\{⟨1,2⟩,⟨2,1⟩\right\}\leftrightarrow t=\left(z\in \left\{1,2\right\}⟼if\left(z=1,2,1\right)\right)$$
20	19	bicomi	$$⊢t=\left(z\in \left\{1,2\right\}⟼if\left(z=1,2,1\right)\right)\leftrightarrow t=\left\{⟨1,2⟩,⟨2,1⟩\right\}$$
21	20	rexbii	$$⊢\exists p\in \left\{\left\{1,2\right\}\right\}t=\left(z\in \left\{1,2\right\}⟼if\left(z=1,2,1\right)\right)\leftrightarrow \exists p\in \left\{\left\{1,2\right\}\right\}t=\left\{⟨1,2⟩,⟨2,1⟩\right\}$$
22	21	abbii	$$⊢\left\{t|\exists p\in \left\{\left\{1,2\right\}\right\}t=\left(z\in \left\{1,2\right\}⟼if\left(z=1,2,1\right)\right)\right\}=\left\{t|\exists p\in \left\{\left\{1,2\right\}\right\}t=\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}$$
23		prex	$$⊢\left\{1,2\right\}\in \mathrm{V}$$
24	23	snnz	$$⊢\left\{\left\{1,2\right\}\right\}\ne \varnothing$$
25		r19.9rzv	$$⊢\left\{\left\{1,2\right\}\right\}\ne \varnothing \to \left(s=\left\{⟨1,2⟩,⟨2,1⟩\right\}\leftrightarrow \exists p\in \left\{\left\{1,2\right\}\right\}s=\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)$$
26	25	bicomd	$$⊢\left\{\left\{1,2\right\}\right\}\ne \varnothing \to \left(\exists p\in \left\{\left\{1,2\right\}\right\}s=\left\{⟨1,2⟩,⟨2,1⟩\right\}\leftrightarrow s=\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)$$
27	24 26	ax-mp	$$⊢\exists p\in \left\{\left\{1,2\right\}\right\}s=\left\{⟨1,2⟩,⟨2,1⟩\right\}\leftrightarrow s=\left\{⟨1,2⟩,⟨2,1⟩\right\}$$
28		vex	$$⊢s\in \mathrm{V}$$
29		eqeq1	$$⊢t=s\to \left(t=\left\{⟨1,2⟩,⟨2,1⟩\right\}\leftrightarrow s=\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)$$
30	29	rexbidv	$$⊢t=s\to \left(\exists p\in \left\{\left\{1,2\right\}\right\}t=\left\{⟨1,2⟩,⟨2,1⟩\right\}\leftrightarrow \exists p\in \left\{\left\{1,2\right\}\right\}s=\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)$$
31	28 30	elab	$$⊢s\in \left\{t|\exists p\in \left\{\left\{1,2\right\}\right\}t=\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}\leftrightarrow \exists p\in \left\{\left\{1,2\right\}\right\}s=\left\{⟨1,2⟩,⟨2,1⟩\right\}$$
32		velsn	$$⊢s\in \left\{\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}\leftrightarrow s=\left\{⟨1,2⟩,⟨2,1⟩\right\}$$
33	27 31 32	3bitr4i	$$⊢s\in \left\{t|\exists p\in \left\{\left\{1,2\right\}\right\}t=\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}\leftrightarrow s\in \left\{\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}$$
34	33	eqriv	$$⊢\left\{t|\exists p\in \left\{\left\{1,2\right\}\right\}t=\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}=\left\{\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}$$
35	22 34	eqtri	$$⊢\left\{t|\exists p\in \left\{\left\{1,2\right\}\right\}t=\left(z\in \left\{1,2\right\}⟼if\left(z=1,2,1\right)\right)\right\}=\left\{\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}$$
36	4 35	eqtri	$$⊢\mathrm{ran}\left(p\in \left\{\left\{1,2\right\}\right\}⟼\left(z\in \left\{1,2\right\}⟼if\left(z=1,2,1\right)\right)\right)=\left\{\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}$$
37	2 36	eqtri	$$⊢\mathrm{ran}\mathrm{pmTrsp}\left(\left\{1,2\right\}\right)=\left\{\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}$$