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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpmtr	⊢ pmTrsp
1		vd	⊢ 𝑑
2		cvv	⊢ V
3		vp	⊢ 𝑝
4		vy	⊢ 𝑦
5	1	cv	⊢ 𝑑
6	5	cpw	⊢ 𝒫 𝑑
7	4	cv	⊢ 𝑦
8		cen	⊢ ≈
9		c2o	⊢ 2o
10	7 9 8	wbr	⊢ 𝑦 ≈ 2o
11	10 4 6	crab	⊢ { 𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o }
12		vz	⊢ 𝑧
13	12	cv	⊢ 𝑧
14	3	cv	⊢ 𝑝
15	13 14	wcel	⊢ 𝑧 ∈ 𝑝
16	13	csn	⊢ { 𝑧 }
17	14 16	cdif	⊢ ( 𝑝 ∖ { 𝑧 } )
18	17	cuni	⊢ ∪ ( 𝑝 ∖ { 𝑧 } )
19	15 18 13	cif	⊢ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 )
20	12 5 19	cmpt	⊢ ( 𝑧 ∈ 𝑑 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) )
21	3 11 20	cmpt	⊢ ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝑑 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) )
22	1 2 21	cmpt	⊢ ( 𝑑 ∈ V ↦ ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝑑 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) )
23	0 22	wceq	⊢ pmTrsp = ( 𝑑 ∈ V ↦ ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝑑 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) )