Definition df-pmtr 18965

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 ↦ (𝑝 ∈ {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))))

Distinct variable group:   𝑝,𝑑,𝑦,𝑧

Detailed syntax breakdown of Definition df-pmtr

Step	Hyp	Ref	Expression
1		cpmtr 18964	. 2 class pmTrsp
2		vd	. . 3 setvar 𝑑
3		cvv 3422	. . 3 class V
4		vp	. . . 4 setvar 𝑝
5		vy	. . . . . . 7 setvar 𝑦
6	5	cv 1538	. . . . . 6 class 𝑦
7		c2o 8261	. . . . . 6 class 2o
8		cen 8688	. . . . . 6 class ≈
9	6, 7, 8	wbr 5070	. . . . 5 wff 𝑦 ≈ 2o
10	2	cv 1538	. . . . . 6 class 𝑑
11	10	cpw 4530	. . . . 5 class 𝒫 𝑑
12	9, 5, 11	crab 3067	. . . 4 class {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o}
13		vz	. . . . 5 setvar 𝑧
14	13, 4	wel 2109	. . . . . 6 wff 𝑧 ∈ 𝑝
15	4	cv 1538	. . . . . . . 8 class 𝑝
16	13	cv 1538	. . . . . . . . 9 class 𝑧
17	16	csn 4558	. . . . . . . 8 class {𝑧}
18	15, 17	cdif 3880	. . . . . . 7 class (𝑝 ∖ {𝑧})
19	18	cuni 4836	. . . . . 6 class ∪ (𝑝 ∖ {𝑧})
20	14, 19, 16	cif 4456	. . . . 5 class if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)
21	13, 10, 20	cmpt 5153	. . . 4 class (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))
22	4, 12, 21	cmpt 5153	. . 3 class (𝑝 ∈ {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))
23	2, 3, 22	cmpt 5153	. 2 class (𝑑 ∈ V ↦ (𝑝 ∈ {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))))
24	1, 23	wceq 1539	1 wff pmTrsp = (𝑑 ∈ V ↦ (𝑝 ∈ {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))))

This definition is referenced by:  pmtrfval  18973