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