Metamath Proof Explorer

Theorem ddemeas

Description: The Dirac delta measure is a measure. (Contributed by Thierry Arnoux, 14-Sep-2018)

Ref Expression
Assertion ddemeas δ ∈ ( measures ‘ 𝒫 ℝ )

Proof

Step Hyp Ref Expression
1 1xr ⊢ 1 ∈ ℝ*
2 0le1 ⊢ 0 ≤ 1
3 pnfge ⊢ ( 1 ∈ ℝ* → 1 ≤ +∞ )
4 1 3 ax-mp ⊢ 1 ≤ +∞
5 0xr ⊢ 0 ∈ ℝ*
6 pnfxr ⊢ +∞ ∈ ℝ*
7 elicc1 ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 1 ∈ ( 0 [,] +∞ ) ↔ ( 1 ∈ ℝ* ∧ 0 ≤ 1 ∧ 1 ≤ +∞ ) ) )
8 5 6 7 mp2an ⊢ ( 1 ∈ ( 0 [,] +∞ ) ↔ ( 1 ∈ ℝ* ∧ 0 ≤ 1 ∧ 1 ≤ +∞ ) )
9 1 2 4 8 mpbir3an ⊢ 1 ∈ ( 0 [,] +∞ )
10 0e0iccpnf ⊢ 0 ∈ ( 0 [,] +∞ )
11 9 10 ifcli ⊢ if ( 0 ∈ 𝑎 , 1 , 0 ) ∈ ( 0 [,] +∞ )
12 11 rgenw ⊢ ∀ 𝑎 ∈ 𝒫 ℝ if ( 0 ∈ 𝑎 , 1 , 0 ) ∈ ( 0 [,] +∞ )
13 df-dde ⊢ δ = ( 𝑎 ∈ 𝒫 ℝ ↦ if ( 0 ∈ 𝑎 , 1 , 0 ) )
14 13 fmpt ⊢ ( ∀ 𝑎 ∈ 𝒫 ℝ if ( 0 ∈ 𝑎 , 1 , 0 ) ∈ ( 0 [,] +∞ ) ↔ δ : 𝒫 ℝ ⟶ ( 0 [,] +∞ ) )
15 12 14 mpbi ⊢ δ : 𝒫 ℝ ⟶ ( 0 [,] +∞ )
16 0ss ⊢ ∅ ⊆ ℝ
17 noel ⊢ ¬ 0 ∈ ∅
18 ddeval0 ⊢ ( ( ∅ ⊆ ℝ ∧ ¬ 0 ∈ ∅ ) → ( δ ‘ ∅ ) = 0 )
19 16 17 18 mp2an ⊢ ( δ ‘ ∅ ) = 0
20 rabxm ⊢ 𝑥 = ( { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ∪ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } )
21 esumeq1 ⊢ ( 𝑥 = ( { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ∪ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ) → Σ* 𝑦 ∈ 𝑥 ( δ ‘ 𝑦 ) = Σ* 𝑦 ∈ ( { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ∪ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ) ( δ ‘ 𝑦 ) )
22 20 21 ax-mp ⊢ Σ* 𝑦 ∈ 𝑥 ( δ ‘ 𝑦 ) = Σ* 𝑦 ∈ ( { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ∪ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ) ( δ ‘ 𝑦 )
23 nfv ⊢ Ⅎ 𝑦 𝑥 ∈ 𝒫 𝒫 ℝ
24 nfcv ⊢ Ⅎ 𝑦 { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 }
25 nfcv ⊢ Ⅎ 𝑦 { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 }
26 rabexg ⊢ ( 𝑥 ∈ 𝒫 𝒫 ℝ → { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ∈ V )
27 rabexg ⊢ ( 𝑥 ∈ 𝒫 𝒫 ℝ → { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ∈ V )
28 rabnc ⊢ ( { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ∩ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ) = ∅
29 28 a1i ⊢ ( 𝑥 ∈ 𝒫 𝒫 ℝ → ( { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ∩ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ) = ∅ )
30 elrabi ⊢ ( 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } → 𝑦 ∈ 𝑥 )
31 30 adantl ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ) → 𝑦 ∈ 𝑥 )
32 simpl ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ) → 𝑥 ∈ 𝒫 𝒫 ℝ )
33 elelpwi ⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 𝒫 ℝ ) → 𝑦 ∈ 𝒫 ℝ )
34 31 32 33 syl2anc ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ) → 𝑦 ∈ 𝒫 ℝ )
35 15 ffvelcdmi ⊢ ( 𝑦 ∈ 𝒫 ℝ → ( δ ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
36 34 35 syl ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ) → ( δ ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
37 elrabi ⊢ ( 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } → 𝑦 ∈ 𝑥 )
38 37 adantl ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ) → 𝑦 ∈ 𝑥 )
39 simpl ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ) → 𝑥 ∈ 𝒫 𝒫 ℝ )
40 38 39 33 syl2anc ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ) → 𝑦 ∈ 𝒫 ℝ )
41 40 35 syl ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ) → ( δ ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
42 23 24 25 26 27 29 36 41 esumsplit ⊢ ( 𝑥 ∈ 𝒫 𝒫 ℝ → Σ* 𝑦 ∈ ( { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ∪ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ) ( δ ‘ 𝑦 ) = ( Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ( δ ‘ 𝑦 ) +𝑒 Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ( δ ‘ 𝑦 ) ) )
43 22 42 eqtrid ⊢ ( 𝑥 ∈ 𝒫 𝒫 ℝ → Σ* 𝑦 ∈ 𝑥 ( δ ‘ 𝑦 ) = ( Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ( δ ‘ 𝑦 ) +𝑒 Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ( δ ‘ 𝑦 ) ) )
44 43 adantr ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → Σ* 𝑦 ∈ 𝑥 ( δ ‘ 𝑦 ) = ( Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ( δ ‘ 𝑦 ) +𝑒 Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ( δ ‘ 𝑦 ) ) )
45 esumeq1 ⊢ ( { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = { 𝑘 } → Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ( δ ‘ 𝑦 ) = Σ* 𝑦 ∈ { 𝑘 } ( δ ‘ 𝑦 ) )
46 45 adantl ⊢ ( ( ( ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 ) ∧ 𝑘 ∈ 𝑥 ) ∧ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = { 𝑘 } ) → Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ( δ ‘ 𝑦 ) = Σ* 𝑦 ∈ { 𝑘 } ( δ ‘ 𝑦 ) )
47 simp-4l ⊢ ( ( ( ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 ) ∧ 𝑘 ∈ 𝑥 ) ∧ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = { 𝑘 } ) → 𝑥 ∈ 𝒫 𝒫 ℝ )
48 vex ⊢ 𝑘 ∈ V
49 48 rabsnel ⊢ ( { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = { 𝑘 } → 𝑘 ∈ 𝑥 )
50 49 adantl ⊢ ( ( ( ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 ) ∧ 𝑘 ∈ 𝑥 ) ∧ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = { 𝑘 } ) → 𝑘 ∈ 𝑥 )
51 eleq2w ⊢ ( 𝑎 = 𝑘 → ( 0 ∈ 𝑎 ↔ 0 ∈ 𝑘 ) )
52 48 51 rabsnt ⊢ ( { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = { 𝑘 } → 0 ∈ 𝑘 )
53 52 adantl ⊢ ( ( ( ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 ) ∧ 𝑘 ∈ 𝑥 ) ∧ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = { 𝑘 } ) → 0 ∈ 𝑘 )
54 elelpwi ⊢ ( ( 𝑘 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 𝒫 ℝ ) → 𝑘 ∈ 𝒫 ℝ )
55 54 ancoms ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑘 ∈ 𝑥 ) → 𝑘 ∈ 𝒫 ℝ )
56 55 adantrr ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ ( 𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘 ) ) → 𝑘 ∈ 𝒫 ℝ )
57 simpr ⊢ ( ( 𝑘 ∈ 𝒫 ℝ ∧ 𝑦 = 𝑘 ) → 𝑦 = 𝑘 )
58 57 fveq2d ⊢ ( ( 𝑘 ∈ 𝒫 ℝ ∧ 𝑦 = 𝑘 ) → ( δ ‘ 𝑦 ) = ( δ ‘ 𝑘 ) )
59 48 a1i ⊢ ( 𝑘 ∈ 𝒫 ℝ → 𝑘 ∈ V )
60 15 ffvelcdmi ⊢ ( 𝑘 ∈ 𝒫 ℝ → ( δ ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) )
61 58 59 60 esumsn ⊢ ( 𝑘 ∈ 𝒫 ℝ → Σ* 𝑦 ∈ { 𝑘 } ( δ ‘ 𝑦 ) = ( δ ‘ 𝑘 ) )
62 56 61 syl ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ ( 𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘 ) ) → Σ* 𝑦 ∈ { 𝑘 } ( δ ‘ 𝑦 ) = ( δ ‘ 𝑘 ) )
63 56 elpwid ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ ( 𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘 ) ) → 𝑘 ⊆ ℝ )
64 simprr ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ ( 𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘 ) ) → 0 ∈ 𝑘 )
65 ddeval1 ⊢ ( ( 𝑘 ⊆ ℝ ∧ 0 ∈ 𝑘 ) → ( δ ‘ 𝑘 ) = 1 )
66 63 64 65 syl2anc ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ ( 𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘 ) ) → ( δ ‘ 𝑘 ) = 1 )
67 62 66 eqtrd ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ ( 𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘 ) ) → Σ* 𝑦 ∈ { 𝑘 } ( δ ‘ 𝑦 ) = 1 )
68 47 50 53 67 syl12anc ⊢ ( ( ( ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 ) ∧ 𝑘 ∈ 𝑥 ) ∧ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = { 𝑘 } ) → Σ* 𝑦 ∈ { 𝑘 } ( δ ‘ 𝑦 ) = 1 )
69 46 68 eqtrd ⊢ ( ( ( ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 ) ∧ 𝑘 ∈ 𝑥 ) ∧ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = { 𝑘 } ) → Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ( δ ‘ 𝑦 ) = 1 )
70 df-disj ⊢ ( Disj 𝑦 ∈ 𝑥 𝑦 ↔ ∀ 𝑘 ∃* 𝑦 ∈ 𝑥 𝑘 ∈ 𝑦 )
71 c0ex ⊢ 0 ∈ V
72 eleq1 ⊢ ( 𝑘 = 0 → ( 𝑘 ∈ 𝑦 ↔ 0 ∈ 𝑦 ) )
73 72 rmobidv ⊢ ( 𝑘 = 0 → ( ∃* 𝑦 ∈ 𝑥 𝑘 ∈ 𝑦 ↔ ∃* 𝑦 ∈ 𝑥 0 ∈ 𝑦 ) )
74 71 73 spcv ⊢ ( ∀ 𝑘 ∃* 𝑦 ∈ 𝑥 𝑘 ∈ 𝑦 → ∃* 𝑦 ∈ 𝑥 0 ∈ 𝑦 )
75 70 74 sylbi ⊢ ( Disj 𝑦 ∈ 𝑥 𝑦 → ∃* 𝑦 ∈ 𝑥 0 ∈ 𝑦 )
76 rmo5 ⊢ ( ∃* 𝑦 ∈ 𝑥 0 ∈ 𝑦 ↔ ( ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 → ∃! 𝑦 ∈ 𝑥 0 ∈ 𝑦 ) )
77 76 biimpi ⊢ ( ∃* 𝑦 ∈ 𝑥 0 ∈ 𝑦 → ( ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 → ∃! 𝑦 ∈ 𝑥 0 ∈ 𝑦 ) )
78 77 imp ⊢ ( ( ∃* 𝑦 ∈ 𝑥 0 ∈ 𝑦 ∧ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 ) → ∃! 𝑦 ∈ 𝑥 0 ∈ 𝑦 )
79 75 78 sylan ⊢ ( ( Disj 𝑦 ∈ 𝑥 𝑦 ∧ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 ) → ∃! 𝑦 ∈ 𝑥 0 ∈ 𝑦 )
80 reusn ⊢ ( ∃! 𝑦 ∈ 𝑥 0 ∈ 𝑦 ↔ ∃ 𝑘 { 𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦 } = { 𝑘 } )
81 79 80 sylib ⊢ ( ( Disj 𝑦 ∈ 𝑥 𝑦 ∧ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 ) → ∃ 𝑘 { 𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦 } = { 𝑘 } )
82 eleq2w ⊢ ( 𝑎 = 𝑦 → ( 0 ∈ 𝑎 ↔ 0 ∈ 𝑦 ) )
83 82 cbvrabv ⊢ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = { 𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦 }
84 83 eqeq1i ⊢ ( { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = { 𝑘 } ↔ { 𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦 } = { 𝑘 } )
85 49 ancri ⊢ ( { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = { 𝑘 } → ( 𝑘 ∈ 𝑥 ∧ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = { 𝑘 } ) )
86 84 85 sylbir ⊢ ( { 𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦 } = { 𝑘 } → ( 𝑘 ∈ 𝑥 ∧ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = { 𝑘 } ) )
87 86 eximi ⊢ ( ∃ 𝑘 { 𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦 } = { 𝑘 } → ∃ 𝑘 ( 𝑘 ∈ 𝑥 ∧ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = { 𝑘 } ) )
88 df-rex ⊢ ( ∃ 𝑘 ∈ 𝑥 { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = { 𝑘 } ↔ ∃ 𝑘 ( 𝑘 ∈ 𝑥 ∧ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = { 𝑘 } ) )
89 87 88 sylibr ⊢ ( ∃ 𝑘 { 𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦 } = { 𝑘 } → ∃ 𝑘 ∈ 𝑥 { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = { 𝑘 } )
90 81 89 syl ⊢ ( ( Disj 𝑦 ∈ 𝑥 𝑦 ∧ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 ) → ∃ 𝑘 ∈ 𝑥 { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = { 𝑘 } )
91 90 adantll ⊢ ( ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 ) → ∃ 𝑘 ∈ 𝑥 { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = { 𝑘 } )
92 69 91 r19.29a ⊢ ( ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 ) → Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ( δ ‘ 𝑦 ) = 1 )
93 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝒫 ℝ → 𝑥 ⊆ 𝒫 ℝ )
94 sspwuni ⊢ ( 𝑥 ⊆ 𝒫 ℝ ↔ ∪ 𝑥 ⊆ ℝ )
95 93 94 sylib ⊢ ( 𝑥 ∈ 𝒫 𝒫 ℝ → ∪ 𝑥 ⊆ ℝ )
96 eluni2 ⊢ ( 0 ∈ ∪ 𝑥 ↔ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 )
97 96 biimpri ⊢ ( ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 → 0 ∈ ∪ 𝑥 )
98 ddeval1 ⊢ ( ( ∪ 𝑥 ⊆ ℝ ∧ 0 ∈ ∪ 𝑥 ) → ( δ ‘ ∪ 𝑥 ) = 1 )
99 95 97 98 syl2an ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 ) → ( δ ‘ ∪ 𝑥 ) = 1 )
100 99 adantlr ⊢ ( ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 ) → ( δ ‘ ∪ 𝑥 ) = 1 )
101 92 100 eqtr4d ⊢ ( ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 ) → Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ( δ ‘ 𝑦 ) = ( δ ‘ ∪ 𝑥 ) )
102 nfre1 ⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦
103 102 nfn ⊢ Ⅎ 𝑦 ¬ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦
104 82 elrab ⊢ ( 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ↔ ( 𝑦 ∈ 𝑥 ∧ 0 ∈ 𝑦 ) )
105 104 exbii ⊢ ( ∃ 𝑦 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ 0 ∈ 𝑦 ) )
106 neq0 ⊢ ( ¬ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = ∅ ↔ ∃ 𝑦 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } )
107 df-rex ⊢ ( ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ 0 ∈ 𝑦 ) )
108 105 106 107 3bitr4i ⊢ ( ¬ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = ∅ ↔ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 )
109 108 biimpi ⊢ ( ¬ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = ∅ → ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 )
110 109 con1i ⊢ ( ¬ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 → { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } = ∅ )
111 103 110 esumeq1d ⊢ ( ¬ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 → Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ( δ ‘ 𝑦 ) = Σ* 𝑦 ∈ ∅ ( δ ‘ 𝑦 ) )
112 esumnul ⊢ Σ* 𝑦 ∈ ∅ ( δ ‘ 𝑦 ) = 0
113 111 112 eqtrdi ⊢ ( ¬ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 → Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ( δ ‘ 𝑦 ) = 0 )
114 113 adantl ⊢ ( ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ ¬ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 ) → Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ( δ ‘ 𝑦 ) = 0 )
115 96 biimpi ⊢ ( 0 ∈ ∪ 𝑥 → ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 )
116 115 con3i ⊢ ( ¬ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 → ¬ 0 ∈ ∪ 𝑥 )
117 ddeval0 ⊢ ( ( ∪ 𝑥 ⊆ ℝ ∧ ¬ 0 ∈ ∪ 𝑥 ) → ( δ ‘ ∪ 𝑥 ) = 0 )
118 95 116 117 syl2an ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ ¬ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 ) → ( δ ‘ ∪ 𝑥 ) = 0 )
119 118 adantlr ⊢ ( ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ ¬ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 ) → ( δ ‘ ∪ 𝑥 ) = 0 )
120 114 119 eqtr4d ⊢ ( ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ∧ ¬ ∃ 𝑦 ∈ 𝑥 0 ∈ 𝑦 ) → Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ( δ ‘ 𝑦 ) = ( δ ‘ ∪ 𝑥 ) )
121 101 120 pm2.61dan ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ( δ ‘ 𝑦 ) = ( δ ‘ ∪ 𝑥 ) )
122 40 elpwid ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ) → 𝑦 ⊆ ℝ )
123 82 notbid ⊢ ( 𝑎 = 𝑦 → ( ¬ 0 ∈ 𝑎 ↔ ¬ 0 ∈ 𝑦 ) )
124 123 elrab ⊢ ( 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ↔ ( 𝑦 ∈ 𝑥 ∧ ¬ 0 ∈ 𝑦 ) )
125 124 simprbi ⊢ ( 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } → ¬ 0 ∈ 𝑦 )
126 125 adantl ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ) → ¬ 0 ∈ 𝑦 )
127 ddeval0 ⊢ ( ( 𝑦 ⊆ ℝ ∧ ¬ 0 ∈ 𝑦 ) → ( δ ‘ 𝑦 ) = 0 )
128 122 126 127 syl2anc ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ) → ( δ ‘ 𝑦 ) = 0 )
129 128 esumeq2dv ⊢ ( 𝑥 ∈ 𝒫 𝒫 ℝ → Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ( δ ‘ 𝑦 ) = Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } 0 )
130 vex ⊢ 𝑥 ∈ V
131 130 rabex ⊢ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ∈ V
132 25 esum0 ⊢ ( { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ∈ V → Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } 0 = 0 )
133 131 132 ax-mp ⊢ Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } 0 = 0
134 129 133 eqtrdi ⊢ ( 𝑥 ∈ 𝒫 𝒫 ℝ → Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ( δ ‘ 𝑦 ) = 0 )
135 134 adantr ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ( δ ‘ 𝑦 ) = 0 )
136 121 135 oveq12d ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎 } ( δ ‘ 𝑦 ) +𝑒 Σ* 𝑦 ∈ { 𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎 } ( δ ‘ 𝑦 ) ) = ( ( δ ‘ ∪ 𝑥 ) +𝑒 0 ) )
137 vuniex ⊢ ∪ 𝑥 ∈ V
138 137 elpw ⊢ ( ∪ 𝑥 ∈ 𝒫 ℝ ↔ ∪ 𝑥 ⊆ ℝ )
139 138 biimpri ⊢ ( ∪ 𝑥 ⊆ ℝ → ∪ 𝑥 ∈ 𝒫 ℝ )
140 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
141 15 ffvelcdmi ⊢ ( ∪ 𝑥 ∈ 𝒫 ℝ → ( δ ‘ ∪ 𝑥 ) ∈ ( 0 [,] +∞ ) )
142 140 141 sselid ⊢ ( ∪ 𝑥 ∈ 𝒫 ℝ → ( δ ‘ ∪ 𝑥 ) ∈ ℝ* )
143 xaddrid ⊢ ( ( δ ‘ ∪ 𝑥 ) ∈ ℝ* → ( ( δ ‘ ∪ 𝑥 ) +𝑒 0 ) = ( δ ‘ ∪ 𝑥 ) )
144 95 139 142 143 4syl ⊢ ( 𝑥 ∈ 𝒫 𝒫 ℝ → ( ( δ ‘ ∪ 𝑥 ) +𝑒 0 ) = ( δ ‘ ∪ 𝑥 ) )
145 144 adantr ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( ( δ ‘ ∪ 𝑥 ) +𝑒 0 ) = ( δ ‘ ∪ 𝑥 ) )
146 44 136 145 3eqtrrd ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( δ ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( δ ‘ 𝑦 ) )
147 146 adantrl ⊢ ( ( 𝑥 ∈ 𝒫 𝒫 ℝ ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( δ ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( δ ‘ 𝑦 ) )
148 147 ex ⊢ ( 𝑥 ∈ 𝒫 𝒫 ℝ → ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( δ ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( δ ‘ 𝑦 ) ) )
149 148 rgen ⊢ ∀ 𝑥 ∈ 𝒫 𝒫 ℝ ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( δ ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( δ ‘ 𝑦 ) )
150 reex ⊢ ℝ ∈ V
151 pwsiga ⊢ ( ℝ ∈ V → 𝒫 ℝ ∈ ( sigAlgebra ‘ ℝ ) )
152 150 151 ax-mp ⊢ 𝒫 ℝ ∈ ( sigAlgebra ‘ ℝ )
153 elrnsiga ⊢ ( 𝒫 ℝ ∈ ( sigAlgebra ‘ ℝ ) → 𝒫 ℝ ∈ ∪ ran sigAlgebra )
154 ismeas ⊢ ( 𝒫 ℝ ∈ ∪ ran sigAlgebra → ( δ ∈ ( measures ‘ 𝒫 ℝ ) ↔ ( δ : 𝒫 ℝ ⟶ ( 0 [,] +∞ ) ∧ ( δ ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝒫 ℝ ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( δ ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( δ ‘ 𝑦 ) ) ) ) )
155 152 153 154 mp2b ⊢ ( δ ∈ ( measures ‘ 𝒫 ℝ ) ↔ ( δ : 𝒫 ℝ ⟶ ( 0 [,] +∞ ) ∧ ( δ ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝒫 ℝ ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( δ ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( δ ‘ 𝑦 ) ) ) )
156 15 19 149 155 mpbir3an ⊢ δ ∈ ( measures ‘ 𝒫 ℝ )