Definition df-pmtr

Description: Define a function that generates the transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015)

	Ref	Expression
Assertion	df-pmtr	$$⊢\mathrm{pmTrsp}=\left(d\in \mathrm{V}⟼\left(p\in \left\{y\in 𝒫d|y\approx 2_{𝑜}\right\}⟼\left(z\in d⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpmtr	$$class\mathrm{pmTrsp}$$
1		vd	$$setvard$$
2		cvv	$$class\mathrm{V}$$
3		vp	$$setvarp$$
4		vy	$$setvary$$
5	1	cv	$$setvard$$
6	5	cpw	$$class𝒫d$$
7	4	cv	$$setvary$$
8		cen	$$class\approx$$
9		c2o	$$class{2}_{𝑜}$$
10	7 9 8	wbr	$$wffy\approx 2_{𝑜}$$
11	10 4 6	crab	$$class\left\{y\in 𝒫d|y\approx 2_{𝑜}\right\}$$
12		vz	$$setvarz$$
13	12	cv	$$setvarz$$
14	3	cv	$$setvarp$$
15	13 14	wcel	$$wffz\in p$$
16	13	csn	$$class\left\{z\right\}$$
17	14 16	cdif	$$class\left(p\setminus \left\{z\right\}\right)$$
18	17	cuni	$$class\bigcup \left(p\setminus \left\{z\right\}\right)$$
19	15 18 13	cif	$$classif\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)$$
20	12 5 19	cmpt	$$class\left(z\in d⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)$$
21	3 11 20	cmpt	$$class\left(p\in \left\{y\in 𝒫d|y\approx 2_{𝑜}\right\}⟼\left(z\in d⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\right)$$
22	1 2 21	cmpt	$$class\left(d\in \mathrm{V}⟼\left(p\in \left\{y\in 𝒫d|y\approx 2_{𝑜}\right\}⟼\left(z\in d⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\right)\right)$$
23	0 22	wceq	$$wff\mathrm{pmTrsp}=\left(d\in \mathrm{V}⟼\left(p\in \left\{y\in 𝒫d|y\approx 2_{𝑜}\right\}⟼\left(z\in d⟼if\left(z\in p,\bigcup \left(p\setminus \left\{z\right\}\right),z\right)\right)\right)\right)$$