Step |
Hyp |
Ref |
Expression |
1 |
|
dssmapfvd.o |
|- O = ( b e. _V |-> ( f e. ( ~P b ^m ~P b ) |-> ( s e. ~P b |-> ( b \ ( f ` ( b \ s ) ) ) ) ) ) |
2 |
|
dssmapfvd.d |
|- D = ( O ` B ) |
3 |
|
dssmapfvd.b |
|- ( ph -> B e. V ) |
4 |
|
dssmapfv2d.f |
|- ( ph -> F e. ( ~P B ^m ~P B ) ) |
5 |
|
dssmapfv2d.g |
|- G = ( D ` F ) |
6 |
|
dssmapfv3d.s |
|- ( ph -> S e. ~P B ) |
7 |
|
dssmapfv3d.t |
|- T = ( G ` S ) |
8 |
1 2 3 4 5
|
dssmapfv2d |
|- ( ph -> G = ( s e. ~P B |-> ( B \ ( F ` ( B \ s ) ) ) ) ) |
9 |
|
difeq2 |
|- ( s = S -> ( B \ s ) = ( B \ S ) ) |
10 |
9
|
fveq2d |
|- ( s = S -> ( F ` ( B \ s ) ) = ( F ` ( B \ S ) ) ) |
11 |
10
|
difeq2d |
|- ( s = S -> ( B \ ( F ` ( B \ s ) ) ) = ( B \ ( F ` ( B \ S ) ) ) ) |
12 |
11
|
adantl |
|- ( ( ph /\ s = S ) -> ( B \ ( F ` ( B \ s ) ) ) = ( B \ ( F ` ( B \ S ) ) ) ) |
13 |
|
difexg |
|- ( B e. V -> ( B \ ( F ` ( B \ S ) ) ) e. _V ) |
14 |
3 13
|
syl |
|- ( ph -> ( B \ ( F ` ( B \ S ) ) ) e. _V ) |
15 |
8 12 6 14
|
fvmptd |
|- ( ph -> ( G ` S ) = ( B \ ( F ` ( B \ S ) ) ) ) |
16 |
7 15
|
syl5eq |
|- ( ph -> T = ( B \ ( F ` ( B \ S ) ) ) ) |