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 ) ) ) )