Metamath Proof Explorer

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpmtr 
 |-  pmTrsp
1 vd 
 |-  d
2 cvv 
 |-  _V
3 vp 
 |-  p
4 vy 
 |-  y
5 1 cv 
 |-  d
6 5 cpw 
 |-  ~P d
7 4 cv 
 |-  y
8 cen 
 |-  ~~
9 c2o 
 |-  2o
10 7 9 8 wbr 
 |-  y ~~ 2o
11 10 4 6 crab 
 |-  { y e. ~P d | y ~~ 2o }
12 vz 
 |-  z
13 12 cv 
 |-  z
14 3 cv 
 |-  p
15 13 14 wcel 
 |-  z e. p
16 13 csn 
 |-  { z }
17 14 16 cdif 
 |-  ( p \ { z } )
18 17 cuni 
 |-  U. ( p \ { z } )
19 15 18 13 cif 
 |-  if ( z e. p , U. ( p \ { z } ) , z )
20 12 5 19 cmpt 
 |-  ( z e. d |-> if ( z e. p , U. ( p \ { z } ) , z ) )
21 3 11 20 cmpt 
 |-  ( p e. { y e. ~P d | y ~~ 2o } |-> ( z e. d |-> if ( z e. p , U. ( p \ { z } ) , z ) ) )
22 1 2 21 cmpt 
 |-  ( d e. _V |-> ( p e. { y e. ~P d | y ~~ 2o } |-> ( z e. d |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) )
23 0 22 wceq 
 |-  pmTrsp = ( d e. _V |-> ( p e. { y e. ~P d | y ~~ 2o } |-> ( z e. d |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) )