Theorem ddemeas 32213

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

Assertion

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

Proof of Theorem ddemeas

Dummy variables 𝑘 𝑎 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1xr 11043	. . . . . 6 ⊢ 1 ∈ ℝ*
2		0le1 11507	. . . . . 6 ⊢ 0 ≤ 1
3		pnfge 12875	. . . . . . 7 ⊢ (1 ∈ ℝ* → 1 ≤ +∞)
4	1, 3	ax-mp 5	. . . . . 6 ⊢ 1 ≤ +∞
5		0xr 11031	. . . . . . 7 ⊢ 0 ∈ ℝ*
6		pnfxr 11038	. . . . . . 7 ⊢ +∞ ∈ ℝ*
7		elicc1 13132	. . . . . . 7 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (1 ∈ (0[,]+∞) ↔ (1 ∈ ℝ* ∧ 0 ≤ 1 ∧ 1 ≤ +∞)))
8	5, 6, 7	mp2an 689	. . . . . 6 ⊢ (1 ∈ (0[,]+∞) ↔ (1 ∈ ℝ* ∧ 0 ≤ 1 ∧ 1 ≤ +∞))
9	1, 2, 4, 8	mpbir3an 1340	. . . . 5 ⊢ 1 ∈ (0[,]+∞)
10		0e0iccpnf 13200	. . . . 5 ⊢ 0 ∈ (0[,]+∞)
11	9, 10	ifcli 4507	. . . 4 ⊢ if(0 ∈ 𝑎, 1, 0) ∈ (0[,]+∞)
12	11	rgenw 3077	. . 3 ⊢ ∀𝑎 ∈ 𝒫 ℝif(0 ∈ 𝑎, 1, 0) ∈ (0[,]+∞)
13		df-dde 32210	. . . 4 ⊢ δ = (𝑎 ∈ 𝒫 ℝ ↦ if(0 ∈ 𝑎, 1, 0))
14	13	fmpt 6993	. . 3 ⊢ (∀𝑎 ∈ 𝒫 ℝif(0 ∈ 𝑎, 1, 0) ∈ (0[,]+∞) ↔ δ:𝒫 ℝ⟶(0[,]+∞))
15	12, 14	mpbi 229	. 2 ⊢ δ:𝒫 ℝ⟶(0[,]+∞)
16		0ss 4331	. . 3 ⊢ ∅ ⊆ ℝ
17		noel 4265	. . 3 ⊢ ¬ 0 ∈ ∅
18		ddeval0 32212	. . 3 ⊢ ((∅ ⊆ ℝ ∧ ¬ 0 ∈ ∅) → (δ‘∅) = 0)
19	16, 17, 18	mp2an 689	. 2 ⊢ (δ‘∅) = 0
20		rabxm 4321	. . . . . . . . 9 ⊢ 𝑥 = ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∪ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎})
21		esumeq1 32011	. . . . . . . . 9 ⊢ (𝑥 = ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∪ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) → Σ*𝑦 ∈ 𝑥(δ‘𝑦) = Σ*𝑦 ∈ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∪ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎})(δ‘𝑦))
22	20, 21	ax-mp 5	. . . . . . . 8 ⊢ Σ*𝑦 ∈ 𝑥(δ‘𝑦) = Σ*𝑦 ∈ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∪ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎})(δ‘𝑦)
23		nfv 1918	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑥 ∈ 𝒫 𝒫 ℝ
24		nfcv 2908	. . . . . . . . 9 ⊢ Ⅎ𝑦{𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎}
25		nfcv 2908	. . . . . . . . 9 ⊢ Ⅎ𝑦{𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}
26		rabexg 5256	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∈ V)
27		rabexg 5256	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} ∈ V)
28		rabnc 4322	. . . . . . . . . 10 ⊢ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∩ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) = ∅
29	28	a1i 11	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∩ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) = ∅)
30		elrabi 3619	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} → 𝑦 ∈ 𝑥)
31	30	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎}) → 𝑦 ∈ 𝑥)
32		simpl 483	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎}) → 𝑥 ∈ 𝒫 𝒫 ℝ)
33		elelpwi 4546	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 𝒫 ℝ) → 𝑦 ∈ 𝒫 ℝ)
34	31, 32, 33	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎}) → 𝑦 ∈ 𝒫 ℝ)
35	15	ffvelrni 6969	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝒫 ℝ → (δ‘𝑦) ∈ (0[,]+∞))
36	34, 35	syl 17	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎}) → (δ‘𝑦) ∈ (0[,]+∞))
37		elrabi 3619	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} → 𝑦 ∈ 𝑥)
38	37	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) → 𝑦 ∈ 𝑥)
39		simpl 483	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) → 𝑥 ∈ 𝒫 𝒫 ℝ)
40	38, 39, 33	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) → 𝑦 ∈ 𝒫 ℝ)
41	40, 35	syl 17	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) → (δ‘𝑦) ∈ (0[,]+∞))
42	23, 24, 25, 26, 27, 29, 36, 41	esumsplit 32030	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → Σ*𝑦 ∈ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∪ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎})(δ‘𝑦) = (Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) +𝑒 Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} (δ‘𝑦)))
43	22, 42	eqtrid 2791	. . . . . . 7 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → Σ*𝑦 ∈ 𝑥(δ‘𝑦) = (Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) +𝑒 Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} (δ‘𝑦)))
44	43	adantr 481	. . . . . 6 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) → Σ*𝑦 ∈ 𝑥(δ‘𝑦) = (Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) +𝑒 Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} (δ‘𝑦)))
45		esumeq1 32011	. . . . . . . . . . . 12 ⊢ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘} → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = Σ*𝑦 ∈ {𝑘} (δ‘𝑦))
46	45	adantl 482	. . . . . . . . . . 11 ⊢ (((((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) ∧ 𝑘 ∈ 𝑥) ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = Σ*𝑦 ∈ {𝑘} (δ‘𝑦))
47		simp-4l 780	. . . . . . . . . . . 12 ⊢ (((((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) ∧ 𝑘 ∈ 𝑥) ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}) → 𝑥 ∈ 𝒫 𝒫 ℝ)
48		vex 3437	. . . . . . . . . . . . . 14 ⊢ 𝑘 ∈ V
49	48	rabsnel 30856	. . . . . . . . . . . . 13 ⊢ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘} → 𝑘 ∈ 𝑥)
50	49	adantl 482	. . . . . . . . . . . 12 ⊢ (((((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) ∧ 𝑘 ∈ 𝑥) ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}) → 𝑘 ∈ 𝑥)
51		eleq2w 2823	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑘 → (0 ∈ 𝑎 ↔ 0 ∈ 𝑘))
52	48, 51	rabsnt 4668	. . . . . . . . . . . . 13 ⊢ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘} → 0 ∈ 𝑘)
53	52	adantl 482	. . . . . . . . . . . 12 ⊢ (((((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) ∧ 𝑘 ∈ 𝑥) ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}) → 0 ∈ 𝑘)
54		elelpwi 4546	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 𝒫 ℝ) → 𝑘 ∈ 𝒫 ℝ)
55	54	ancoms 459	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝒫 ℝ)
56	55	adantrr 714	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ (𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘)) → 𝑘 ∈ 𝒫 ℝ)
57		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ 𝒫 ℝ ∧ 𝑦 = 𝑘) → 𝑦 = 𝑘)
58	57	fveq2d 6787	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ 𝒫 ℝ ∧ 𝑦 = 𝑘) → (δ‘𝑦) = (δ‘𝑘))
59	48	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ 𝒫 ℝ → 𝑘 ∈ V)
60	15	ffvelrni 6969	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ 𝒫 ℝ → (δ‘𝑘) ∈ (0[,]+∞))
61	58, 59, 60	esumsn 32042	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝒫 ℝ → Σ*𝑦 ∈ {𝑘} (δ‘𝑦) = (δ‘𝑘))
62	56, 61	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ (𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘)) → Σ*𝑦 ∈ {𝑘} (δ‘𝑦) = (δ‘𝑘))
63	56	elpwid 4545	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ (𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘)) → 𝑘 ⊆ ℝ)
64		simprr 770	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ (𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘)) → 0 ∈ 𝑘)
65		ddeval1 32211	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ⊆ ℝ ∧ 0 ∈ 𝑘) → (δ‘𝑘) = 1)
66	63, 64, 65	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ (𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘)) → (δ‘𝑘) = 1)
67	62, 66	eqtrd 2779	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ (𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘)) → Σ*𝑦 ∈ {𝑘} (δ‘𝑦) = 1)
68	47, 50, 53, 67	syl12anc 834	. . . . . . . . . . 11 ⊢ (((((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) ∧ 𝑘 ∈ 𝑥) ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}) → Σ*𝑦 ∈ {𝑘} (δ‘𝑦) = 1)
69	46, 68	eqtrd 2779	. . . . . . . . . 10 ⊢ (((((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) ∧ 𝑘 ∈ 𝑥) ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = 1)
70		df-disj 5041	. . . . . . . . . . . . . . 15 ⊢ (Disj 𝑦 ∈ 𝑥 𝑦 ↔ ∀𝑘∃*𝑦 ∈ 𝑥 𝑘 ∈ 𝑦)
71		c0ex 10978	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ V
72		eleq1 2827	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 0 → (𝑘 ∈ 𝑦 ↔ 0 ∈ 𝑦))
73	72	rmobidv 3330	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 0 → (∃*𝑦 ∈ 𝑥 𝑘 ∈ 𝑦 ↔ ∃*𝑦 ∈ 𝑥 0 ∈ 𝑦))
74	71, 73	spcv 3545	. . . . . . . . . . . . . . 15 ⊢ (∀𝑘∃*𝑦 ∈ 𝑥 𝑘 ∈ 𝑦 → ∃*𝑦 ∈ 𝑥 0 ∈ 𝑦)
75	70, 74	sylbi 216	. . . . . . . . . . . . . 14 ⊢ (Disj 𝑦 ∈ 𝑥 𝑦 → ∃*𝑦 ∈ 𝑥 0 ∈ 𝑦)
76		rmo5 3366	. . . . . . . . . . . . . . . 16 ⊢ (∃*𝑦 ∈ 𝑥 0 ∈ 𝑦 ↔ (∃𝑦 ∈ 𝑥 0 ∈ 𝑦 → ∃!𝑦 ∈ 𝑥 0 ∈ 𝑦))
77	76	biimpi 215	. . . . . . . . . . . . . . 15 ⊢ (∃*𝑦 ∈ 𝑥 0 ∈ 𝑦 → (∃𝑦 ∈ 𝑥 0 ∈ 𝑦 → ∃!𝑦 ∈ 𝑥 0 ∈ 𝑦))
78	77	imp 407	. . . . . . . . . . . . . 14 ⊢ ((∃*𝑦 ∈ 𝑥 0 ∈ 𝑦 ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → ∃!𝑦 ∈ 𝑥 0 ∈ 𝑦)
79	75, 78	sylan 580	. . . . . . . . . . . . 13 ⊢ ((Disj 𝑦 ∈ 𝑥 𝑦 ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → ∃!𝑦 ∈ 𝑥 0 ∈ 𝑦)
80		reusn 4664	. . . . . . . . . . . . 13 ⊢ (∃!𝑦 ∈ 𝑥 0 ∈ 𝑦 ↔ ∃𝑘{𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦} = {𝑘})
81	79, 80	sylib 217	. . . . . . . . . . . 12 ⊢ ((Disj 𝑦 ∈ 𝑥 𝑦 ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → ∃𝑘{𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦} = {𝑘})
82		eleq2w 2823	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑦 → (0 ∈ 𝑎 ↔ 0 ∈ 𝑦))
83	82	cbvrabv 3427	. . . . . . . . . . . . . . . 16 ⊢ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦}
84	83	eqeq1i 2744	. . . . . . . . . . . . . . 15 ⊢ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘} ↔ {𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦} = {𝑘})
85	49	ancri 550	. . . . . . . . . . . . . . 15 ⊢ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘} → (𝑘 ∈ 𝑥 ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}))
86	84, 85	sylbir 234	. . . . . . . . . . . . . 14 ⊢ ({𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦} = {𝑘} → (𝑘 ∈ 𝑥 ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}))
87	86	eximi 1838	. . . . . . . . . . . . 13 ⊢ (∃𝑘{𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦} = {𝑘} → ∃𝑘(𝑘 ∈ 𝑥 ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}))
88		df-rex 3071	. . . . . . . . . . . . 13 ⊢ (∃𝑘 ∈ 𝑥 {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘} ↔ ∃𝑘(𝑘 ∈ 𝑥 ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}))
89	87, 88	sylibr 233	. . . . . . . . . . . 12 ⊢ (∃𝑘{𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦} = {𝑘} → ∃𝑘 ∈ 𝑥 {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘})
90	81, 89	syl 17	. . . . . . . . . . 11 ⊢ ((Disj 𝑦 ∈ 𝑥 𝑦 ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → ∃𝑘 ∈ 𝑥 {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘})
91	90	adantll 711	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → ∃𝑘 ∈ 𝑥 {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘})
92	69, 91	r19.29a 3219	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = 1)
93		elpwi 4543	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → 𝑥 ⊆ 𝒫 ℝ)
94		sspwuni 5030	. . . . . . . . . . . 12 ⊢ (𝑥 ⊆ 𝒫 ℝ ↔ ∪ 𝑥 ⊆ ℝ)
95	93, 94	sylib 217	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → ∪ 𝑥 ⊆ ℝ)
96		eluni2 4844	. . . . . . . . . . . 12 ⊢ (0 ∈ ∪ 𝑥 ↔ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦)
97	96	biimpri 227	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝑥 0 ∈ 𝑦 → 0 ∈ ∪ 𝑥)
98		ddeval1 32211	. . . . . . . . . . 11 ⊢ ((∪ 𝑥 ⊆ ℝ ∧ 0 ∈ ∪ 𝑥) → (δ‘∪ 𝑥) = 1)
99	95, 97, 98	syl2an 596	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → (δ‘∪ 𝑥) = 1)
100	99	adantlr 712	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → (δ‘∪ 𝑥) = 1)
101	92, 100	eqtr4d 2782	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = (δ‘∪ 𝑥))
102		nfre1 3240	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∃𝑦 ∈ 𝑥 0 ∈ 𝑦
103	102	nfn 1861	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 ¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦
104	82	elrab 3625	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ↔ (𝑦 ∈ 𝑥 ∧ 0 ∈ 𝑦))
105	104	exbii 1851	. . . . . . . . . . . . . . 15 ⊢ (∃𝑦 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ↔ ∃𝑦(𝑦 ∈ 𝑥 ∧ 0 ∈ 𝑦))
106		neq0 4280	. . . . . . . . . . . . . . 15 ⊢ (¬ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = ∅ ↔ ∃𝑦 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎})
107		df-rex 3071	. . . . . . . . . . . . . . 15 ⊢ (∃𝑦 ∈ 𝑥 0 ∈ 𝑦 ↔ ∃𝑦(𝑦 ∈ 𝑥 ∧ 0 ∈ 𝑦))
108	105, 106, 107	3bitr4i 303	. . . . . . . . . . . . . 14 ⊢ (¬ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = ∅ ↔ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦)
109	108	biimpi 215	. . . . . . . . . . . . 13 ⊢ (¬ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = ∅ → ∃𝑦 ∈ 𝑥 0 ∈ 𝑦)
110	109	con1i 147	. . . . . . . . . . . 12 ⊢ (¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦 → {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = ∅)
111	103, 110	esumeq1d 32012	. . . . . . . . . . 11 ⊢ (¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦 → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = Σ*𝑦 ∈ ∅(δ‘𝑦))
112		esumnul 32025	. . . . . . . . . . 11 ⊢ Σ*𝑦 ∈ ∅(δ‘𝑦) = 0
113	111, 112	eqtrdi 2795	. . . . . . . . . 10 ⊢ (¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦 → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = 0)
114	113	adantl 482	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = 0)
115	96	biimpi 215	. . . . . . . . . . . 12 ⊢ (0 ∈ ∪ 𝑥 → ∃𝑦 ∈ 𝑥 0 ∈ 𝑦)
116	115	con3i 154	. . . . . . . . . . 11 ⊢ (¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦 → ¬ 0 ∈ ∪ 𝑥)
117		ddeval0 32212	. . . . . . . . . . 11 ⊢ ((∪ 𝑥 ⊆ ℝ ∧ ¬ 0 ∈ ∪ 𝑥) → (δ‘∪ 𝑥) = 0)
118	95, 116, 117	syl2an 596	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ ¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → (δ‘∪ 𝑥) = 0)
119	118	adantlr 712	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → (δ‘∪ 𝑥) = 0)
120	114, 119	eqtr4d 2782	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = (δ‘∪ 𝑥))
121	101, 120	pm2.61dan 810	. . . . . . 7 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = (δ‘∪ 𝑥))
122	40	elpwid 4545	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) → 𝑦 ⊆ ℝ)
123	82	notbid 318	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑦 → (¬ 0 ∈ 𝑎 ↔ ¬ 0 ∈ 𝑦))
124	123	elrab 3625	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} ↔ (𝑦 ∈ 𝑥 ∧ ¬ 0 ∈ 𝑦))
125	124	simprbi 497	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} → ¬ 0 ∈ 𝑦)
126	125	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) → ¬ 0 ∈ 𝑦)
127		ddeval0 32212	. . . . . . . . . . 11 ⊢ ((𝑦 ⊆ ℝ ∧ ¬ 0 ∈ 𝑦) → (δ‘𝑦) = 0)
128	122, 126, 127	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) → (δ‘𝑦) = 0)
129	128	esumeq2dv 32015	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} (δ‘𝑦) = Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}0)
130		vex 3437	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
131	130	rabex 5257	. . . . . . . . . 10 ⊢ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} ∈ V
132	25	esum0 32026	. . . . . . . . . 10 ⊢ ({𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} ∈ V → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}0 = 0)
133	131, 132	ax-mp 5	. . . . . . . . 9 ⊢ Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}0 = 0
134	129, 133	eqtrdi 2795	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} (δ‘𝑦) = 0)
135	134	adantr 481	. . . . . . 7 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} (δ‘𝑦) = 0)
136	121, 135	oveq12d 7302	. . . . . 6 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) +𝑒 Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} (δ‘𝑦)) = ((δ‘∪ 𝑥) +𝑒 0))
137		vuniex 7601	. . . . . . . . . 10 ⊢ ∪ 𝑥 ∈ V
138	137	elpw 4538	. . . . . . . . 9 ⊢ (∪ 𝑥 ∈ 𝒫 ℝ ↔ ∪ 𝑥 ⊆ ℝ)
139	138	biimpri 227	. . . . . . . 8 ⊢ (∪ 𝑥 ⊆ ℝ → ∪ 𝑥 ∈ 𝒫 ℝ)
140		iccssxr 13171	. . . . . . . . 9 ⊢ (0[,]+∞) ⊆ ℝ*
141	15	ffvelrni 6969	. . . . . . . . 9 ⊢ (∪ 𝑥 ∈ 𝒫 ℝ → (δ‘∪ 𝑥) ∈ (0[,]+∞))
142	140, 141	sselid 3920	. . . . . . . 8 ⊢ (∪ 𝑥 ∈ 𝒫 ℝ → (δ‘∪ 𝑥) ∈ ℝ*)
143		xaddid1 12984	. . . . . . . 8 ⊢ ((δ‘∪ 𝑥) ∈ ℝ* → ((δ‘∪ 𝑥) +𝑒 0) = (δ‘∪ 𝑥))
144	95, 139, 142, 143	4syl 19	. . . . . . 7 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → ((δ‘∪ 𝑥) +𝑒 0) = (δ‘∪ 𝑥))
145	144	adantr 481	. . . . . 6 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ((δ‘∪ 𝑥) +𝑒 0) = (δ‘∪ 𝑥))
146	44, 136, 145	3eqtrrd 2784	. . . . 5 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (δ‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(δ‘𝑦))
147	146	adantrl 713	. . . 4 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → (δ‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(δ‘𝑦))
148	147	ex 413	. . 3 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (δ‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(δ‘𝑦)))
149	148	rgen 3075	. 2 ⊢ ∀𝑥 ∈ 𝒫 𝒫 ℝ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (δ‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(δ‘𝑦))
150		reex 10971	. . . 4 ⊢ ℝ ∈ V
151		pwsiga 32107	. . . 4 ⊢ (ℝ ∈ V → 𝒫 ℝ ∈ (sigAlgebra‘ℝ))
152	150, 151	ax-mp 5	. . 3 ⊢ 𝒫 ℝ ∈ (sigAlgebra‘ℝ)
153		elrnsiga 32103	. . 3 ⊢ (𝒫 ℝ ∈ (sigAlgebra‘ℝ) → 𝒫 ℝ ∈ ∪ ran sigAlgebra)
154		ismeas 32176	. . 3 ⊢ (𝒫 ℝ ∈ ∪ ran sigAlgebra → (δ ∈ (measures‘𝒫 ℝ) ↔ (δ:𝒫 ℝ⟶(0[,]+∞) ∧ (δ‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝒫 ℝ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (δ‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(δ‘𝑦)))))
155	152, 153, 154	mp2b 10	. 2 ⊢ (δ ∈ (measures‘𝒫 ℝ) ↔ (δ:𝒫 ℝ⟶(0[,]+∞) ∧ (δ‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝒫 ℝ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (δ‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(δ‘𝑦))))
156	15, 19, 149, 155	mpbir3an 1340	1 ⊢ δ ∈ (measures‘𝒫 ℝ)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086  ∀wal 1537   = wceq 1539  ∃wex 1782   ∈ wcel 2107  ∀wral 3065  ∃wrex 3066  ∃!wreu 3067  ∃*wrmo 3068  {crab 3069  Vcvv 3433   ∪ cun 3886   ∩ cin 3887   ⊆ wss 3888  ∅c0 4257  ifcif 4460  𝒫 cpw 4534  {csn 4562  ∪ cuni 4840  Disj wdisj 5040   class class class wbr 5075  ran crn 5591  ⟶wf 6433  ‘cfv 6437  (class class class)co 7284  ωcom 7721   ≼ cdom 8740  ℝcr 10879  0cc0 10880  1c1 10881  +∞cpnf 11015  ℝ^*cxr 11017   ≤ cle 11019   +_𝑒 cxad 12855  [,]cicc 13091  Σ^*cesum 32004  sigAlgebracsiga 32085  measurescmeas 32172  δcdde 32209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-inf2 9408  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957  ax-pre-sup 10958  ax-addf 10959  ax-mulf 10960

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-tp 4567  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-iin 4928  df-disj 5041  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-se 5546  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-isom 6446  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-of 7542  df-om 7722  df-1st 7840  df-2nd 7841  df-supp 7987  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-1o 8306  df-2o 8307  df-er 8507  df-map 8626  df-pm 8627  df-ixp 8695  df-en 8743  df-dom 8744  df-sdom 8745  df-fin 8746  df-fsupp 9138  df-fi 9179  df-sup 9210  df-inf 9211  df-oi 9278  df-card 9706  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-div 11642  df-nn 11983  df-2 12045  df-3 12046  df-4 12047  df-5 12048  df-6 12049  df-7 12050  df-8 12051  df-9 12052  df-n0 12243  df-z 12329  df-dec 12447  df-uz 12592  df-q 12698  df-rp 12740  df-xneg 12857  df-xadd 12858  df-xmul 12859  df-ioo 13092  df-ioc 13093  df-ico 13094  df-icc 13095  df-fz 13249  df-fzo 13392  df-fl 13521  df-mod 13599  df-seq 13731  df-exp 13792  df-fac 13997  df-bc 14026  df-hash 14054  df-shft 14787  df-cj 14819  df-re 14820  df-im 14821  df-sqrt 14955  df-abs 14956  df-limsup 15189  df-clim 15206  df-rlim 15207  df-sum 15407  df-ef 15786  df-sin 15788  df-cos 15789  df-pi 15791  df-struct 16857  df-sets 16874  df-slot 16892  df-ndx 16904  df-base 16922  df-ress 16951  df-plusg 16984  df-mulr 16985  df-starv 16986  df-sca 16987  df-vsca 16988  df-ip 16989  df-tset 16990  df-ple 16991  df-ds 16993  df-unif 16994  df-hom 16995  df-cco 16996  df-rest 17142  df-topn 17143  df-0g 17161  df-gsum 17162  df-topgen 17163  df-pt 17164  df-prds 17167  df-ordt 17221  df-xrs 17222  df-qtop 17227  df-imas 17228  df-xps 17230  df-mre 17304  df-mrc 17305  df-acs 17307  df-ps 18293  df-tsr 18294  df-plusf 18334  df-mgm 18335  df-sgrp 18384  df-mnd 18395  df-mhm 18439  df-submnd 18440  df-grp 18589  df-minusg 18590  df-sbg 18591  df-mulg 18710  df-subg 18761  df-cntz 18932  df-cmn 19397  df-abl 19398  df-mgp 19730  df-ur 19747  df-ring 19794  df-cring 19795  df-subrg 20031  df-abv 20086  df-lmod 20134  df-scaf 20135  df-sra 20443  df-rgmod 20444  df-psmet 20598  df-xmet 20599  df-met 20600  df-bl 20601  df-mopn 20602  df-fbas 20603  df-fg 20604  df-cnfld 20607  df-top 22052  df-topon 22069  df-topsp 22091  df-bases 22105  df-cld 22179  df-ntr 22180  df-cls 22181  df-nei 22258  df-lp 22296  df-perf 22297  df-cn 22387  df-cnp 22388  df-haus 22475  df-tx 22722  df-hmeo 22915  df-fil 23006  df-fm 23098  df-flim 23099  df-flf 23100  df-tmd 23232  df-tgp 23233  df-tsms 23287  df-trg 23320  df-xms 23482  df-ms 23483  df-tms 23484  df-nm 23747  df-ngp 23748  df-nrg 23750  df-nlm 23751  df-ii 24049  df-cncf 24050  df-limc 25039  df-dv 25040  df-log 25721  df-esum 32005  df-siga 32086  df-meas 32173  df-dde 32210

This theorem is referenced by: (None)