| Step |
Hyp |
Ref |
Expression |
| 1 |
|
rpnnen2.1 |
|- F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) ) |
| 2 |
|
nnex |
|- NN e. _V |
| 3 |
2
|
elpw2 |
|- ( A e. ~P NN <-> A C_ NN ) |
| 4 |
|
eleq2 |
|- ( x = A -> ( n e. x <-> n e. A ) ) |
| 5 |
4
|
ifbid |
|- ( x = A -> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) = if ( n e. A , ( ( 1 / 3 ) ^ n ) , 0 ) ) |
| 6 |
5
|
mpteq2dv |
|- ( x = A -> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) = ( n e. NN |-> if ( n e. A , ( ( 1 / 3 ) ^ n ) , 0 ) ) ) |
| 7 |
2
|
mptex |
|- ( n e. NN |-> if ( n e. A , ( ( 1 / 3 ) ^ n ) , 0 ) ) e. _V |
| 8 |
6 1 7
|
fvmpt |
|- ( A e. ~P NN -> ( F ` A ) = ( n e. NN |-> if ( n e. A , ( ( 1 / 3 ) ^ n ) , 0 ) ) ) |
| 9 |
3 8
|
sylbir |
|- ( A C_ NN -> ( F ` A ) = ( n e. NN |-> if ( n e. A , ( ( 1 / 3 ) ^ n ) , 0 ) ) ) |
| 10 |
9
|
fveq1d |
|- ( A C_ NN -> ( ( F ` A ) ` N ) = ( ( n e. NN |-> if ( n e. A , ( ( 1 / 3 ) ^ n ) , 0 ) ) ` N ) ) |
| 11 |
|
eleq1 |
|- ( n = N -> ( n e. A <-> N e. A ) ) |
| 12 |
|
oveq2 |
|- ( n = N -> ( ( 1 / 3 ) ^ n ) = ( ( 1 / 3 ) ^ N ) ) |
| 13 |
11 12
|
ifbieq1d |
|- ( n = N -> if ( n e. A , ( ( 1 / 3 ) ^ n ) , 0 ) = if ( N e. A , ( ( 1 / 3 ) ^ N ) , 0 ) ) |
| 14 |
|
eqid |
|- ( n e. NN |-> if ( n e. A , ( ( 1 / 3 ) ^ n ) , 0 ) ) = ( n e. NN |-> if ( n e. A , ( ( 1 / 3 ) ^ n ) , 0 ) ) |
| 15 |
|
ovex |
|- ( ( 1 / 3 ) ^ N ) e. _V |
| 16 |
|
c0ex |
|- 0 e. _V |
| 17 |
15 16
|
ifex |
|- if ( N e. A , ( ( 1 / 3 ) ^ N ) , 0 ) e. _V |
| 18 |
13 14 17
|
fvmpt |
|- ( N e. NN -> ( ( n e. NN |-> if ( n e. A , ( ( 1 / 3 ) ^ n ) , 0 ) ) ` N ) = if ( N e. A , ( ( 1 / 3 ) ^ N ) , 0 ) ) |
| 19 |
10 18
|
sylan9eq |
|- ( ( A C_ NN /\ N e. NN ) -> ( ( F ` A ) ` N ) = if ( N e. A , ( ( 1 / 3 ) ^ N ) , 0 ) ) |