Definition df-pmtr 17862

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

Assertion

Ref	Expression
df-pmtr	⊢ pmTrsp = (𝑑 ∈ V ↦ (𝑝 ∈ {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2𝑜} ↦ (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))))

Distinct variable group:   𝑝,𝑑,𝑦,𝑧

Detailed syntax breakdown of Definition df-pmtr

Step	Hyp	Ref	Expression
1		cpmtr 17861	. 2 class pmTrsp
2		vd	. . 3 setvar 𝑑
3		cvv 3200	. . 3 class V
4		vp	. . . 4 setvar 𝑝
5		vy	. . . . . . 7 setvar 𝑦
6	5	cv 1482	. . . . . 6 class 𝑦
7		c2o 7554	. . . . . 6 class 2𝑜
8		cen 7952	. . . . . 6 class ≈
9	6, 7, 8	wbr 4653	. . . . 5 wff 𝑦 ≈ 2𝑜
10	2	cv 1482	. . . . . 6 class 𝑑
11	10	cpw 4158	. . . . 5 class 𝒫 𝑑
12	9, 5, 11	crab 2916	. . . 4 class {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2𝑜}
13		vz	. . . . 5 setvar 𝑧
14	13, 4	wel 1991	. . . . . 6 wff 𝑧 ∈ 𝑝
15	4	cv 1482	. . . . . . . 8 class 𝑝
16	13	cv 1482	. . . . . . . . 9 class 𝑧
17	16	csn 4177	. . . . . . . 8 class {𝑧}
18	15, 17	cdif 3571	. . . . . . 7 class (𝑝 ∖ {𝑧})
19	18	cuni 4436	. . . . . 6 class ∪ (𝑝 ∖ {𝑧})
20	14, 19, 16	cif 4086	. . . . 5 class if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)
21	13, 10, 20	cmpt 4729	. . . 4 class (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))
22	4, 12, 21	cmpt 4729	. . 3 class (𝑝 ∈ {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2𝑜} ↦ (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))
23	2, 3, 22	cmpt 4729	. 2 class (𝑑 ∈ V ↦ (𝑝 ∈ {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2𝑜} ↦ (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))))
24	1, 23	wceq 1483	1 wff pmTrsp = (𝑑 ∈ V ↦ (𝑝 ∈ {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2𝑜} ↦ (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))))

This definition is referenced by:  pmtrfval  17870