MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-pmtr Structured version   Unicode version

Definition df-pmtr 16068
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
StepHypRef Expression
1 cpmtr 16067 . 2  class pmTrsp
2 vd . . 3  setvar  d
3 cvv 3078 . . 3  class  _V
4 vp . . . 4  setvar  p
5 vy . . . . . . 7  setvar  y
65cv 1369 . . . . . 6  class  y
7 c2o 7025 . . . . . 6  class  2o
8 cen 7418 . . . . . 6  class  ~~
96, 7, 8wbr 4401 . . . . 5  wff  y  ~~  2o
102cv 1369 . . . . . 6  class  d
1110cpw 3969 . . . . 5  class  ~P d
129, 5, 11crab 2803 . . . 4  class  { y  e.  ~P d  |  y  ~~  2o }
13 vz . . . . 5  setvar  z
1413, 4wel 1759 . . . . . 6  wff  z  e.  p
154cv 1369 . . . . . . . 8  class  p
1613cv 1369 . . . . . . . . 9  class  z
1716csn 3986 . . . . . . . 8  class  { z }
1815, 17cdif 3434 . . . . . . 7  class  ( p 
\  { z } )
1918cuni 4200 . . . . . 6  class  U. (
p  \  { z } )
2014, 19, 16cif 3900 . . . . 5  class  if ( z  e.  p , 
U. ( p  \  { z } ) ,  z )
2113, 10, 20cmpt 4459 . . . 4  class  ( z  e.  d  |->  if ( z  e.  p , 
U. ( p  \  { z } ) ,  z ) )
224, 12, 21cmpt 4459 . . 3  class  ( p  e.  { y  e. 
~P d  |  y 
~~  2o }  |->  ( z  e.  d  |->  if ( z  e.  p ,  U. ( p  \  { z } ) ,  z ) ) )
232, 3, 22cmpt 4459 . 2  class  ( d  e.  _V  |->  ( p  e.  { y  e. 
~P d  |  y 
~~  2o }  |->  ( z  e.  d  |->  if ( z  e.  p ,  U. ( p  \  { z } ) ,  z ) ) ) )
241, 23wceq 1370 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 ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  pmtrfval  16076
  Copyright terms: Public domain W3C validator