Metamath Proof Explorer

Theorem pmtrfval

Description: The function generating transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015)

Ref Expression
Hypothesis pmtrfval.t 
|- T = ( pmTrsp ` D )
Assertion pmtrfval 
|- ( D e. V -> T = ( p e. { y e. ~P D | y ~~ 2o } |-> ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) )

Proof

Step Hyp Ref Expression
1 pmtrfval.t 
 |-  T = ( pmTrsp ` D )
2 elex 
 |-  ( D e. V -> D e. _V )
3 pweq 
 |-  ( d = D -> ~P d = ~P D )
4 3 rabeqdv 
 |-  ( d = D -> { y e. ~P d | y ~~ 2o } = { y e. ~P D | y ~~ 2o } )
5 mpteq1 
 |-  ( d = D -> ( z e. d |-> if ( z e. p , U. ( p \ { z } ) , z ) ) = ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) )
6 4 5 mpteq12dv 
 |-  ( d = D -> ( p e. { y e. ~P d | y ~~ 2o } |-> ( z e. d |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) = ( p e. { y e. ~P D | y ~~ 2o } |-> ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) )
7 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 ) ) ) )
8 vpwex 
 |-  ~P d e. _V
9 8 mptrabex 
 |-  ( p e. { y e. ~P d | y ~~ 2o } |-> ( z e. d |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) e. _V
10 6 7 9 fvmpt3i 
 |-  ( D e. _V -> ( pmTrsp ` D ) = ( p e. { y e. ~P D | y ~~ 2o } |-> ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) )
11 2 10 syl 
 |-  ( D e. V -> ( pmTrsp ` D ) = ( p e. { y e. ~P D | y ~~ 2o } |-> ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) )
12 1 11 syl5eq 
 |-  ( D e. V -> T = ( p e. { y e. ~P D | y ~~ 2o } |-> ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) )