Step |
Hyp |
Ref |
Expression |
1 |
|
elex |
|- ( W e. X -> W e. _V ) |
2 |
|
fvex |
|- ( W ` ( ( # ` W ) - 1 ) ) e. _V |
3 |
|
id |
|- ( w = W -> w = W ) |
4 |
|
fveq2 |
|- ( w = W -> ( # ` w ) = ( # ` W ) ) |
5 |
4
|
oveq1d |
|- ( w = W -> ( ( # ` w ) - 1 ) = ( ( # ` W ) - 1 ) ) |
6 |
3 5
|
fveq12d |
|- ( w = W -> ( w ` ( ( # ` w ) - 1 ) ) = ( W ` ( ( # ` W ) - 1 ) ) ) |
7 |
|
df-lsw |
|- lastS = ( w e. _V |-> ( w ` ( ( # ` w ) - 1 ) ) ) |
8 |
6 7
|
fvmptg |
|- ( ( W e. _V /\ ( W ` ( ( # ` W ) - 1 ) ) e. _V ) -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) ) |
9 |
1 2 8
|
sylancl |
|- ( W e. X -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) ) |