omsmeas

Description: The restriction of a constructed outer measure to Caratheodory measurable sets is a measure. This theorem allows to construct measures from pre-measures with the required characteristics, as for the Lebesgue measure. (Contributed by Thierry Arnoux, 17-May-2020)

	Ref	Expression
Hypotheses	omsmeas.m	$⊢ M = toOMeas (R)$
	omsmeas.s	$⊢ S = toCaraSiga (M)$
	omsmeas.o	$⊢ φ \to Q \in V$
	omsmeas.r	$⊢ φ \to R : Q ⟶ [0, +∞]$
	omsmeas.d	$⊢ φ \to \emptyset \in dom R$
	omsmeas.0	$⊢ φ \to R (\emptyset) = 0$
Assertion	omsmeas	$⊢ φ \to {M ↾}_{S} \in measures (S)$

Proof

Step	Hyp	Ref	Expression
1		omsmeas.m	$⊢ M = toOMeas (R)$
2		omsmeas.s	$⊢ S = toCaraSiga (M)$
3		omsmeas.o	$⊢ φ \to Q \in V$
4		omsmeas.r	$⊢ φ \to R : Q ⟶ [0, +∞]$
5		omsmeas.d	$⊢ φ \to \emptyset \in dom R$
6		omsmeas.0	$⊢ φ \to R (\emptyset) = 0$
7		omsf	$⊢ (Q \in V \land R : Q ⟶ [0, +∞]) \to toOMeas (R) : 𝒫 ⋃ dom R ⟶ [0, +∞]$
8	3 4 7	syl2anc	$⊢ φ \to toOMeas (R) : 𝒫 ⋃ dom R ⟶ [0, +∞]$
9	1	a1i	$⊢ φ \to M = toOMeas (R)$
10	4	fdmd	$⊢ φ \to dom R = Q$
11	10	eqcomd	$⊢ φ \to Q = dom R$
12	11	unieqd	$⊢ φ \to ⋃ Q = ⋃ dom R$
13	12	pweqd	$⊢ φ \to 𝒫 ⋃ Q = 𝒫 ⋃ dom R$
14	9 13	feq12d	$⊢ φ \to (M : 𝒫 ⋃ Q ⟶ [0, +∞] \leftrightarrow toOMeas (R) : 𝒫 ⋃ dom R ⟶ [0, +∞])$
15	8 14	mpbird	$⊢ φ \to M : 𝒫 ⋃ Q ⟶ [0, +∞]$
16	3	uniexd	$⊢ φ \to ⋃ Q \in V$
17	16 15	carsgcl	$⊢ φ \to toCaraSiga (M) \subseteq 𝒫 ⋃ Q$
18	2 17	eqsstrid	$⊢ φ \to S \subseteq 𝒫 ⋃ Q$
19	15 18	fssresd	$⊢ φ \to ({M ↾}_{S}) : S ⟶ [0, +∞]$
20	1 3 4 5 6	oms0	$⊢ φ \to M (\emptyset) = 0$
21	16 15 20	0elcarsg	$⊢ φ \to \emptyset \in toCaraSiga (M)$
22	21 2	eleqtrrdi	$⊢ φ \to \emptyset \in S$
23		fvres	$⊢ \emptyset \in S \to ({M ↾}_{S}) (\emptyset) = M (\emptyset)$
24	22 23	syl	$⊢ φ \to ({M ↾}_{S}) (\emptyset) = M (\emptyset)$
25	24 20	eqtrd	$⊢ φ \to ({M ↾}_{S}) (\emptyset) = 0$
26		nfcv	$⊢ \underline{Ⅎ} g f$
27		nfcv	$⊢ \underline{Ⅎ} f g$
28		id	$⊢ f = g \to f = g$
29	26 27 28	cbvdisj	$⊢ \underset{f \in e}{Disj} f \leftrightarrow \underset{g \in e}{Disj} g$
30	29	anbi2i	$⊢ (e ≼ ω \land \underset{f \in e}{Disj} f) \leftrightarrow (e ≼ ω \land \underset{g \in e}{Disj} g)$
31	3	ad2antrr	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to Q \in V$
32	4	ad2antrr	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to R : Q ⟶ [0, +∞]$
33		simplr	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to e \in 𝒫 S$
34	33	elpwid	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to e \subseteq S$
35	18	ad2antrr	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to S \subseteq 𝒫 ⋃ Q$
36	34 35	sstrd	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to e \subseteq 𝒫 ⋃ Q$
37	36	sselda	$⊢ (((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \land f \in e) \to f \in 𝒫 ⋃ Q$
38	37	elpwid	$⊢ (((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \land f \in e) \to f \subseteq ⋃ Q$
39		simprl	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to e ≼ ω$
40	1 31 32 38 39	omssubadd	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to M (⋃_{f \in e} f) \leq \underset{f \in e}{\sum^{*}} M (f)$
41	16	ad2antrr	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to ⋃ Q \in V$
42	15	ad2antrr	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to M : 𝒫 ⋃ Q ⟶ [0, +∞]$
43	20	ad2antrr	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to M (\emptyset) = 0$
44		uniiun	$⊢ ⋃ x = ⋃_{y \in x} y$
45	44	fveq2i	$⊢ M (⋃ x) = M (⋃_{y \in x} y)$
46	3	3ad2ant1	$⊢ (φ \land x ≼ ω \land x \subseteq 𝒫 ⋃ Q) \to Q \in V$
47	4	3ad2ant1	$⊢ (φ \land x ≼ ω \land x \subseteq 𝒫 ⋃ Q) \to R : Q ⟶ [0, +∞]$
48		simpl3	$⊢ ((φ \land x ≼ ω \land x \subseteq 𝒫 ⋃ Q) \land y \in x) \to x \subseteq 𝒫 ⋃ Q$
49		simpr	$⊢ ((φ \land x ≼ ω \land x \subseteq 𝒫 ⋃ Q) \land y \in x) \to y \in x$
50	48 49	sseldd	$⊢ ((φ \land x ≼ ω \land x \subseteq 𝒫 ⋃ Q) \land y \in x) \to y \in 𝒫 ⋃ Q$
51	50	elpwid	$⊢ ((φ \land x ≼ ω \land x \subseteq 𝒫 ⋃ Q) \land y \in x) \to y \subseteq ⋃ Q$
52		simp2	$⊢ (φ \land x ≼ ω \land x \subseteq 𝒫 ⋃ Q) \to x ≼ ω$
53	1 46 47 51 52	omssubadd	$⊢ (φ \land x ≼ ω \land x \subseteq 𝒫 ⋃ Q) \to M (⋃_{y \in x} y) \leq \underset{y \in x}{\sum^{*}} M (y)$
54	45 53	eqbrtrid	$⊢ (φ \land x ≼ ω \land x \subseteq 𝒫 ⋃ Q) \to M (⋃ x) \leq \underset{y \in x}{\sum^{*}} M (y)$
55	54	3adant1r	$⊢ ((φ \land e \in 𝒫 S) \land x ≼ ω \land x \subseteq 𝒫 ⋃ Q) \to M (⋃ x) \leq \underset{y \in x}{\sum^{*}} M (y)$
56	55	3adant1r	$⊢ (((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \land x ≼ ω \land x \subseteq 𝒫 ⋃ Q) \to M (⋃ x) \leq \underset{y \in x}{\sum^{*}} M (y)$
57	3	3ad2ant1	$⊢ (φ \land x \subseteq y \land y \in 𝒫 ⋃ Q) \to Q \in V$
58	4	3ad2ant1	$⊢ (φ \land x \subseteq y \land y \in 𝒫 ⋃ Q) \to R : Q ⟶ [0, +∞]$
59		simp2	$⊢ (φ \land x \subseteq y \land y \in 𝒫 ⋃ Q) \to x \subseteq y$
60		elpwi	$⊢ y \in 𝒫 ⋃ Q \to y \subseteq ⋃ Q$
61	60	3ad2ant3	$⊢ (φ \land x \subseteq y \land y \in 𝒫 ⋃ Q) \to y \subseteq ⋃ Q$
62	1 57 58 59 61	omsmon	$⊢ (φ \land x \subseteq y \land y \in 𝒫 ⋃ Q) \to M (x) \leq M (y)$
63	62	3adant1r	$⊢ ((φ \land e \in 𝒫 S) \land x \subseteq y \land y \in 𝒫 ⋃ Q) \to M (x) \leq M (y)$
64	63	3adant1r	$⊢ (((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \land x \subseteq y \land y \in 𝒫 ⋃ Q) \to M (x) \leq M (y)$
65		elpwi	$⊢ e \in 𝒫 S \to e \subseteq S$
66	65	ad2antlr	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to e \subseteq S$
67	66 2	sseqtrdi	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to e \subseteq toCaraSiga (M)$
68	41 42 43 56 64 39 67	carsgclctun	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to ⋃ e \in toCaraSiga (M)$
69	68 2	eleqtrrdi	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to ⋃ e \in S$
70		fvres	$⊢ ⋃ e \in S \to ({M ↾}_{S}) (⋃ e) = M (⋃ e)$
71		uniiun	$⊢ ⋃ e = ⋃_{f \in e} f$
72	71	fveq2i	$⊢ M (⋃ e) = M (⋃_{f \in e} f)$
73	70 72	eqtrdi	$⊢ ⋃ e \in S \to ({M ↾}_{S}) (⋃ e) = M (⋃_{f \in e} f)$
74	69 73	syl	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to ({M ↾}_{S}) (⋃ e) = M (⋃_{f \in e} f)$
75		nfv	$⊢ Ⅎ f ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g))$
76	66	sselda	$⊢ (((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \land f \in e) \to f \in S$
77		fvres	$⊢ f \in S \to ({M ↾}_{S}) (f) = M (f)$
78	76 77	syl	$⊢ (((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \land f \in e) \to ({M ↾}_{S}) (f) = M (f)$
79	78	ralrimiva	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to \forall f \in e ({M ↾}_{S}) (f) = M (f)$
80	75 79	esumeq2d	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to \underset{f \in e}{\sum^{}} ({M ↾}_{S}) (f) = \underset{f \in e}{\sum^{}} M (f)$
81	40 74 80	3brtr4d	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to ({M ↾}_{S}) (⋃ e) \leq \underset{f \in e}{\sum^{*}} ({M ↾}_{S}) (f)$
82		snex	$⊢ \{\emptyset\} \in V$
83	82	a1i	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to \{\emptyset\} \in V$
84	42	adantr	$⊢ (((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \land f \in e) \to M : 𝒫 ⋃ Q ⟶ [0, +∞]$
85	84 37	ffvelcdmd	$⊢ (((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \land f \in e) \to M (f) \in [0, +∞]$
86		elsni	$⊢ f \in \{\emptyset\} \to f = \emptyset$
87	86	fveq2d	$⊢ f \in \{\emptyset\} \to M (f) = M (\emptyset)$
88	87 43	sylan9eqr	$⊢ (((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \land f \in \{\emptyset\}) \to M (f) = 0$
89	33 83 85 88	esumpad2	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to \underset{f \in e ∖ \{\emptyset\}}{\sum^{}} M (f) = \underset{f \in e}{\sum^{}} M (f)$
90		neldifsnd	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to \neg \emptyset \in (e ∖ \{\emptyset\})$
91		difss	$⊢ e ∖ \{\emptyset\} \subseteq e$
92		ssdomg	$⊢ e \in 𝒫 S \to (e ∖ \{\emptyset\} \subseteq e \to (e ∖ \{\emptyset\}) ≼ e)$
93	33 91 92	mpisyl	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to (e ∖ \{\emptyset\}) ≼ e$
94		domtr	$⊢ ((e ∖ \{\emptyset\}) ≼ e \land e ≼ ω) \to (e ∖ \{\emptyset\}) ≼ ω$
95	93 39 94	syl2anc	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to (e ∖ \{\emptyset\}) ≼ ω$
96	67	ssdifssd	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to e ∖ \{\emptyset\} \subseteq toCaraSiga (M)$
97		simprr	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to \underset{g \in e}{Disj} g$
98		nfcv	$⊢ \underline{Ⅎ} y g$
99		nfcv	$⊢ \underline{Ⅎ} g y$
100		id	$⊢ g = y \to g = y$
101	98 99 100	cbvdisj	$⊢ \underset{g \in e}{Disj} g \leftrightarrow \underset{y \in e}{Disj} y$
102	97 101	sylib	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to \underset{y \in e}{Disj} y$
103		disjss1	$⊢ e ∖ \{\emptyset\} \subseteq e \to (\underset{y \in e}{Disj} y \to \underset{y \in e ∖ \{\emptyset\}}{Disj} y)$
104	91 102 103	mpsyl	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to \underset{y \in e ∖ \{\emptyset\}}{Disj} y$
105	41 42 43 56 90 95 96 104 64	carsggect	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to \underset{f \in e ∖ \{\emptyset\}}{\sum^{*}} M (f) \leq M (⋃ (e ∖ \{\emptyset\}))$
106	89 105	eqbrtrrd	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to \underset{f \in e}{\sum^{*}} M (f) \leq M (⋃ (e ∖ \{\emptyset\}))$
107		unidif0	$⊢ ⋃ (e ∖ \{\emptyset\}) = ⋃ e$
108	107	fveq2i	$⊢ M (⋃ (e ∖ \{\emptyset\})) = M (⋃ e)$
109	106 108	breqtrdi	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to \underset{f \in e}{\sum^{*}} M (f) \leq M (⋃ e)$
110	69 70	syl	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to ({M ↾}_{S}) (⋃ e) = M (⋃ e)$
111	109 80 110	3brtr4d	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to \underset{f \in e}{\sum^{*}} ({M ↾}_{S}) (f) \leq ({M ↾}_{S}) (⋃ e)$
112	81 111	jca	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to (({M ↾}_{S}) (⋃ e) \leq \underset{f \in e}{\sum^{}} ({M ↾}_{S}) (f) \land \underset{f \in e}{\sum^{}} ({M ↾}_{S}) (f) \leq ({M ↾}_{S}) (⋃ e))$
113		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
114	19	ad2antrr	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to ({M ↾}_{S}) : S ⟶ [0, +∞]$
115	114 69	ffvelcdmd	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to ({M ↾}_{S}) (⋃ e) \in [0, +∞]$
116	113 115	sselid	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to ({M ↾}_{S}) (⋃ e) \in ℝ^{*}$
117	114	adantr	$⊢ (((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \land f \in e) \to ({M ↾}_{S}) : S ⟶ [0, +∞]$
118	117 76	ffvelcdmd	$⊢ (((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \land f \in e) \to ({M ↾}_{S}) (f) \in [0, +∞]$
119	118	ralrimiva	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to \forall f \in e ({M ↾}_{S}) (f) \in [0, +∞]$
120		nfcv	$⊢ \underline{Ⅎ} f e$
121	120	esumcl	$⊢ (e \in 𝒫 S \land \forall f \in e ({M ↾}_{S}) (f) \in [0, +∞]) \to \underset{f \in e}{\sum^{*}} ({M ↾}_{S}) (f) \in [0, +∞]$
122	33 119 121	syl2anc	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to \underset{f \in e}{\sum^{*}} ({M ↾}_{S}) (f) \in [0, +∞]$
123	113 122	sselid	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to \underset{f \in e}{\sum^{}} ({M ↾}_{S}) (f) \in ℝ^{}$
124		xrletri3	$⊢ (({M ↾}_{S}) (⋃ e) \in ℝ^{} \land \underset{f \in e}{\sum^{}} ({M ↾}_{S}) (f) \in ℝ^{}) \to (({M ↾}_{S}) (⋃ e) = \underset{f \in e}{\sum^{}} ({M ↾}_{S}) (f) \leftrightarrow (({M ↾}_{S}) (⋃ e) \leq \underset{f \in e}{\sum^{}} ({M ↾}_{S}) (f) \land \underset{f \in e}{\sum^{}} ({M ↾}_{S}) (f) \leq ({M ↾}_{S}) (⋃ e)))$
125	116 123 124	syl2anc	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to (({M ↾}_{S}) (⋃ e) = \underset{f \in e}{\sum^{}} ({M ↾}_{S}) (f) \leftrightarrow (({M ↾}_{S}) (⋃ e) \leq \underset{f \in e}{\sum^{}} ({M ↾}_{S}) (f) \land \underset{f \in e}{\sum^{*}} ({M ↾}_{S}) (f) \leq ({M ↾}_{S}) (⋃ e)))$
126	112 125	mpbird	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{g \in e}{Disj} g)) \to ({M ↾}_{S}) (⋃ e) = \underset{f \in e}{\sum^{*}} ({M ↾}_{S}) (f)$
127	30 126	sylan2b	$⊢ ((φ \land e \in 𝒫 S) \land (e ≼ ω \land \underset{f \in e}{Disj} f)) \to ({M ↾}_{S}) (⋃ e) = \underset{f \in e}{\sum^{*}} ({M ↾}_{S}) (f)$
128	127	ex	$⊢ (φ \land e \in 𝒫 S) \to ((e ≼ ω \land \underset{f \in e}{Disj} f) \to ({M ↾}_{S}) (⋃ e) = \underset{f \in e}{\sum^{*}} ({M ↾}_{S}) (f))$
129	128	ralrimiva	$⊢ φ \to \forall e \in 𝒫 S ((e ≼ ω \land \underset{f \in e}{Disj} f) \to ({M ↾}_{S}) (⋃ e) = \underset{f \in e}{\sum^{*}} ({M ↾}_{S}) (f))$
130	19 25 129	3jca	$⊢ φ \to (({M ↾}_{S}) : S ⟶ [0, +∞] \land ({M ↾}_{S}) (\emptyset) = 0 \land \forall e \in 𝒫 S ((e ≼ ω \land \underset{f \in e}{Disj} f) \to ({M ↾}_{S}) (⋃ e) = \underset{f \in e}{\sum^{*}} ({M ↾}_{S}) (f)))$
131	16 15 20 54 62	carsgsiga	$⊢ φ \to toCaraSiga (M) \in sigAlgebra (⋃ Q)$
132	2 131	eqeltrid	$⊢ φ \to S \in sigAlgebra (⋃ Q)$
133		elrnsiga	$⊢ S \in sigAlgebra (⋃ Q) \to S \in ⋃ ran sigAlgebra$
134		ismeas	$⊢ S \in ⋃ ran sigAlgebra \to ({M ↾}_{S} \in measures (S) \leftrightarrow (({M ↾}_{S}) : S ⟶ [0, +∞] \land ({M ↾}_{S}) (\emptyset) = 0 \land \forall e \in 𝒫 S ((e ≼ ω \land \underset{f \in e}{Disj} f) \to ({M ↾}_{S}) (⋃ e) = \underset{f \in e}{\sum^{*}} ({M ↾}_{S}) (f))))$
135	132 133 134	3syl	$⊢ φ \to ({M ↾}_{S} \in measures (S) \leftrightarrow (({M ↾}_{S}) : S ⟶ [0, +∞] \land ({M ↾}_{S}) (\emptyset) = 0 \land \forall e \in 𝒫 S ((e ≼ ω \land \underset{f \in e}{Disj} f) \to ({M ↾}_{S}) (⋃ e) = \underset{f \in e}{\sum^{*}} ({M ↾}_{S}) (f))))$
136	130 135	mpbird	$⊢ φ \to {M ↾}_{S} \in measures (S)$

Metamath Proof Explorer

Theorem omsmeas

Proof