Metamath Proof Explorer

Theorem cnndvlem2

Description: Lemma for cnndv . (Contributed by Asger C. Ipsen, 26-Aug-2021)

Ref Expression
Hypotheses cnndvlem2.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
cnndvlem2.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ 1 2 n ⁢ T ⁡ 2 ⋅ 3 n ⁢ y
cnndvlem2.w ⊢ W = w ∈ ℝ ⟼ ∑ i ∈ ℕ 0 F ⁡ w ⁡ i
Assertion cnndvlem2 ⊢ ∃ f f : ℝ ⟶cn ℝ ∧ dom ⁡ f ℝ ′ = ∅

Proof

Step Hyp Ref Expression
1 cnndvlem2.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
2 cnndvlem2.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ 1 2 n ⁢ T ⁡ 2 ⋅ 3 n ⁢ y
3 cnndvlem2.w ⊢ W = w ∈ ℝ ⟼ ∑ i ∈ ℕ 0 F ⁡ w ⁡ i
4 1 2 3 cnndvlem1 ⊢ W : ℝ ⟶cn ℝ ∧ dom ⁡ W ℝ ′ = ∅
5 reex ⊢ ℝ ∈ V
6 5 mptex ⊢ w ∈ ℝ ⟼ ∑ i ∈ ℕ 0 F ⁡ w ⁡ i ∈ V
7 3 6 eqeltri ⊢ W ∈ V
8 eleq1 ⊢ f = W → f : ℝ ⟶cn ℝ ↔ W : ℝ ⟶cn ℝ
9 oveq2 ⊢ f = W → ℝ D f = ℝ D W
10 9 dmeqd ⊢ f = W → dom ⁡ f ℝ ′ = dom ⁡ W ℝ ′
11 10 eqeq1d ⊢ f = W → dom ⁡ f ℝ ′ = ∅ ↔ dom ⁡ W ℝ ′ = ∅
12 8 11 anbi12d ⊢ f = W → f : ℝ ⟶cn ℝ ∧ dom ⁡ f ℝ ′ = ∅ ↔ W : ℝ ⟶cn ℝ ∧ dom ⁡ W ℝ ′ = ∅
13 7 12 spcev ⊢ W : ℝ ⟶cn ℝ ∧ dom ⁡ W ℝ ′ = ∅ → ∃ f f : ℝ ⟶cn ℝ ∧ dom ⁡ f ℝ ′ = ∅
14 4 13 ax-mp ⊢ ∃ f f : ℝ ⟶cn ℝ ∧ dom ⁡ f ℝ ′ = ∅