Theorem ddeval1

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

	Ref	Expression
Assertion	ddeval1	⊢ ( ( 𝐴 ⊆ ℝ ∧ 0 ∈ 𝐴 ) → ( δ ‘ 𝐴 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		reex	⊢ ℝ ∈ V
2	1	ssex	⊢ ( 𝐴 ⊆ ℝ → 𝐴 ∈ V )
3		elpwg	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ 𝒫 ℝ ↔ 𝐴 ⊆ ℝ ) )
4	3	biimpar	⊢ ( ( 𝐴 ∈ V ∧ 𝐴 ⊆ ℝ ) → 𝐴 ∈ 𝒫 ℝ )
5	2 4	mpancom	⊢ ( 𝐴 ⊆ ℝ → 𝐴 ∈ 𝒫 ℝ )
6		eleq2	⊢ ( 𝑎 = 𝐴 → ( 0 ∈ 𝑎 ↔ 0 ∈ 𝐴 ) )
7	6	ifbid	⊢ ( 𝑎 = 𝐴 → if ( 0 ∈ 𝑎 , 1 , 0 ) = if ( 0 ∈ 𝐴 , 1 , 0 ) )
8		df-dde	⊢ δ = ( 𝑎 ∈ 𝒫 ℝ ↦ if ( 0 ∈ 𝑎 , 1 , 0 ) )
9		1ex	⊢ 1 ∈ V
10		c0ex	⊢ 0 ∈ V
11	9 10	ifex	⊢ if ( 0 ∈ 𝐴 , 1 , 0 ) ∈ V
12	7 8 11	fvmpt	⊢ ( 𝐴 ∈ 𝒫 ℝ → ( δ ‘ 𝐴 ) = if ( 0 ∈ 𝐴 , 1 , 0 ) )
13	5 12	syl	⊢ ( 𝐴 ⊆ ℝ → ( δ ‘ 𝐴 ) = if ( 0 ∈ 𝐴 , 1 , 0 ) )
14		iftrue	⊢ ( 0 ∈ 𝐴 → if ( 0 ∈ 𝐴 , 1 , 0 ) = 1 )
15	13 14	sylan9eq	⊢ ( ( 𝐴 ⊆ ℝ ∧ 0 ∈ 𝐴 ) → ( δ ‘ 𝐴 ) = 1 )