Theorem ddemeas 31497

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 10702	. . . . . 6 ⊢ 1 ∈ ℝ*
2		0le1 11165	. . . . . 6 ⊢ 0 ≤ 1
3		pnfge 12528	. . . . . . 7 ⊢ (1 ∈ ℝ* → 1 ≤ +∞)
4	1, 3	ax-mp 5	. . . . . 6 ⊢ 1 ≤ +∞
5		0xr 10690	. . . . . . 7 ⊢ 0 ∈ ℝ*
6		pnfxr 10697	. . . . . . 7 ⊢ +∞ ∈ ℝ*
7		elicc1 12785	. . . . . . 7 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (1 ∈ (0[,]+∞) ↔ (1 ∈ ℝ* ∧ 0 ≤ 1 ∧ 1 ≤ +∞)))
8	5, 6, 7	mp2an 690	. . . . . 6 ⊢ (1 ∈ (0[,]+∞) ↔ (1 ∈ ℝ* ∧ 0 ≤ 1 ∧ 1 ≤ +∞))
9	1, 2, 4, 8	mpbir3an 1337	. . . . 5 ⊢ 1 ∈ (0[,]+∞)
10		0e0iccpnf 12850	. . . . 5 ⊢ 0 ∈ (0[,]+∞)
11	9, 10	ifcli 4515	. . . 4 ⊢ if(0 ∈ 𝑎, 1, 0) ∈ (0[,]+∞)
12	11	rgenw 3152	. . 3 ⊢ ∀𝑎 ∈ 𝒫 ℝif(0 ∈ 𝑎, 1, 0) ∈ (0[,]+∞)
13		df-dde 31494	. . . 4 ⊢ δ = (𝑎 ∈ 𝒫 ℝ ↦ if(0 ∈ 𝑎, 1, 0))
14	13	fmpt 6876	. . 3 ⊢ (∀𝑎 ∈ 𝒫 ℝif(0 ∈ 𝑎, 1, 0) ∈ (0[,]+∞) ↔ δ:𝒫 ℝ⟶(0[,]+∞))
15	12, 14	mpbi 232	. 2 ⊢ δ:𝒫 ℝ⟶(0[,]+∞)
16		0ss 4352	. . 3 ⊢ ∅ ⊆ ℝ
17		noel 4298	. . 3 ⊢ ¬ 0 ∈ ∅
18		ddeval0 31496	. . 3 ⊢ ((∅ ⊆ ℝ ∧ ¬ 0 ∈ ∅) → (δ‘∅) = 0)
19	16, 17, 18	mp2an 690	. 2 ⊢ (δ‘∅) = 0
20		rabxm 4342	. . . . . . . . 9 ⊢ 𝑥 = ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∪ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎})
21		esumeq1 31295	. . . . . . . . 9 ⊢ (𝑥 = ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∪ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) → Σ*𝑦 ∈ 𝑥(δ‘𝑦) = Σ*𝑦 ∈ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∪ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎})(δ‘𝑦))
22	20, 21	ax-mp 5	. . . . . . . 8 ⊢ Σ*𝑦 ∈ 𝑥(δ‘𝑦) = Σ*𝑦 ∈ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∪ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎})(δ‘𝑦)
23		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑥 ∈ 𝒫 𝒫 ℝ
24		nfcv 2979	. . . . . . . . 9 ⊢ Ⅎ𝑦{𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎}
25		nfcv 2979	. . . . . . . . 9 ⊢ Ⅎ𝑦{𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}
26		rabexg 5236	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∈ V)
27		rabexg 5236	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} ∈ V)
28		rabnc 4343	. . . . . . . . . 10 ⊢ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∩ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) = ∅
29	28	a1i 11	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∩ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) = ∅)
30		elrabi 3677	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} → 𝑦 ∈ 𝑥)
31	30	adantl 484	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎}) → 𝑦 ∈ 𝑥)
32		simpl 485	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎}) → 𝑥 ∈ 𝒫 𝒫 ℝ)
33		elelpwi 4553	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 𝒫 ℝ) → 𝑦 ∈ 𝒫 ℝ)
34	31, 32, 33	syl2anc 586	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎}) → 𝑦 ∈ 𝒫 ℝ)
35	15	ffvelrni 6852	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝒫 ℝ → (δ‘𝑦) ∈ (0[,]+∞))
36	34, 35	syl 17	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎}) → (δ‘𝑦) ∈ (0[,]+∞))
37		elrabi 3677	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} → 𝑦 ∈ 𝑥)
38	37	adantl 484	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) → 𝑦 ∈ 𝑥)
39		simpl 485	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) → 𝑥 ∈ 𝒫 𝒫 ℝ)
40	38, 39, 33	syl2anc 586	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) → 𝑦 ∈ 𝒫 ℝ)
41	40, 35	syl 17	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) → (δ‘𝑦) ∈ (0[,]+∞))
42	23, 24, 25, 26, 27, 29, 36, 41	esumsplit 31314	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → Σ*𝑦 ∈ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ∪ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎})(δ‘𝑦) = (Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) +𝑒 Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} (δ‘𝑦)))
43	22, 42	syl5eq 2870	. . . . . . 7 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → Σ*𝑦 ∈ 𝑥(δ‘𝑦) = (Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) +𝑒 Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} (δ‘𝑦)))
44	43	adantr 483	. . . . . 6 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) → Σ*𝑦 ∈ 𝑥(δ‘𝑦) = (Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) +𝑒 Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} (δ‘𝑦)))
45		esumeq1 31295	. . . . . . . . . . . 12 ⊢ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘} → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = Σ*𝑦 ∈ {𝑘} (δ‘𝑦))
46	45	adantl 484	. . . . . . . . . . 11 ⊢ (((((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) ∧ 𝑘 ∈ 𝑥) ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = Σ*𝑦 ∈ {𝑘} (δ‘𝑦))
47		simp-4l 781	. . . . . . . . . . . 12 ⊢ (((((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) ∧ 𝑘 ∈ 𝑥) ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}) → 𝑥 ∈ 𝒫 𝒫 ℝ)
48		vex 3499	. . . . . . . . . . . . . 14 ⊢ 𝑘 ∈ V
49	48	rabsnel 30265	. . . . . . . . . . . . 13 ⊢ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘} → 𝑘 ∈ 𝑥)
50	49	adantl 484	. . . . . . . . . . . 12 ⊢ (((((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) ∧ 𝑘 ∈ 𝑥) ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}) → 𝑘 ∈ 𝑥)
51		eleq2w 2898	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑘 → (0 ∈ 𝑎 ↔ 0 ∈ 𝑘))
52	48, 51	rabsnt 4669	. . . . . . . . . . . . 13 ⊢ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘} → 0 ∈ 𝑘)
53	52	adantl 484	. . . . . . . . . . . 12 ⊢ (((((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) ∧ 𝑘 ∈ 𝑥) ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}) → 0 ∈ 𝑘)
54		elelpwi 4553	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 𝒫 ℝ) → 𝑘 ∈ 𝒫 ℝ)
55	54	ancoms 461	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝒫 ℝ)
56	55	adantrr 715	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ (𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘)) → 𝑘 ∈ 𝒫 ℝ)
57		simpr 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ 𝒫 ℝ ∧ 𝑦 = 𝑘) → 𝑦 = 𝑘)
58	57	fveq2d 6676	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ 𝒫 ℝ ∧ 𝑦 = 𝑘) → (δ‘𝑦) = (δ‘𝑘))
59	48	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ 𝒫 ℝ → 𝑘 ∈ V)
60	15	ffvelrni 6852	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ 𝒫 ℝ → (δ‘𝑘) ∈ (0[,]+∞))
61	58, 59, 60	esumsn 31326	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝒫 ℝ → Σ*𝑦 ∈ {𝑘} (δ‘𝑦) = (δ‘𝑘))
62	56, 61	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ (𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘)) → Σ*𝑦 ∈ {𝑘} (δ‘𝑦) = (δ‘𝑘))
63	56	elpwid 4552	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ (𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘)) → 𝑘 ⊆ ℝ)
64		simprr 771	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ (𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘)) → 0 ∈ 𝑘)
65		ddeval1 31495	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ⊆ ℝ ∧ 0 ∈ 𝑘) → (δ‘𝑘) = 1)
66	63, 64, 65	syl2anc 586	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ (𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘)) → (δ‘𝑘) = 1)
67	62, 66	eqtrd 2858	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ (𝑘 ∈ 𝑥 ∧ 0 ∈ 𝑘)) → Σ*𝑦 ∈ {𝑘} (δ‘𝑦) = 1)
68	47, 50, 53, 67	syl12anc 834	. . . . . . . . . . 11 ⊢ (((((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) ∧ 𝑘 ∈ 𝑥) ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}) → Σ*𝑦 ∈ {𝑘} (δ‘𝑦) = 1)
69	46, 68	eqtrd 2858	. . . . . . . . . 10 ⊢ (((((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) ∧ 𝑘 ∈ 𝑥) ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = 1)
70		df-disj 5034	. . . . . . . . . . . . . . 15 ⊢ (Disj 𝑦 ∈ 𝑥 𝑦 ↔ ∀𝑘∃*𝑦 ∈ 𝑥 𝑘 ∈ 𝑦)
71		c0ex 10637	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ V
72		eleq1 2902	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 0 → (𝑘 ∈ 𝑦 ↔ 0 ∈ 𝑦))
73	72	rmobidv 3396	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 0 → (∃*𝑦 ∈ 𝑥 𝑘 ∈ 𝑦 ↔ ∃*𝑦 ∈ 𝑥 0 ∈ 𝑦))
74	71, 73	spcv 3608	. . . . . . . . . . . . . . 15 ⊢ (∀𝑘∃*𝑦 ∈ 𝑥 𝑘 ∈ 𝑦 → ∃*𝑦 ∈ 𝑥 0 ∈ 𝑦)
75	70, 74	sylbi 219	. . . . . . . . . . . . . 14 ⊢ (Disj 𝑦 ∈ 𝑥 𝑦 → ∃*𝑦 ∈ 𝑥 0 ∈ 𝑦)
76		rmo5 3436	. . . . . . . . . . . . . . . 16 ⊢ (∃*𝑦 ∈ 𝑥 0 ∈ 𝑦 ↔ (∃𝑦 ∈ 𝑥 0 ∈ 𝑦 → ∃!𝑦 ∈ 𝑥 0 ∈ 𝑦))
77	76	biimpi 218	. . . . . . . . . . . . . . 15 ⊢ (∃*𝑦 ∈ 𝑥 0 ∈ 𝑦 → (∃𝑦 ∈ 𝑥 0 ∈ 𝑦 → ∃!𝑦 ∈ 𝑥 0 ∈ 𝑦))
78	77	imp 409	. . . . . . . . . . . . . 14 ⊢ ((∃*𝑦 ∈ 𝑥 0 ∈ 𝑦 ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → ∃!𝑦 ∈ 𝑥 0 ∈ 𝑦)
79	75, 78	sylan 582	. . . . . . . . . . . . 13 ⊢ ((Disj 𝑦 ∈ 𝑥 𝑦 ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → ∃!𝑦 ∈ 𝑥 0 ∈ 𝑦)
80		reusn 4665	. . . . . . . . . . . . 13 ⊢ (∃!𝑦 ∈ 𝑥 0 ∈ 𝑦 ↔ ∃𝑘{𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦} = {𝑘})
81	79, 80	sylib 220	. . . . . . . . . . . 12 ⊢ ((Disj 𝑦 ∈ 𝑥 𝑦 ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → ∃𝑘{𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦} = {𝑘})
82		eleq2w 2898	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑦 → (0 ∈ 𝑎 ↔ 0 ∈ 𝑦))
83	82	cbvrabv 3493	. . . . . . . . . . . . . . . 16 ⊢ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦}
84	83	eqeq1i 2828	. . . . . . . . . . . . . . 15 ⊢ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘} ↔ {𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦} = {𝑘})
85	49	ancri 552	. . . . . . . . . . . . . . 15 ⊢ ({𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘} → (𝑘 ∈ 𝑥 ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}))
86	84, 85	sylbir 237	. . . . . . . . . . . . . 14 ⊢ ({𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦} = {𝑘} → (𝑘 ∈ 𝑥 ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}))
87	86	eximi 1835	. . . . . . . . . . . . 13 ⊢ (∃𝑘{𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦} = {𝑘} → ∃𝑘(𝑘 ∈ 𝑥 ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}))
88		df-rex 3146	. . . . . . . . . . . . 13 ⊢ (∃𝑘 ∈ 𝑥 {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘} ↔ ∃𝑘(𝑘 ∈ 𝑥 ∧ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘}))
89	87, 88	sylibr 236	. . . . . . . . . . . 12 ⊢ (∃𝑘{𝑦 ∈ 𝑥 ∣ 0 ∈ 𝑦} = {𝑘} → ∃𝑘 ∈ 𝑥 {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘})
90	81, 89	syl 17	. . . . . . . . . . 11 ⊢ ((Disj 𝑦 ∈ 𝑥 𝑦 ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → ∃𝑘 ∈ 𝑥 {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘})
91	90	adantll 712	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → ∃𝑘 ∈ 𝑥 {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = {𝑘})
92	69, 91	r19.29a 3291	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = 1)
93		elpwi 4550	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → 𝑥 ⊆ 𝒫 ℝ)
94		sspwuni 5024	. . . . . . . . . . . 12 ⊢ (𝑥 ⊆ 𝒫 ℝ ↔ ∪ 𝑥 ⊆ ℝ)
95	93, 94	sylib 220	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → ∪ 𝑥 ⊆ ℝ)
96		eluni2 4844	. . . . . . . . . . . 12 ⊢ (0 ∈ ∪ 𝑥 ↔ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦)
97	96	biimpri 230	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝑥 0 ∈ 𝑦 → 0 ∈ ∪ 𝑥)
98		ddeval1 31495	. . . . . . . . . . 11 ⊢ ((∪ 𝑥 ⊆ ℝ ∧ 0 ∈ ∪ 𝑥) → (δ‘∪ 𝑥) = 1)
99	95, 97, 98	syl2an 597	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → (δ‘∪ 𝑥) = 1)
100	99	adantlr 713	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → (δ‘∪ 𝑥) = 1)
101	92, 100	eqtr4d 2861	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = (δ‘∪ 𝑥))
102		nfre1 3308	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∃𝑦 ∈ 𝑥 0 ∈ 𝑦
103	102	nfn 1857	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 ¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦
104	82	elrab 3682	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ↔ (𝑦 ∈ 𝑥 ∧ 0 ∈ 𝑦))
105	104	exbii 1848	. . . . . . . . . . . . . . 15 ⊢ (∃𝑦 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} ↔ ∃𝑦(𝑦 ∈ 𝑥 ∧ 0 ∈ 𝑦))
106		neq0 4311	. . . . . . . . . . . . . . 15 ⊢ (¬ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = ∅ ↔ ∃𝑦 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎})
107		df-rex 3146	. . . . . . . . . . . . . . 15 ⊢ (∃𝑦 ∈ 𝑥 0 ∈ 𝑦 ↔ ∃𝑦(𝑦 ∈ 𝑥 ∧ 0 ∈ 𝑦))
108	105, 106, 107	3bitr4i 305	. . . . . . . . . . . . . 14 ⊢ (¬ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = ∅ ↔ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦)
109	108	biimpi 218	. . . . . . . . . . . . 13 ⊢ (¬ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = ∅ → ∃𝑦 ∈ 𝑥 0 ∈ 𝑦)
110	109	con1i 149	. . . . . . . . . . . 12 ⊢ (¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦 → {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} = ∅)
111	103, 110	esumeq1d 31296	. . . . . . . . . . 11 ⊢ (¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦 → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = Σ*𝑦 ∈ ∅(δ‘𝑦))
112		esumnul 31309	. . . . . . . . . . 11 ⊢ Σ*𝑦 ∈ ∅(δ‘𝑦) = 0
113	111, 112	syl6eq 2874	. . . . . . . . . 10 ⊢ (¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦 → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = 0)
114	113	adantl 484	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = 0)
115	96	biimpi 218	. . . . . . . . . . . 12 ⊢ (0 ∈ ∪ 𝑥 → ∃𝑦 ∈ 𝑥 0 ∈ 𝑦)
116	115	con3i 157	. . . . . . . . . . 11 ⊢ (¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦 → ¬ 0 ∈ ∪ 𝑥)
117		ddeval0 31496	. . . . . . . . . . 11 ⊢ ((∪ 𝑥 ⊆ ℝ ∧ ¬ 0 ∈ ∪ 𝑥) → (δ‘∪ 𝑥) = 0)
118	95, 116, 117	syl2an 597	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ ¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → (δ‘∪ 𝑥) = 0)
119	118	adantlr 713	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → (δ‘∪ 𝑥) = 0)
120	114, 119	eqtr4d 2861	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ ¬ ∃𝑦 ∈ 𝑥 0 ∈ 𝑦) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = (δ‘∪ 𝑥))
121	101, 120	pm2.61dan 811	. . . . . . 7 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) = (δ‘∪ 𝑥))
122	40	elpwid 4552	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) → 𝑦 ⊆ ℝ)
123	82	notbid 320	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑦 → (¬ 0 ∈ 𝑎 ↔ ¬ 0 ∈ 𝑦))
124	123	elrab 3682	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} ↔ (𝑦 ∈ 𝑥 ∧ ¬ 0 ∈ 𝑦))
125	124	simprbi 499	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} → ¬ 0 ∈ 𝑦)
126	125	adantl 484	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) → ¬ 0 ∈ 𝑦)
127		ddeval0 31496	. . . . . . . . . . 11 ⊢ ((𝑦 ⊆ ℝ ∧ ¬ 0 ∈ 𝑦) → (δ‘𝑦) = 0)
128	122, 126, 127	syl2anc 586	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ 𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}) → (δ‘𝑦) = 0)
129	128	esumeq2dv 31299	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} (δ‘𝑦) = Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}0)
130		vex 3499	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
131	130	rabex 5237	. . . . . . . . . 10 ⊢ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} ∈ V
132	25	esum0 31310	. . . . . . . . . 10 ⊢ ({𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} ∈ V → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}0 = 0)
133	131, 132	ax-mp 5	. . . . . . . . 9 ⊢ Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎}0 = 0
134	129, 133	syl6eq 2874	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} (δ‘𝑦) = 0)
135	134	adantr 483	. . . . . . 7 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) → Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} (δ‘𝑦) = 0)
136	121, 135	oveq12d 7176	. . . . . 6 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ 0 ∈ 𝑎} (δ‘𝑦) +𝑒 Σ*𝑦 ∈ {𝑎 ∈ 𝑥 ∣ ¬ 0 ∈ 𝑎} (δ‘𝑦)) = ((δ‘∪ 𝑥) +𝑒 0))
137		vuniex 7467	. . . . . . . . . 10 ⊢ ∪ 𝑥 ∈ V
138	137	elpw 4545	. . . . . . . . 9 ⊢ (∪ 𝑥 ∈ 𝒫 ℝ ↔ ∪ 𝑥 ⊆ ℝ)
139	138	biimpri 230	. . . . . . . 8 ⊢ (∪ 𝑥 ⊆ ℝ → ∪ 𝑥 ∈ 𝒫 ℝ)
140		iccssxr 12822	. . . . . . . . 9 ⊢ (0[,]+∞) ⊆ ℝ*
141	15	ffvelrni 6852	. . . . . . . . 9 ⊢ (∪ 𝑥 ∈ 𝒫 ℝ → (δ‘∪ 𝑥) ∈ (0[,]+∞))
142	140, 141	sseldi 3967	. . . . . . . 8 ⊢ (∪ 𝑥 ∈ 𝒫 ℝ → (δ‘∪ 𝑥) ∈ ℝ*)
143		xaddid1 12637	. . . . . . . 8 ⊢ ((δ‘∪ 𝑥) ∈ ℝ* → ((δ‘∪ 𝑥) +𝑒 0) = (δ‘∪ 𝑥))
144	95, 139, 142, 143	4syl 19	. . . . . . 7 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → ((δ‘∪ 𝑥) +𝑒 0) = (δ‘∪ 𝑥))
145	144	adantr 483	. . . . . 6 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ((δ‘∪ 𝑥) +𝑒 0) = (δ‘∪ 𝑥))
146	44, 136, 145	3eqtrrd 2863	. . . . 5 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (δ‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(δ‘𝑦))
147	146	adantrl 714	. . . 4 ⊢ ((𝑥 ∈ 𝒫 𝒫 ℝ ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → (δ‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(δ‘𝑦))
148	147	ex 415	. . 3 ⊢ (𝑥 ∈ 𝒫 𝒫 ℝ → ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (δ‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(δ‘𝑦)))
149	148	rgen 3150	. 2 ⊢ ∀𝑥 ∈ 𝒫 𝒫 ℝ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (δ‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(δ‘𝑦))
150		reex 10630	. . . 4 ⊢ ℝ ∈ V
151		pwsiga 31391	. . . 4 ⊢ (ℝ ∈ V → 𝒫 ℝ ∈ (sigAlgebra‘ℝ))
152	150, 151	ax-mp 5	. . 3 ⊢ 𝒫 ℝ ∈ (sigAlgebra‘ℝ)
153		elrnsiga 31387	. . 3 ⊢ (𝒫 ℝ ∈ (sigAlgebra‘ℝ) → 𝒫 ℝ ∈ ∪ ran sigAlgebra)
154		ismeas 31460	. . 3 ⊢ (𝒫 ℝ ∈ ∪ ran sigAlgebra → (δ ∈ (measures‘𝒫 ℝ) ↔ (δ:𝒫 ℝ⟶(0[,]+∞) ∧ (δ‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝒫 ℝ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (δ‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(δ‘𝑦)))))
155	152, 153, 154	mp2b 10	. 2 ⊢ (δ ∈ (measures‘𝒫 ℝ) ↔ (δ:𝒫 ℝ⟶(0[,]+∞) ∧ (δ‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝒫 ℝ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (δ‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(δ‘𝑦))))
156	15, 19, 149, 155	mpbir3an 1337	1 ⊢ δ ∈ (measures‘𝒫 ℝ)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083  ∀wal 1535   = wceq 1537  ∃wex 1780   ∈ wcel 2114  ∀wral 3140  ∃wrex 3141  ∃!wreu 3142  ∃*wrmo 3143  {crab 3144  Vcvv 3496   ∪ cun 3936   ∩ cin 3937   ⊆ wss 3938  ∅c0 4293  ifcif 4469  𝒫 cpw 4541  {csn 4569  ∪ cuni 4840  Disj wdisj 5033   class class class wbr 5068  ran crn 5558  ⟶wf 6353  ‘cfv 6357  (class class class)co 7158  ωcom 7582   ≼ cdom 8509  ℝcr 10538  0cc0 10539  1c1 10540  +∞cpnf 10674  ℝ^*cxr 10676   ≤ cle 10678   +_𝑒 cxad 12508  [,]cicc 12744  Σ^*cesum 31288  sigAlgebracsiga 31369  measurescmeas 31456  δcdde 31493

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-rep 5192  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-inf2 9106  ax-cnex 10595  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615  ax-pre-mulgt0 10616  ax-pre-sup 10617  ax-addf 10618  ax-mulf 10619

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-int 4879  df-iun 4923  df-iin 4924  df-disj 5034  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-se 5517  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-isom 6366  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-of 7411  df-om 7583  df-1st 7691  df-2nd 7692  df-supp 7833  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-1o 8104  df-2o 8105  df-oadd 8108  df-er 8291  df-map 8410  df-pm 8411  df-ixp 8464  df-en 8512  df-dom 8513  df-sdom 8514  df-fin 8515  df-fsupp 8836  df-fi 8877  df-sup 8908  df-inf 8909  df-oi 8976  df-card 9370  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-sub 10874  df-neg 10875  df-div 11300  df-nn 11641  df-2 11703  df-3 11704  df-4 11705  df-5 11706  df-6 11707  df-7 11708  df-8 11709  df-9 11710  df-n0 11901  df-z 11985  df-dec 12102  df-uz 12247  df-q 12352  df-rp 12393  df-xneg 12510  df-xadd 12511  df-xmul 12512  df-ioo 12745  df-ioc 12746  df-ico 12747  df-icc 12748  df-fz 12896  df-fzo 13037  df-fl 13165  df-mod 13241  df-seq 13373  df-exp 13433  df-fac 13637  df-bc 13666  df-hash 13694  df-shft 14428  df-cj 14460  df-re 14461  df-im 14462  df-sqrt 14596  df-abs 14597  df-limsup 14830  df-clim 14847  df-rlim 14848  df-sum 15045  df-ef 15423  df-sin 15425  df-cos 15426  df-pi 15428  df-struct 16487  df-ndx 16488  df-slot 16489  df-base 16491  df-sets 16492  df-ress 16493  df-plusg 16580  df-mulr 16581  df-starv 16582  df-sca 16583  df-vsca 16584  df-ip 16585  df-tset 16586  df-ple 16587  df-ds 16589  df-unif 16590  df-hom 16591  df-cco 16592  df-rest 16698  df-topn 16699  df-0g 16717  df-gsum 16718  df-topgen 16719  df-pt 16720  df-prds 16723  df-ordt 16776  df-xrs 16777  df-qtop 16782  df-imas 16783  df-xps 16785  df-mre 16859  df-mrc 16860  df-acs 16862  df-ps 17812  df-tsr 17813  df-plusf 17853  df-mgm 17854  df-sgrp 17903  df-mnd 17914  df-mhm 17958  df-submnd 17959  df-grp 18108  df-minusg 18109  df-sbg 18110  df-mulg 18227  df-subg 18278  df-cntz 18449  df-cmn 18910  df-abl 18911  df-mgp 19242  df-ur 19254  df-ring 19301  df-cring 19302  df-subrg 19535  df-abv 19590  df-lmod 19638  df-scaf 19639  df-sra 19946  df-rgmod 19947  df-psmet 20539  df-xmet 20540  df-met 20541  df-bl 20542  df-mopn 20543  df-fbas 20544  df-fg 20545  df-cnfld 20548  df-top 21504  df-topon 21521  df-topsp 21543  df-bases 21556  df-cld 21629  df-ntr 21630  df-cls 21631  df-nei 21708  df-lp 21746  df-perf 21747  df-cn 21837  df-cnp 21838  df-haus 21925  df-tx 22172  df-hmeo 22365  df-fil 22456  df-fm 22548  df-flim 22549  df-flf 22550  df-tmd 22682  df-tgp 22683  df-tsms 22737  df-trg 22770  df-xms 22932  df-ms 22933  df-tms 22934  df-nm 23194  df-ngp 23195  df-nrg 23197  df-nlm 23198  df-ii 23487  df-cncf 23488  df-limc 24466  df-dv 24467  df-log 25142  df-esum 31289  df-siga 31370  df-meas 31457  df-dde 31494

This theorem is referenced by: (None)