cnndvlem2

	Ref	Expression
Hypotheses	cnndvlem2.t	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
	cnndvlem2.f	$⊢ F = (y \in ℝ ⟼ (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n} T ({2 \cdot 3}^{n} y)))$
	cnndvlem2.w	$⊢ W = (w \in ℝ ⟼ \sum_{i \in ℕ_{0}} F (w) (i))$
Assertion	cnndvlem2	$⊢ \exists f (f : ℝ \underset{cn}{⟶} ℝ \land dom f_{ℝ}^{'} = \emptyset)$

Step	Hyp	Ref	Expression
1		cnndvlem2.t	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
2		cnndvlem2.f	$⊢ F = (y \in ℝ ⟼ (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n} T ({2 \cdot 3}^{n} y)))$
3		cnndvlem2.w	$⊢ W = (w \in ℝ ⟼ \sum_{i \in ℕ_{0}} F (w) (i))$
4	1 2 3	cnndvlem1	$⊢ (W : ℝ \underset{cn}{⟶} ℝ \land dom W_{ℝ}^{'} = \emptyset)$
5		reex	$⊢ ℝ \in V$
6	5	mptex	$⊢ (w \in ℝ ⟼ \sum_{i \in ℕ_{0}} F (w) (i)) \in V$
7	3 6	eqeltri	$⊢ W \in V$
8		eleq1	$⊢ f = W \to (f : ℝ \underset{cn}{⟶} ℝ \leftrightarrow W : ℝ \underset{cn}{⟶} ℝ)$
9		oveq2	$⊢ f = W \to ℝ D f = ℝ D W$
10	9	dmeqd	$⊢ f = W \to dom f_{ℝ}^{'} = dom W_{ℝ}^{'}$
11	10	eqeq1d	$⊢ f = W \to (dom f_{ℝ}^{'} = \emptyset \leftrightarrow dom W_{ℝ}^{'} = \emptyset)$
12	8 11	anbi12d	$⊢ f = W \to ((f : ℝ \underset{cn}{⟶} ℝ \land dom f_{ℝ}^{'} = \emptyset) \leftrightarrow (W : ℝ \underset{cn}{⟶} ℝ \land dom W_{ℝ}^{'} = \emptyset))$
13	7 12	spcev	$⊢ (W : ℝ \underset{cn}{⟶} ℝ \land dom W_{ℝ}^{'} = \emptyset) \to \exists f (f : ℝ \underset{cn}{⟶} ℝ \land dom f_{ℝ}^{'} = \emptyset)$
14	4 13	ax-mp	$⊢ \exists f (f : ℝ \underset{cn}{⟶} ℝ \land dom f_{ℝ}^{'} = \emptyset)$

Metamath Proof Explorer