Metamath Proof Explorer


Theorem ddeval0

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

Ref Expression
Assertion ddeval0 ( ( 𝐴 ⊆ ℝ ∧ ¬ 0 ∈ 𝐴 ) → ( δ ‘ 𝐴 ) = 0 )

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 iffalse ( ¬ 0 ∈ 𝐴 → if ( 0 ∈ 𝐴 , 1 , 0 ) = 0 )
15 13 14 sylan9eq ( ( 𝐴 ⊆ ℝ ∧ ¬ 0 ∈ 𝐴 ) → ( δ ‘ 𝐴 ) = 0 )