Theorem ddemeas 32502

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 11135	. . . . . 6 ⊢ 1 ∈ ℝ*
2		0le1 11599	. . . . . 6 ⊢ 0 ≤ 1
3		pnfge 12967	. . . . . . 7 ⊢ (1 ∈ ℝ* → 1 ≤ +∞)
4	1, 3	ax-mp 5	. . . . . 6 ⊢ 1 ≤ +∞
5		0xr 11123	. . . . . . 7 ⊢ 0 ∈ ℝ*
6		pnfxr 11130	. . . . . . 7 ⊢ +∞ ∈ ℝ*
7		elicc1 13224	. . . . . . 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 13292	. . . . 5 ⊢ 0 ∈ (0[,]+∞)
11	9, 10	ifcli 4520	. . . 4 ⊢ if(0 ∈ 𝑎, 1, 0) ∈ (0[,]+∞)
12	11	rgenw 3065	. . 3 ⊢ ∀𝑎 ∈ 𝒫 ℝif(0 ∈ 𝑎, 1, 0) ∈ (0[,]+∞)
13		df-dde 32499	. . . 4 ⊢ δ = (𝑎 ∈ 𝒫 ℝ ↦ if(0 ∈ 𝑎, 1, 0))
14	13	fmpt 7040	. . 3 ⊢ (∀𝑎 ∈ 𝒫 ℝif(0 ∈ 𝑎, 1, 0) ∈ (0[,]+∞) ↔ δ:𝒫 ℝ⟶(0[,]+∞))
15	12, 14	mpbi 229	. 2 ⊢ δ:𝒫 ℝ⟶(0[,]+∞)
16		0ss 4343	. . 3 ⊢ ∅ ⊆ ℝ
17		noel 4277	. . 3 ⊢ ¬ 0 ∈ ∅
18		ddeval0 32501	. . 3 ⊢ ((∅ ⊆ ℝ ∧ ¬ 0 ∈ ∅) → (δ‘∅) = 0)
19	16, 17, 18	mp2an 689	. 2 ⊢ (δ‘∅) = 0
20		rabxm 4333	. . . . . . . . 9 ⊢ 𝑥 = ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∪ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎})
21		esumeq1 32300	. . . . . . . . 9 ⊢ (𝑥 = ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∪ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) → Σ*𝑦 ∈ 𝑥(δ‘𝑦) = Σ*𝑦 ∈ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∪ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎})(δ‘𝑦))
22	20, 21	ax-mp 5	. . . . . . . 8 ⊢ Σ*𝑦 ∈ 𝑥(δ‘𝑦) = Σ*𝑦 ∈ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∪ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎})(δ‘𝑦)
23		nfv 1916	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑥 ∈ 𝒫 𝒫 ℝ
24		nfcv 2904	. . . . . . . . 9 ⊢ Ⅎ𝑦{𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎}
25		nfcv 2904	. . . . . . . . 9 ⊢ Ⅎ𝑦{𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}
26		rabexg 5275	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∈ V)
27		rabexg 5275	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} ∈ V)
28		rabnc 4334	. . . . . . . . . 10 ⊢ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∩ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) = ∅
29	28	a1i 11	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∩ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) = ∅)
30		elrabi 3628	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} → 𝑦 ∈ 𝑥)
31	30	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎}) → 𝑦 ∈ 𝑥)
32		simpl 483	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎}) → 𝑥 ∈ 𝒫 𝒫 ℝ)
33		elelpwi 4557	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 𝒫 ℝ) → 𝑦 ∈ 𝒫 ℝ)
34	31, 32, 33	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎}) → 𝑦 ∈ 𝒫 ℝ)
35	15	ffvelcdmi 7016	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝒫 ℝ → (δ‘𝑦) ∈ (0[,]+∞))
36	34, 35	syl 17	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎}) → (δ‘𝑦) ∈ (0[,]+∞))
37		elrabi 3628	. . . . . . . . . . . 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 32319	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → Σ*𝑦 ∈ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∪ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎})(δ‘𝑦) = (Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) +𝑒 Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} (δ‘𝑦)))
43	22, 42	eqtrid 2788	. . . . . . 7 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → Σ*𝑦 ∈ 𝑥(δ‘𝑦) = (Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) +𝑒 Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} (δ‘𝑦)))
44	43	adantr 481	. . . . . 6 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) → Σ*𝑦 ∈ 𝑥(δ‘𝑦) = (Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) +𝑒 Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} (δ‘𝑦)))
45		esumeq1 32300	. . . . . . . . . . . 12 ⊢ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘} → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = Σ*𝑦 ∈ {𝑘} (δ‘𝑦))
46	45	adantl 482	. . . . . . . . . . 11 ⊢ (((((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) ∧ 𝑘 ∈ 𝑥) ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = Σ*𝑦 ∈ {𝑘} (δ‘𝑦))
47		simp-4l 780	. . . . . . . . . . . 12 ⊢ (((((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) ∧ 𝑘 ∈ 𝑥) ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}) → 𝑥 ∈ 𝒫 𝒫 ℝ)
48		vex 3445	. . . . . . . . . . . . . 14 ⊢ 𝑘 ∈ V
49	48	rabsnel 31135	. . . . . . . . . . . . 13 ⊢ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘} → 𝑘 ∈ 𝑥)
50	49	adantl 482	. . . . . . . . . . . 12 ⊢ (((((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) ∧ 𝑘 ∈ 𝑥) ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}) → 𝑘 ∈ 𝑥)
51		eleq2w 2820	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑘 → (0 ∈ 𝑎 ↔ 0 ∈ 𝑘))
52	48, 51	rabsnt 4679	. . . . . . . . . . . . 13 ⊢ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘} → 0 ∈ 𝑘)
53	52	adantl 482	. . . . . . . . . . . 12 ⊢ (((((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) ∧ 𝑘 ∈ 𝑥) ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}) → 0 ∈ 𝑘)
54		elelpwi 4557	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 𝒫 ℝ) → 𝑘 ∈ 𝒫 ℝ)
55	54	ancoms 459	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝒫 ℝ)
56	55	adantrr 714	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ (𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘)) → 𝑘 ∈ 𝒫 ℝ)
57		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ 𝒫 ℝ ∧ 𝑦 = 𝑘) → 𝑦 = 𝑘)
58	57	fveq2d 6829	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ 𝒫 ℝ ∧ 𝑦 = 𝑘) → (δ‘𝑦) = (δ‘𝑘))
59	48	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ 𝒫 ℝ → 𝑘 ∈ V)
60	15	ffvelcdmi 7016	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ 𝒫 ℝ → (δ‘𝑘) ∈ (0[,]+∞))
61	58, 59, 60	esumsn 32331	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝒫 ℝ → Σ*𝑦 ∈ {𝑘} (δ‘𝑦) = (δ‘𝑘))
62	56, 61	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ (𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘)) → Σ*𝑦 ∈ {𝑘} (δ‘𝑦) = (δ‘𝑘))
63	56	elpwid 4556	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ (𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘)) → 𝑘 ⊆ ℝ)
64		simprr 770	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ (𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘)) → 0 ∈ 𝑘)
65		ddeval1 32500	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ⊆ ℝ ∧ 0 ∈ 𝑘) → (δ‘𝑘) = 1)
66	63, 64, 65	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ (𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘)) → (δ‘𝑘) = 1)
67	62, 66	eqtrd 2776	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ (𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘)) → Σ*𝑦 ∈ {𝑘} (δ‘𝑦) = 1)
68	47, 50, 53, 67	syl12anc 834	. . . . . . . . . . 11 ⊢ (((((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) ∧ 𝑘 ∈ 𝑥) ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}) → Σ*𝑦 ∈ {𝑘} (δ‘𝑦) = 1)
69	46, 68	eqtrd 2776	. . . . . . . . . 10 ⊢ (((((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) ∧ 𝑘 ∈ 𝑥) ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = 1)
70		df-disj 5058	. . . . . . . . . . . . . . 15 ⊢ (Disj 𝑦 ∈ 𝑥 𝑦 ↔ ∀𝑘∃*𝑦 ∈ 𝑥 𝑘 ∈ 𝑦)
71		c0ex 11070	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ V
72		eleq1 2824	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 0 → (𝑘 ∈ 𝑦 ↔ 0 ∈ 𝑦))
73	72	rmobidv 3366	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 0 → (∃*𝑦 ∈ 𝑥 𝑘 ∈ 𝑦 ↔ ∃*𝑦 ∈ 𝑥 0 ∈ 𝑦))
74	71, 73	spcv 3553	. . . . . . . . . . . . . . 15 ⊢ (∀𝑘∃*𝑦 ∈ 𝑥 𝑘 ∈ 𝑦 → ∃*𝑦 ∈ 𝑥 0 ∈ 𝑦)
75	70, 74	sylbi 216	. . . . . . . . . . . . . 14 ⊢ (Disj 𝑦 ∈ 𝑥 𝑦 → ∃*𝑦 ∈ 𝑥 0 ∈ 𝑦)
76		rmo5 3369	. . . . . . . . . . . . . . . 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 4675	. . . . . . . . . . . . 13 ⊢ (∃!𝑦 ∈ 𝑥 0 ∈ 𝑦 ↔ ∃𝑘{𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦} = {𝑘})
81	79, 80	sylib 217	. . . . . . . . . . . 12 ⊢ ((Disj 𝑦 ∈ 𝑥 𝑦 ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → ∃𝑘{𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦} = {𝑘})
82		eleq2w 2820	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑦 → (0 ∈ 𝑎 ↔ 0 ∈ 𝑦))
83	82	cbvrabv 3413	. . . . . . . . . . . . . . . 16 ⊢ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦}
84	83	eqeq1i 2741	. . . . . . . . . . . . . . 15 ⊢ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘} ↔ {𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦} = {𝑘})
85	49	ancri 550	. . . . . . . . . . . . . . 15 ⊢ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘} → (𝑘 ∈ 𝑥 ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}))
86	84, 85	sylbir 234	. . . . . . . . . . . . . 14 ⊢ ({𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦} = {𝑘} → (𝑘 ∈ 𝑥 ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}))
87	86	eximi 1836	. . . . . . . . . . . . 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 3155	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = 1)
93		elpwi 4554	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → 𝑥 ⊆ 𝒫 ℝ)
94		sspwuni 5047	. . . . . . . . . . . 12 ⊢ (𝑥 ⊆ 𝒫 ℝ ↔ ∪ 𝑥 ⊆ ℝ)
95	93, 94	sylib 217	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → ∪ 𝑥 ⊆ ℝ)
96		eluni2 4856	. . . . . . . . . . . 12 ⊢ (0 ∈ ∪ 𝑥 ↔ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦)
97	96	biimpri 227	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝑥 0 ∈ 𝑦 → 0 ∈ ∪ 𝑥)
98		ddeval1 32500	. . . . . . . . . . 11 ⊢ ((∪ 𝑥 ⊆ ℝ ∧ 0 ∈ ∪ 𝑥) → (δ‘∪ 𝑥) = 1)
99	95, 97, 98	syl2an 596	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → (δ‘∪ 𝑥) = 1)
100	99	adantlr 712	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → (δ‘∪ 𝑥) = 1)
101	92, 100	eqtr4d 2779	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = (δ‘∪ 𝑥))
102		nfre1 3264	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∃𝑦 ∈ 𝑥 0 ∈ 𝑦
103	102	nfn 1859	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 ¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦
104	82	elrab 3634	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ↔ (𝑦 ∈ 𝑥 ∧ 0 ∈ 𝑦))
105	104	exbii 1849	. . . . . . . . . . . . . . 15 ⊢ (∃𝑦 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ↔ ∃𝑦(𝑦 ∈ 𝑥 ∧ 0 ∈ 𝑦))
106		neq0 4292	. . . . . . . . . . . . . . 15 ⊢ (¬ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = ∅ ↔ ∃𝑦 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎})
107		df-rex 3071	. . . . . . . . . . . . . . 15 ⊢ (∃𝑦 ∈ 𝑥 0 ∈ 𝑦 ↔ ∃𝑦(𝑦 ∈ 𝑥 ∧ 0 ∈ 𝑦))
108	105, 106, 107	3bitr4i 302	. . . . . . . . . . . . . 14 ⊢ (¬ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = ∅ ↔ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦)
109	108	biimpi 215	. . . . . . . . . . . . 13 ⊢ (¬ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = ∅ → ∃𝑦 ∈ 𝑥 0 ∈ 𝑦)
110	109	con1i 147	. . . . . . . . . . . 12 ⊢ (¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦 → {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = ∅)
111	103, 110	esumeq1d 32301	. . . . . . . . . . 11 ⊢ (¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦 → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = Σ*𝑦 ∈ ∅(δ‘𝑦))
112		esumnul 32314	. . . . . . . . . . 11 ⊢ Σ*𝑦 ∈ ∅(δ‘𝑦) = 0
113	111, 112	eqtrdi 2792	. . . . . . . . . 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 32501	. . . . . . . . . . 11 ⊢ ((∪ 𝑥 ⊆ ℝ ∧ ¬ 0 ∈ ∪ 𝑥) → (δ‘∪ 𝑥) = 0)
118	95, 116, 117	syl2an 596	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ ¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → (δ‘∪ 𝑥) = 0)
119	118	adantlr 712	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → (δ‘∪ 𝑥) = 0)
120	114, 119	eqtr4d 2779	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = (δ‘∪ 𝑥))
121	101, 120	pm2.61dan 810	. . . . . . 7 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = (δ‘∪ 𝑥))
122	40	elpwid 4556	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) → 𝑦 ⊆ ℝ)
123	82	notbid 317	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑦 → (¬ 0 ∈ 𝑎 ↔ ¬ 0 ∈ 𝑦))
124	123	elrab 3634	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} ↔ (𝑦 ∈ 𝑥 ∧ ¬ 0 ∈ 𝑦))
125	124	simprbi 497	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} → ¬ 0 ∈ 𝑦)
126	125	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) → ¬ 0 ∈ 𝑦)
127		ddeval0 32501	. . . . . . . . . . 11 ⊢ ((𝑦 ⊆ ℝ ∧ ¬ 0 ∈ 𝑦) → (δ‘𝑦) = 0)
128	122, 126, 127	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) → (δ‘𝑦) = 0)
129	128	esumeq2dv 32304	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} (δ‘𝑦) = Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}0)
130		vex 3445	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
131	130	rabex 5276	. . . . . . . . . 10 ⊢ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} ∈ V
132	25	esum0 32315	. . . . . . . . . 10 ⊢ ({𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} ∈ V → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}0 = 0)
133	131, 132	ax-mp 5	. . . . . . . . 9 ⊢ Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}0 = 0
134	129, 133	eqtrdi 2792	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} (δ‘𝑦) = 0)
135	134	adantr 481	. . . . . . 7 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} (δ‘𝑦) = 0)
136	121, 135	oveq12d 7355	. . . . . 6 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) +𝑒 Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} (δ‘𝑦)) = ((δ‘∪ 𝑥) +𝑒 0))
137		vuniex 7654	. . . . . . . . . 10 ⊢ ∪ 𝑥 ∈ V
138	137	elpw 4551	. . . . . . . . 9 ⊢ (∪ 𝑥 ∈ 𝒫 ℝ ↔ ∪ 𝑥 ⊆ ℝ)
139	138	biimpri 227	. . . . . . . 8 ⊢ (∪ 𝑥 ⊆ ℝ → ∪ 𝑥 ∈ 𝒫 ℝ)
140		iccssxr 13263	. . . . . . . . 9 ⊢ (0[,]+∞) ⊆ ℝ*
141	15	ffvelcdmi 7016	. . . . . . . . 9 ⊢ (∪ 𝑥 ∈ 𝒫 ℝ → (δ‘∪ 𝑥) ∈ (0[,]+∞))
142	140, 141	sselid 3930	. . . . . . . 8 ⊢ (∪ 𝑥 ∈ 𝒫 ℝ → (δ‘∪ 𝑥) ∈ ℝ*)
143		xaddid1 13076	. . . . . . . 8 ⊢ ((δ‘∪ 𝑥) ∈ ℝ* → ((δ‘∪ 𝑥) +𝑒 0) = (δ‘∪ 𝑥))
144	95, 139, 142, 143	4syl 19	. . . . . . 7 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → ((δ‘∪ 𝑥) +𝑒 0) = (δ‘∪ 𝑥))
145	144	adantr 481	. . . . . 6 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ((δ‘∪ 𝑥) +𝑒 0) = (δ‘∪ 𝑥))
146	44, 136, 145	3eqtrrd 2781	. . . . 5 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (δ‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(δ‘𝑦))
147	146	adantrl 713	. . . 4 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → (δ‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(δ‘𝑦))
148	147	ex 413	. . 3 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (δ‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(δ‘𝑦)))
149	148	rgen 3063	. 2 ⊢ ∀𝑥 ∈ 𝒫 𝒫 ℝ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (δ‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(δ‘𝑦))
150		reex 11063	. . . 4 ⊢ ℝ ∈ V
151		pwsiga 32396	. . . 4 ⊢ (ℝ ∈ V → 𝒫 ℝ ∈ (sigAlgebra‘ℝ))
152	150, 151	ax-mp 5	. . 3 ⊢ 𝒫 ℝ ∈ (sigAlgebra‘ℝ)
153		elrnsiga 32392	. . 3 ⊢ (𝒫 ℝ ∈ (sigAlgebra‘ℝ) → 𝒫 ℝ ∈ ∪ ran sigAlgebra)
154		ismeas 32465	. . 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 1538   = wceq 1540  ∃wex 1780   ∈ wcel 2105  ∀wral 3061  ∃wrex 3070  ∃!wreu 3347  ∃*wrmo 3348  {crab 3403  Vcvv 3441   ∪ cun 3896   ∩ cin 3897   ⊆ wss 3898  ∅c0 4269  ifcif 4473  𝒫 cpw 4547  {csn 4573  ∪ cuni 4852  Disj wdisj 5057   class class class wbr 5092  ran crn 5621  ⟶wf 6475  ‘cfv 6479  (class class class)co 7337  ωcom 7780   ≼ cdom 8802  ℝcr 10971  0cc0 10972  1c1 10973  +∞cpnf 11107  ℝ^*cxr 11109   ≤ cle 11111   +_𝑒 cxad 12947  [,]cicc 13183  Σ^*cesum 32293  sigAlgebracsiga 32374  measurescmeas 32461  δcdde 32498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5229  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650  ax-inf2 9498  ax-cnex 11028  ax-resscn 11029  ax-1cn 11030  ax-icn 11031  ax-addcl 11032  ax-addrcl 11033  ax-mulcl 11034  ax-mulrcl 11035  ax-mulcom 11036  ax-addass 11037  ax-mulass 11038  ax-distr 11039  ax-i2m1 11040  ax-1ne0 11041  ax-1rid 11042  ax-rnegex 11043  ax-rrecex 11044  ax-cnre 11045  ax-pre-lttri 11046  ax-pre-lttrn 11047  ax-pre-ltadd 11048  ax-pre-mulgt0 11049  ax-pre-sup 11050  ax-addf 11051  ax-mulf 11052

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-tp 4578  df-op 4580  df-uni 4853  df-int 4895  df-iun 4943  df-iin 4944  df-disj 5058  df-br 5093  df-opab 5155  df-mpt 5176  df-tr 5210  df-id 5518  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5575  df-se 5576  df-we 5577  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6238  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-isom 6488  df-riota 7293  df-ov 7340  df-oprab 7341  df-mpo 7342  df-of 7595  df-om 7781  df-1st 7899  df-2nd 7900  df-supp 8048  df-frecs 8167  df-wrecs 8198  df-recs 8272  df-rdg 8311  df-1o 8367  df-2o 8368  df-er 8569  df-map 8688  df-pm 8689  df-ixp 8757  df-en 8805  df-dom 8806  df-sdom 8807  df-fin 8808  df-fsupp 9227  df-fi 9268  df-sup 9299  df-inf 9300  df-oi 9367  df-card 9796  df-pnf 11112  df-mnf 11113  df-xr 11114  df-ltxr 11115  df-le 11116  df-sub 11308  df-neg 11309  df-div 11734  df-nn 12075  df-2 12137  df-3 12138  df-4 12139  df-5 12140  df-6 12141  df-7 12142  df-8 12143  df-9 12144  df-n0 12335  df-z 12421  df-dec 12539  df-uz 12684  df-q 12790  df-rp 12832  df-xneg 12949  df-xadd 12950  df-xmul 12951  df-ioo 13184  df-ioc 13185  df-ico 13186  df-icc 13187  df-fz 13341  df-fzo 13484  df-fl 13613  df-mod 13691  df-seq 13823  df-exp 13884  df-fac 14089  df-bc 14118  df-hash 14146  df-shft 14877  df-cj 14909  df-re 14910  df-im 14911  df-sqrt 15045  df-abs 15046  df-limsup 15279  df-clim 15296  df-rlim 15297  df-sum 15497  df-ef 15876  df-sin 15878  df-cos 15879  df-pi 15881  df-struct 16945  df-sets 16962  df-slot 16980  df-ndx 16992  df-base 17010  df-ress 17039  df-plusg 17072  df-mulr 17073  df-starv 17074  df-sca 17075  df-vsca 17076  df-ip 17077  df-tset 17078  df-ple 17079  df-ds 17081  df-unif 17082  df-hom 17083  df-cco 17084  df-rest 17230  df-topn 17231  df-0g 17249  df-gsum 17250  df-topgen 17251  df-pt 17252  df-prds 17255  df-ordt 17309  df-xrs 17310  df-qtop 17315  df-imas 17316  df-xps 17318  df-mre 17392  df-mrc 17393  df-acs 17395  df-ps 18381  df-tsr 18382  df-plusf 18422  df-mgm 18423  df-sgrp 18472  df-mnd 18483  df-mhm 18527  df-submnd 18528  df-grp 18676  df-minusg 18677  df-sbg 18678  df-mulg 18797  df-subg 18848  df-cntz 19019  df-cmn 19483  df-abl 19484  df-mgp 19816  df-ur 19833  df-ring 19880  df-cring 19881  df-subrg 20127  df-abv 20183  df-lmod 20231  df-scaf 20232  df-sra 20540  df-rgmod 20541  df-psmet 20695  df-xmet 20696  df-met 20697  df-bl 20698  df-mopn 20699  df-fbas 20700  df-fg 20701  df-cnfld 20704  df-top 22149  df-topon 22166  df-topsp 22188  df-bases 22202  df-cld 22276  df-ntr 22277  df-cls 22278  df-nei 22355  df-lp 22393  df-perf 22394  df-cn 22484  df-cnp 22485  df-haus 22572  df-tx 22819  df-hmeo 23012  df-fil 23103  df-fm 23195  df-flim 23196  df-flf 23197  df-tmd 23329  df-tgp 23330  df-tsms 23384  df-trg 23417  df-xms 23579  df-ms 23580  df-tms 23581  df-nm 23844  df-ngp 23845  df-nrg 23847  df-nlm 23848  df-ii 24146  df-cncf 24147  df-limc 25136  df-dv 25137  df-log 25818  df-esum 32294  df-siga 32375  df-meas 32462  df-dde 32499

This theorem is referenced by: (None)