Metamath Proof Explorer

Theorem rpnnen2lem2

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

Ref Expression
Hypothesis rpnnen2.1 ⊢F=x∈𝒫ℕ⟼n∈ℕ⟼ifn∈x13n0
Assertion rpnnen2lem2 ⊢A⊆ℕ→F⁡A:ℕ⟶ℝ

Proof

Step Hyp Ref Expression
1 rpnnen2.1 ⊢F=x∈𝒫ℕ⟼n∈ℕ⟼ifn∈x13n0
2 nnex ⊢ℕ∈V
3 2 elpw2 ⊢A∈𝒫ℕ↔A⊆ℕ
4 eleq2 ⊢x=A→n∈x↔n∈A
5 4 ifbid ⊢x=A→ifn∈x13n0=ifn∈A13n0
6 5 mpteq2dv ⊢x=A→n∈ℕ⟼ifn∈x13n0=n∈ℕ⟼ifn∈A13n0
7 2 mptex ⊢n∈ℕ⟼ifn∈A13n0∈V
8 6 1 7 fvmpt ⊢A∈𝒫ℕ→F⁡A=n∈ℕ⟼ifn∈A13n0
9 3 8 sylbir ⊢A⊆ℕ→F⁡A=n∈ℕ⟼ifn∈A13n0
10 1re ⊢1∈ℝ
11 3nn ⊢3∈ℕ
12 nndivre ⊢1∈ℝ∧3∈ℕ→13∈ℝ
13 10 11 12 mp2an ⊢13∈ℝ
14 nnnn0 ⊢n∈ℕ→n∈ℕ0
15 reexpcl ⊢13∈ℝ∧n∈ℕ0→13n∈ℝ
16 13 14 15 sylancr ⊢n∈ℕ→13n∈ℝ
17 0re ⊢0∈ℝ
18 ifcl ⊢13n∈ℝ∧0∈ℝ→ifn∈A13n0∈ℝ
19 16 17 18 sylancl ⊢n∈ℕ→ifn∈A13n0∈ℝ
20 19 adantl ⊢A⊆ℕ∧n∈ℕ→ifn∈A13n0∈ℝ
21 9 20 fmpt3d ⊢A⊆ℕ→F⁡A:ℕ⟶ℝ