Metamath Proof Explorer

Theorem rpnnen2lem1

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

Ref Expression
Hypothesis rpnnen2.1 ⊢ F = x ∈ 𝒫 ℕ ⟼ n ∈ ℕ ⟼ if n ∈ x 1 3 n 0
Assertion rpnnen2lem1 ⊢ A ⊆ ℕ ∧ N ∈ ℕ → F ⁡ A ⁡ N = if N ∈ A 1 3 N 0

Proof

Step Hyp Ref Expression
1 rpnnen2.1 ⊢ F = x ∈ 𝒫 ℕ ⟼ n ∈ ℕ ⟼ if n ∈ x 1 3 n 0
2 nnex ⊢ ℕ ∈ V
3 2 elpw2 ⊢ A ∈ 𝒫 ℕ ↔ A ⊆ ℕ
4 eleq2 ⊢ x = A → n ∈ x ↔ n ∈ A
5 4 ifbid ⊢ x = A → if n ∈ x 1 3 n 0 = if n ∈ A 1 3 n 0
6 5 mpteq2dv ⊢ x = A → n ∈ ℕ ⟼ if n ∈ x 1 3 n 0 = n ∈ ℕ ⟼ if n ∈ A 1 3 n 0
7 2 mptex ⊢ n ∈ ℕ ⟼ if n ∈ A 1 3 n 0 ∈ V
8 6 1 7 fvmpt ⊢ A ∈ 𝒫 ℕ → F ⁡ A = n ∈ ℕ ⟼ if n ∈ A 1 3 n 0
9 3 8 sylbir ⊢ A ⊆ ℕ → F ⁡ A = n ∈ ℕ ⟼ if n ∈ A 1 3 n 0
10 9 fveq1d ⊢ A ⊆ ℕ → F ⁡ A ⁡ N = n ∈ ℕ ⟼ if n ∈ A 1 3 n 0 ⁡ N
11 eleq1 ⊢ n = N → n ∈ A ↔ N ∈ A
12 oveq2 ⊢ n = N → 1 3 n = 1 3 N
13 11 12 ifbieq1d ⊢ n = N → if n ∈ A 1 3 n 0 = if N ∈ A 1 3 N 0
14 eqid ⊢ n ∈ ℕ ⟼ if n ∈ A 1 3 n 0 = n ∈ ℕ ⟼ if n ∈ A 1 3 n 0
15 ovex ⊢ 1 3 N ∈ V
16 c0ex ⊢ 0 ∈ V
17 15 16 ifex ⊢ if N ∈ A 1 3 N 0 ∈ V
18 13 14 17 fvmpt ⊢ N ∈ ℕ → n ∈ ℕ ⟼ if n ∈ A 1 3 n 0 ⁡ N = if N ∈ A 1 3 N 0
19 10 18 sylan9eq ⊢ A ⊆ ℕ ∧ N ∈ ℕ → F ⁡ A ⁡ N = if N ∈ A 1 3 N 0