Metamath Proof Explorer

Theorem rpnnen2lem1

Description: Lemma for rpnnen2 . (Contributed by Mario Carneiro, 13-May-2013)

Ref Expression
Hypothesis rpnnen2.1 
|- F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )
Assertion rpnnen2lem1 
|- ( ( A C_ NN /\ N e. NN ) -> ( ( F ` A ) ` N ) = if ( N e. A , ( ( 1 / 3 ) ^ N ) , 0 ) )

Proof

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