Theorem ddeval0

Description: Value of the delta measure. (Contributed by Thierry Arnoux, 14-Sep-2018)

	Ref	Expression
Assertion	ddeval0	$$⊢\left(A\subseteq ℝ\wedge \neg 0\in A\right)\to \delta \left(A\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		reex	$$⊢ℝ\in \mathrm{V}$$
2	1	ssex	$$⊢A\subseteq ℝ\to A\in \mathrm{V}$$
3		elpwg	$$⊢A\in \mathrm{V}\to \left(A\in 𝒫ℝ\leftrightarrow A\subseteq ℝ\right)$$
4	3	biimpar	$$⊢\left(A\in \mathrm{V}\wedge A\subseteq ℝ\right)\to A\in 𝒫ℝ$$
5	2 4	mpancom	$$⊢A\subseteq ℝ\to A\in 𝒫ℝ$$
6		eleq2	$$⊢a=A\to \left(0\in a\leftrightarrow 0\in A\right)$$
7	6	ifbid	$$⊢a=A\to if\left(0\in a,1,0\right)=if\left(0\in A,1,0\right)$$
8		df-dde	$$⊢\delta =\left(a\in 𝒫ℝ⟼if\left(0\in a,1,0\right)\right)$$
9		1ex	$$⊢1\in \mathrm{V}$$
10		c0ex	$$⊢0\in \mathrm{V}$$
11	9 10	ifex	$$⊢if\left(0\in A,1,0\right)\in \mathrm{V}$$
12	7 8 11	fvmpt	$$⊢A\in 𝒫ℝ\to \delta \left(A\right)=if\left(0\in A,1,0\right)$$
13	5 12	syl	$$⊢A\subseteq ℝ\to \delta \left(A\right)=if\left(0\in A,1,0\right)$$
14		iffalse	$$⊢\neg 0\in A\to if\left(0\in A,1,0\right)=0$$
15	13 14	sylan9eq	$$⊢\left(A\subseteq ℝ\wedge \neg 0\in A\right)\to \delta \left(A\right)=0$$