Definition df-pmtr 17138

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 = ( d e. _V |-> ( p e. { y e. ~P d | y ~~ 2o } |-> ( z e. d |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) )

Distinct variable group:   p, d, y, z

Detailed syntax breakdown of Definition df-pmtr

Step	Hyp	Ref	Expression
1		cpmtr 17137	. 2 class pmTrsp
2		vd	. . 3 setvar d
3		cvv 3057	. . 3 class _V
4		vp	. . . 4 setvar p
5		vy	. . . . . . 7 setvar y
6	5	cv 1454	. . . . . 6 class y
7		c2o 7207	. . . . . 6 class 2o
8		cen 7597	. . . . . 6 class ~~
9	6, 7, 8	wbr 4418	. . . . 5 wff y ~~ 2o
10	2	cv 1454	. . . . . 6 class d
11	10	cpw 3963	. . . . 5 class ~P d
12	9, 5, 11	crab 2753	. . . 4 class { y e. ~P d | y ~~ 2o }
13		vz	. . . . 5 setvar z
14	13, 4	wel 1899	. . . . . 6 wff z e. p
15	4	cv 1454	. . . . . . . 8 class p
16	13	cv 1454	. . . . . . . . 9 class z
17	16	csn 3980	. . . . . . . 8 class { z }
18	15, 17	cdif 3413	. . . . . . 7 class ( p \ { z } )
19	18	cuni 4212	. . . . . 6 class U. ( p \ { z } )
20	14, 19, 16	cif 3893	. . . . 5 class if ( z e. p , U. ( p \ { z } ) , z )
21	13, 10, 20	cmpt 4477	. . . 4 class ( z e. d |-> if ( z e. p , U. ( p \ { z } ) , z ) )
22	4, 12, 21	cmpt 4477	. . 3 class ( p e. { y e. ~P d | y ~~ 2o } |-> ( z e. d |-> if ( z e. p , U. ( p \ { z } ) , z ) ) )
23	2, 3, 22	cmpt 4477	. 2 class ( d e. _V |-> ( p e. { y e. ~P d | y ~~ 2o } |-> ( z e. d |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) )
24	1, 23	wceq 1455	1 wff pmTrsp = ( d e. _V |-> ( p e. { y e. ~P d | y ~~ 2o } |-> ( z e. d |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) )

This definition is referenced by:  pmtrfval  17146