Theorem rpnnen2lem1

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

	Ref	Expression
Hypothesis	rpnnen2.1	⊢ 𝐹 = ( 𝑥 ∈ 𝒫 ℕ ↦ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
Assertion	rpnnen2lem1	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑁 ) = if ( 𝑁 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑁 ) , 0 ) )

Proof

Step	Hyp	Ref	Expression
1		rpnnen2.1	⊢ 𝐹 = ( 𝑥 ∈ 𝒫 ℕ ↦ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
2		nnex	⊢ ℕ ∈ V
3	2	elpw2	⊢ ( 𝐴 ∈ 𝒫 ℕ ↔ 𝐴 ⊆ ℕ )
4		eleq2	⊢ ( 𝑥 = 𝐴 → ( 𝑛 ∈ 𝑥 ↔ 𝑛 ∈ 𝐴 ) )
5	4	ifbid	⊢ ( 𝑥 = 𝐴 → if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) = if ( 𝑛 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) )
6	5	mpteq2dv	⊢ ( 𝑥 = 𝐴 → ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
7	2	mptex	⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) ∈ V
8	6 1 7	fvmpt	⊢ ( 𝐴 ∈ 𝒫 ℕ → ( 𝐹 ‘ 𝐴 ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
9	3 8	sylbir	⊢ ( 𝐴 ⊆ ℕ → ( 𝐹 ‘ 𝐴 ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
10	9	fveq1d	⊢ ( 𝐴 ⊆ ℕ → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑁 ) = ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) ‘ 𝑁 ) )
11		eleq1	⊢ ( 𝑛 = 𝑁 → ( 𝑛 ∈ 𝐴 ↔ 𝑁 ∈ 𝐴 ) )
12		oveq2	⊢ ( 𝑛 = 𝑁 → ( ( 1 / 3 ) ↑ 𝑛 ) = ( ( 1 / 3 ) ↑ 𝑁 ) )
13	11 12	ifbieq1d	⊢ ( 𝑛 = 𝑁 → if ( 𝑛 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) = if ( 𝑁 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑁 ) , 0 ) )
14		eqid	⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) )
15		ovex	⊢ ( ( 1 / 3 ) ↑ 𝑁 ) ∈ V
16		c0ex	⊢ 0 ∈ V
17	15 16	ifex	⊢ if ( 𝑁 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑁 ) , 0 ) ∈ V
18	13 14 17	fvmpt	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) ‘ 𝑁 ) = if ( 𝑁 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑁 ) , 0 ) )
19	10 18	sylan9eq	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑁 ) = if ( 𝑁 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑁 ) , 0 ) )