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

Definition df-pmtr 17068
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 17067 . 2  class pmTrsp
2 vd . . 3  setvar  d
3 cvv 3081 . . 3  class  _V
4 vp . . . 4  setvar  p
5 vy . . . . . . 7  setvar  y
65cv 1436 . . . . . 6  class  y
7 c2o 7180 . . . . . 6  class  2o
8 cen 7570 . . . . . 6  class  ~~
96, 7, 8wbr 4420 . . . . 5  wff  y  ~~  2o
102cv 1436 . . . . . 6  class  d
1110cpw 3979 . . . . 5  class  ~P d
129, 5, 11crab 2779 . . . 4  class  { y  e.  ~P d  |  y  ~~  2o }
13 vz . . . . 5  setvar  z
1413, 4wel 1869 . . . . . 6  wff  z  e.  p
154cv 1436 . . . . . . . 8  class  p
1613cv 1436 . . . . . . . . 9  class  z
1716csn 3996 . . . . . . . 8  class  { z }
1815, 17cdif 3433 . . . . . . 7  class  ( p 
\  { z } )
1918cuni 4216 . . . . . 6  class  U. (
p  \  { z } )
2014, 19, 16cif 3909 . . . . 5  class  if ( z  e.  p , 
U. ( p  \  { z } ) ,  z )
2113, 10, 20cmpt 4479 . . . 4  class  ( z  e.  d  |->  if ( z  e.  p , 
U. ( p  \  { z } ) ,  z ) )
224, 12, 21cmpt 4479 . . 3  class  ( p  e.  { y  e. 
~P d  |  y 
~~  2o }  |->  ( z  e.  d  |->  if ( z  e.  p ,  U. ( p  \  { z } ) ,  z ) ) )
232, 3, 22cmpt 4479 . 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 1437 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  17076
  Copyright terms: Public domain W3C validator