ddemeas

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

		Ref	Expression
	Assertion	ddemeas	$⊢ δ \in measures (𝒫 ℝ)$

Proof

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

Metamath Proof Explorer

Theorem ddemeas

Proof