Theorem pmtrprfval

Description: The transpositions on a pair. (Contributed by AV, 9-Dec-2018)

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		prex	$$⊢\left\{1,2\right\}\in \mathrm{V}$$
2		eqid	$$⊢\mathrm{pmTrsp}\left(\left\{1,2\right\}\right)=\mathrm{pmTrsp}\left(\left\{1,2\right\}\right)$$
3	2	pmtrfval	$$⊢\left\{1,2\right\}\in \mathrm{V}\to \mathrm{pmTrsp}\left(\left\{1,2\right\}\right)=\left(p\in \left\{t\in 𝒫\left\{1,2\right\}|t\approx 2_{𝑜}\right\}⟼\left(z\in \left\{1,2\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\right)$$
4	1 3	ax-mp	$$⊢\mathrm{pmTrsp}\left(\left\{1,2\right\}\right)=\left(p\in \left\{t\in 𝒫\left\{1,2\right\}|t\approx 2_{𝑜}\right\}⟼\left(z\in \left\{1,2\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\right)$$
5		1ex	$$⊢1\in \mathrm{V}$$
6		2nn0	$$⊢2\in {\mathbb{N}}_0$$
7		1ne2	$$⊢1\ne 2$$
8		pr2pwpr	$$⊢\left(1\in \mathrm{V}\wedge 2\in {\mathbb{N}}_0\wedge 1\ne 2\right)\to \left\{t\in 𝒫\left\{1,2\right\}|t\approx 2_{𝑜}\right\}=\left\{\left\{1,2\right\}\right\}$$
9	5 6 7 8	mp3an	$$⊢\left\{t\in 𝒫\left\{1,2\right\}|t\approx 2_{𝑜}\right\}=\left\{\left\{1,2\right\}\right\}$$
10	9	mpteq1i	$$⊢\left(p\in \left\{t\in 𝒫\left\{1,2\right\}|t\approx 2_{𝑜}\right\}⟼\left(z\in \left\{1,2\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\right)=\left(p\in \left\{\left\{1,2\right\}\right\}⟼\left(z\in \left\{1,2\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\right)$$
11		elsni	$$⊢p\in \left\{\left\{1,2\right\}\right\}\to p=\left\{1,2\right\}$$
12		eleq2	$$⊢p=\left\{1,2\right\}\to \left(z\in p\leftrightarrow z\in \left\{1,2\right\}\right)$$
13	12	biimpar	$$⊢\left(p=\left\{1,2\right\}\wedge z\in \left\{1,2\right\}\right)\to z\in p$$
14	13	iftrued	$$⊢\left(p=\left\{1,2\right\}\wedge z\in \left\{1,2\right\}\right)\to if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)=\bigcup \left(p\setminus \left\{z\right\}\right)$$
15		elpri	$$⊢z\in \left\{1,2\right\}\to \left(z=1\vee z=2\right)$$
16		2ex	$$⊢2\in \mathrm{V}$$
17	16	unisn	$$⊢\bigcup \left\{2\right\}=2$$
18		simpr	$$⊢\left(z=1\wedge p=\left\{1,2\right\}\right)\to p=\left\{1,2\right\}$$
19		sneq	$$⊢z=1\to \left\{z\right\}=\left\{1\right\}$$
20	19	adantr	$$⊢\left(z=1\wedge p=\left\{1,2\right\}\right)\to \left\{z\right\}=\left\{1\right\}$$
21	18 20	difeq12d	$$⊢\left(z=1\wedge p=\left\{1,2\right\}\right)\to p\setminus \left\{z\right\}=\left\{1,2\right\}\setminus \left\{1\right\}$$
22		difprsn1	$$⊢1\ne 2\to \left\{1,2\right\}\setminus \left\{1\right\}=\left\{2\right\}$$
23	7 22	ax-mp	$$⊢\left\{1,2\right\}\setminus \left\{1\right\}=\left\{2\right\}$$
24	21 23	eqtrdi	$$⊢\left(z=1\wedge p=\left\{1,2\right\}\right)\to p\setminus \left\{z\right\}=\left\{2\right\}$$
25	24	unieqd	$$⊢\left(z=1\wedge p=\left\{1,2\right\}\right)\to \bigcup \left(p\setminus \left\{z\right\}\right)=\bigcup \left\{2\right\}$$
26		iftrue	$$⊢z=1\to if\left(z=1,2,1\right)=2$$
27	26	adantr	$$⊢\left(z=1\wedge p=\left\{1,2\right\}\right)\to if\left(z=1,2,1\right)=2$$
28	17 25 27	3eqtr4a	$$⊢\left(z=1\wedge p=\left\{1,2\right\}\right)\to \bigcup \left(p\setminus \left\{z\right\}\right)=if\left(z=1,2,1\right)$$
29	28	ex	$$⊢z=1\to \left(p=\left\{1,2\right\}\to \bigcup \left(p\setminus \left\{z\right\}\right)=if\left(z=1,2,1\right)\right)$$
30	5	unisn	$$⊢\bigcup \left\{1\right\}=1$$
31		simpr	$$⊢\left(z=2\wedge p=\left\{1,2\right\}\right)\to p=\left\{1,2\right\}$$
32		sneq	$$⊢z=2\to \left\{z\right\}=\left\{2\right\}$$
33	32	adantr	$$⊢\left(z=2\wedge p=\left\{1,2\right\}\right)\to \left\{z\right\}=\left\{2\right\}$$
34	31 33	difeq12d	$$⊢\left(z=2\wedge p=\left\{1,2\right\}\right)\to p\setminus \left\{z\right\}=\left\{1,2\right\}\setminus \left\{2\right\}$$
35		difprsn2	$$⊢1\ne 2\to \left\{1,2\right\}\setminus \left\{2\right\}=\left\{1\right\}$$
36	7 35	ax-mp	$$⊢\left\{1,2\right\}\setminus \left\{2\right\}=\left\{1\right\}$$
37	34 36	eqtrdi	$$⊢\left(z=2\wedge p=\left\{1,2\right\}\right)\to p\setminus \left\{z\right\}=\left\{1\right\}$$
38	37	unieqd	$$⊢\left(z=2\wedge p=\left\{1,2\right\}\right)\to \bigcup \left(p\setminus \left\{z\right\}\right)=\bigcup \left\{1\right\}$$
39	7	nesymi	$$⊢\neg 2=1$$
40		eqeq1	$$⊢z=2\to \left(z=1\leftrightarrow 2=1\right)$$
41	39 40	mtbiri	$$⊢z=2\to \neg z=1$$
42	41	iffalsed	$$⊢z=2\to if\left(z=1,2,1\right)=1$$
43	42	adantr	$$⊢\left(z=2\wedge p=\left\{1,2\right\}\right)\to if\left(z=1,2,1\right)=1$$
44	30 38 43	3eqtr4a	$$⊢\left(z=2\wedge p=\left\{1,2\right\}\right)\to \bigcup \left(p\setminus \left\{z\right\}\right)=if\left(z=1,2,1\right)$$
45	44	ex	$$⊢z=2\to \left(p=\left\{1,2\right\}\to \bigcup \left(p\setminus \left\{z\right\}\right)=if\left(z=1,2,1\right)\right)$$
46	29 45	jaoi	$$⊢\left(z=1\vee z=2\right)\to \left(p=\left\{1,2\right\}\to \bigcup \left(p\setminus \left\{z\right\}\right)=if\left(z=1,2,1\right)\right)$$
47	15 46	syl	$$⊢z\in \left\{1,2\right\}\to \left(p=\left\{1,2\right\}\to \bigcup \left(p\setminus \left\{z\right\}\right)=if\left(z=1,2,1\right)\right)$$
48	47	impcom	$$⊢\left(p=\left\{1,2\right\}\wedge z\in \left\{1,2\right\}\right)\to \bigcup \left(p\setminus \left\{z\right\}\right)=if\left(z=1,2,1\right)$$
49	14 48	eqtrd	$$⊢\left(p=\left\{1,2\right\}\wedge z\in \left\{1,2\right\}\right)\to if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)=if\left(z=1,2,1\right)$$
50	11 49	sylan	$$⊢\left(p\in \left\{\left\{1,2\right\}\right\}\wedge z\in \left\{1,2\right\}\right)\to if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)=if\left(z=1,2,1\right)$$
51	50	mpteq2dva	$$⊢p\in \left\{\left\{1,2\right\}\right\}\to \left(z\in \left\{1,2\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)=\left(z\in \left\{1,2\right\}⟼if\left(z=1,2,1\right)\right)$$
52	51	mpteq2ia	$$⊢\left(p\in \left\{\left\{1,2\right\}\right\}⟼\left(z\in \left\{1,2\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\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)$$
53	10 52	eqtri	$$⊢\left(p\in \left\{t\in 𝒫\left\{1,2\right\}|t\approx 2_{𝑜}\right\}⟼\left(z\in \left\{1,2\right\}⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\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)$$
54	4 53	eqtri	$$⊢\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)$$