Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-pmtr Unicode version

Definition df-pmtr 27488
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 27487 . 2  class pmTrsp
2 vd . . 3  set  d
3 cvv 2801 . . 3  class  _V
4 vp . . . 4  set  p
5 vy . . . . . . 7  set  y
65cv 1631 . . . . . 6  class  y
7 c2o 6489 . . . . . 6  class  2o
8 cen 6876 . . . . . 6  class  ~~
96, 7, 8wbr 4039 . . . . 5  wff  y  ~~  2o
102cv 1631 . . . . . 6  class  d
1110cpw 3638 . . . . 5  class  ~P d
129, 5, 11crab 2560 . . . 4  class  { y  e.  ~P d  |  y  ~~  2o }
13 vz . . . . 5  set  z
1413, 4wel 1697 . . . . . 6  wff  z  e.  p
154cv 1631 . . . . . . . 8  class  p
1613cv 1631 . . . . . . . . 9  class  z
1716csn 3653 . . . . . . . 8  class  { z }
1815, 17cdif 3162 . . . . . . 7  class  ( p 
\  { z } )
1918cuni 3843 . . . . . 6  class  U. (
p  \  { z } )
2014, 19, 16cif 3578 . . . . 5  class  if ( z  e.  p , 
U. ( p  \  { z } ) ,  z )
2113, 10, 20cmpt 4093 . . . 4  class  ( z  e.  d  |->  if ( z  e.  p , 
U. ( p  \  { z } ) ,  z ) )
224, 12, 21cmpt 4093 . . 3  class  ( p  e.  { y  e. 
~P d  |  y 
~~  2o }  |->  ( z  e.  d  |->  if ( z  e.  p ,  U. ( p  \  { z } ) ,  z ) ) )
232, 3, 22cmpt 4093 . 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 1632 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 set class
This definition is referenced by:  pmtrfval  27496
  Copyright terms: Public domain W3C validator