This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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