ismeannd

Description: Sufficient condition to prove that M is a measure. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	ismeannd.sal	$⊢ φ \to S \in SAlg$
	ismeannd.mf	$⊢ φ \to M : S ⟶ [0, +∞]$
	ismeannd.m0	$⊢ φ \to M (\emptyset) = 0$
	ismeannd.iun	$⊢ (φ \land e : ℕ ⟶ S \land \underset{n \in ℕ}{Disj} e (n)) \to M (⋃_{n \in ℕ} e (n)) = sum^((n \in ℕ ⟼ M (e (n))))$
Assertion	ismeannd	$⊢ φ \to M \in Meas$

Proof

Step	Hyp	Ref	Expression
1		ismeannd.sal	$⊢ φ \to S \in SAlg$
2		ismeannd.mf	$⊢ φ \to M : S ⟶ [0, +∞]$
3		ismeannd.m0	$⊢ φ \to M (\emptyset) = 0$
4		ismeannd.iun	$⊢ (φ \land e : ℕ ⟶ S \land \underset{n \in ℕ}{Disj} e (n)) \to M (⋃_{n \in ℕ} e (n)) = sum^((n \in ℕ ⟼ M (e (n))))$
5	2	fdmd	$⊢ φ \to dom M = S$
6	5	feq2d	$⊢ φ \to (M : dom M ⟶ [0, +∞] \leftrightarrow M : S ⟶ [0, +∞])$
7	2 6	mpbird	$⊢ φ \to M : dom M ⟶ [0, +∞]$
8	5 1	eqeltrd	$⊢ φ \to dom M \in SAlg$
9	7 8	jca	$⊢ φ \to (M : dom M ⟶ [0, +∞] \land dom M \in SAlg)$
10		unieq	$⊢ x = \emptyset \to ⋃ x = ⋃ \emptyset$
11		uni0	$⊢ ⋃ \emptyset = \emptyset$
12	11	a1i	$⊢ x = \emptyset \to ⋃ \emptyset = \emptyset$
13	10 12	eqtrd	$⊢ x = \emptyset \to ⋃ x = \emptyset$
14	13	fveq2d	$⊢ x = \emptyset \to M (⋃ x) = M (\emptyset)$
15	14 3	sylan9eqr	$⊢ (φ \land x = \emptyset) \to M (⋃ x) = 0$
16		reseq2	$⊢ x = \emptyset \to {M ↾}_{x} = {M ↾}_{\emptyset}$
17		res0	$⊢ {M ↾}_{\emptyset} = \emptyset$
18	17	a1i	$⊢ x = \emptyset \to {M ↾}_{\emptyset} = \emptyset$
19	16 18	eqtrd	$⊢ x = \emptyset \to {M ↾}_{x} = \emptyset$
20	19	fveq2d	$⊢ x = \emptyset \to sum^({M ↾}_{x}) = sum^(\emptyset)$
21	20	adantl	$⊢ (φ \land x = \emptyset) \to sum^({M ↾}_{x}) = sum^(\emptyset)$
22		sge00	$⊢ sum^(\emptyset) = 0$
23	22	a1i	$⊢ (φ \land x = \emptyset) \to sum^(\emptyset) = 0$
24	21 23	eqtrd	$⊢ (φ \land x = \emptyset) \to sum^({M ↾}_{x}) = 0$
25	15 24	eqtr4d	$⊢ (φ \land x = \emptyset) \to M (⋃ x) = sum^({M ↾}_{x})$
26	25	adantlr	$⊢ ((φ \land x \in 𝒫 dom M) \land x = \emptyset) \to M (⋃ x) = sum^({M ↾}_{x})$
27	26	adantlr	$⊢ (((φ \land x \in 𝒫 dom M) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land x = \emptyset) \to M (⋃ x) = sum^({M ↾}_{x})$
28		simpll	$⊢ (((φ \land x \in 𝒫 dom M) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land \neg x = \emptyset) \to (φ \land x \in 𝒫 dom M)$
29		simplrr	$⊢ (((φ \land x \in 𝒫 dom M) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land \neg x = \emptyset) \to \underset{y \in x}{Disj} y$
30	28 29	jca	$⊢ (((φ \land x \in 𝒫 dom M) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land \neg x = \emptyset) \to ((φ \land x \in 𝒫 dom M) \land \underset{y \in x}{Disj} y)$
31		simplrl	$⊢ (((φ \land x \in 𝒫 dom M) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land \neg x = \emptyset) \to x ≼ ω$
32		neqne	$⊢ \neg x = \emptyset \to x \neq \emptyset$
33	32	adantl	$⊢ (((φ \land x \in 𝒫 dom M) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land \neg x = \emptyset) \to x \neq \emptyset$
34		id	$⊢ y = w \to y = w$
35	34	cbvdisjv	$⊢ \underset{y \in x}{Disj} y \leftrightarrow \underset{w \in x}{Disj} w$
36	35	bilani	$⊢ (x ≼ ω \land \underset{y \in x}{Disj} y) \to \underset{w \in x}{Disj} w$
37	36	ad2antlr	$⊢ (((φ \land x \in 𝒫 dom M) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land \neg x = \emptyset) \to \underset{w \in x}{Disj} w$
38	31 33 37	nnfoctbdj	$⊢ (((φ \land x \in 𝒫 dom M) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land \neg x = \emptyset) \to \exists e (e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\} \land \underset{n \in ℕ}{Disj} e (n))$
39		simpl	$⊢ (((φ \land x \in 𝒫 dom M) \land \underset{y \in x}{Disj} y) \land (e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\} \land \underset{n \in ℕ}{Disj} e (n))) \to ((φ \land x \in 𝒫 dom M) \land \underset{y \in x}{Disj} y)$
40		simprl	$⊢ (((φ \land x \in 𝒫 dom M) \land \underset{y \in x}{Disj} y) \land (e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\} \land \underset{n \in ℕ}{Disj} e (n))) \to e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}$
41		simprr	$⊢ (((φ \land x \in 𝒫 dom M) \land \underset{y \in x}{Disj} y) \land (e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\} \land \underset{n \in ℕ}{Disj} e (n))) \to \underset{n \in ℕ}{Disj} e (n)$
42		founiiun0	$⊢ e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\} \to ⋃ x = ⋃_{n \in ℕ} e (n)$
43	42	fveq2d	$⊢ e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\} \to M (⋃ x) = M (⋃_{n \in ℕ} e (n))$
44	43	ad2antlr	$⊢ ((((φ \land x \in 𝒫 dom M) \land \underset{y \in x}{Disj} y) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n)) \to M (⋃ x) = M (⋃_{n \in ℕ} e (n))$
45		simplll	$⊢ (((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n)) \to φ$
46		fof	$⊢ e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\} \to e : ℕ ⟶ x \cup \{\emptyset\}$
47	46	adantl	$⊢ ((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \to e : ℕ ⟶ x \cup \{\emptyset\}$
48		elpwi	$⊢ x \in 𝒫 dom M \to x \subseteq dom M$
49	48	adantl	$⊢ (φ \land x \in 𝒫 dom M) \to x \subseteq dom M$
50	5	adantr	$⊢ (φ \land x \in 𝒫 dom M) \to dom M = S$
51	49 50	sseqtrd	$⊢ (φ \land x \in 𝒫 dom M) \to x \subseteq S$
52		0sal	$⊢ S \in SAlg \to \emptyset \in S$
53	1 52	syl	$⊢ φ \to \emptyset \in S$
54		snssi	$⊢ \emptyset \in S \to \{\emptyset\} \subseteq S$
55	53 54	syl	$⊢ φ \to \{\emptyset\} \subseteq S$
56	55	adantr	$⊢ (φ \land x \in 𝒫 dom M) \to \{\emptyset\} \subseteq S$
57	51 56	unssd	$⊢ (φ \land x \in 𝒫 dom M) \to x \cup \{\emptyset\} \subseteq S$
58	57	adantr	$⊢ ((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \to x \cup \{\emptyset\} \subseteq S$
59	47 58	fssd	$⊢ ((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \to e : ℕ ⟶ S$
60	59	adantr	$⊢ (((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n)) \to e : ℕ ⟶ S$
61		simpr	$⊢ (((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n)) \to \underset{n \in ℕ}{Disj} e (n)$
62	45 60 61 4	syl3anc	$⊢ (((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n)) \to M (⋃_{n \in ℕ} e (n)) = sum^((n \in ℕ ⟼ M (e (n))))$
63	62	adantllr	$⊢ ((((φ \land x \in 𝒫 dom M) \land \underset{y \in x}{Disj} y) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n)) \to M (⋃_{n \in ℕ} e (n)) = sum^((n \in ℕ ⟼ M (e (n))))$
64	2	feqmptd	$⊢ φ \to M = (y \in S ⟼ M (y))$
65	64	reseq1d	$⊢ φ \to {M ↾}_{x} = {(y \in S ⟼ M (y)) ↾}_{x}$
66	65	adantr	$⊢ (φ \land x \in 𝒫 dom M) \to {M ↾}_{x} = {(y \in S ⟼ M (y)) ↾}_{x}$
67	66	adantr	$⊢ ((φ \land x \in 𝒫 dom M) \land \emptyset \in x) \to {M ↾}_{x} = {(y \in S ⟼ M (y)) ↾}_{x}$
68	51	resmptd	$⊢ (φ \land x \in 𝒫 dom M) \to {(y \in S ⟼ M (y)) ↾}_{x} = (y \in x ⟼ M (y))$
69	68	adantr	$⊢ ((φ \land x \in 𝒫 dom M) \land \emptyset \in x) \to {(y \in S ⟼ M (y)) ↾}_{x} = (y \in x ⟼ M (y))$
70		snssi	$⊢ \emptyset \in x \to \{\emptyset\} \subseteq x$
71		ssequn2	$⊢ \{\emptyset\} \subseteq x \leftrightarrow x \cup \{\emptyset\} = x$
72	70 71	sylib	$⊢ \emptyset \in x \to x \cup \{\emptyset\} = x$
73	72	eqcomd	$⊢ \emptyset \in x \to x = x \cup \{\emptyset\}$
74	73	mpteq1d	$⊢ \emptyset \in x \to (y \in x ⟼ M (y)) = (y \in (x \cup \{\emptyset\}) ⟼ M (y))$
75	74	adantl	$⊢ ((φ \land x \in 𝒫 dom M) \land \emptyset \in x) \to (y \in x ⟼ M (y)) = (y \in (x \cup \{\emptyset\}) ⟼ M (y))$
76	67 69 75	3eqtrd	$⊢ ((φ \land x \in 𝒫 dom M) \land \emptyset \in x) \to {M ↾}_{x} = (y \in (x \cup \{\emptyset\}) ⟼ M (y))$
77	76	fveq2d	$⊢ ((φ \land x \in 𝒫 dom M) \land \emptyset \in x) \to sum^({M ↾}_{x}) = sum^((y \in (x \cup \{\emptyset\}) ⟼ M (y)))$
78		nfv	$⊢ Ⅎ y ((φ \land x \in 𝒫 dom M) \land \neg \emptyset \in x)$
79		simplr	$⊢ ((φ \land x \in 𝒫 dom M) \land \neg \emptyset \in x) \to x \in 𝒫 dom M$
80		p0ex	$⊢ \{\emptyset\} \in V$
81	80	a1i	$⊢ ((φ \land x \in 𝒫 dom M) \land \neg \emptyset \in x) \to \{\emptyset\} \in V$
82		disjsn	$⊢ x \cap \{\emptyset\} = \emptyset \leftrightarrow \neg \emptyset \in x$
83	82	bilanri	$⊢ ((φ \land x \in 𝒫 dom M) \land \neg \emptyset \in x) \to x \cap \{\emptyset\} = \emptyset$
84	2	ad2antrr	$⊢ ((φ \land x \in 𝒫 dom M) \land y \in x) \to M : S ⟶ [0, +∞]$
85	51	sselda	$⊢ ((φ \land x \in 𝒫 dom M) \land y \in x) \to y \in S$
86	84 85	ffvelcdmd	$⊢ ((φ \land x \in 𝒫 dom M) \land y \in x) \to M (y) \in [0, +∞]$
87	86	adantlr	$⊢ (((φ \land x \in 𝒫 dom M) \land \neg \emptyset \in x) \land y \in x) \to M (y) \in [0, +∞]$
88		elsni	$⊢ y \in \{\emptyset\} \to y = \emptyset$
89	88	fveq2d	$⊢ y \in \{\emptyset\} \to M (y) = M (\emptyset)$
90	89	adantl	$⊢ (φ \land y \in \{\emptyset\}) \to M (y) = M (\emptyset)$
91	2 53	ffvelcdmd	$⊢ φ \to M (\emptyset) \in [0, +∞]$
92	91	adantr	$⊢ (φ \land y \in \{\emptyset\}) \to M (\emptyset) \in [0, +∞]$
93	90 92	eqeltrd	$⊢ (φ \land y \in \{\emptyset\}) \to M (y) \in [0, +∞]$
94	93	ad4ant14	$⊢ (((φ \land x \in 𝒫 dom M) \land \neg \emptyset \in x) \land y \in \{\emptyset\}) \to M (y) \in [0, +∞]$
95	78 79 81 83 87 94	sge0splitmpt	$⊢ ((φ \land x \in 𝒫 dom M) \land \neg \emptyset \in x) \to sum^((y \in (x \cup \{\emptyset\}) ⟼ M (y))) = sum^((y \in x ⟼ M (y))) +_{𝑒} sum^((y \in \{\emptyset\} ⟼ M (y)))$
96		fveq2	$⊢ y = \emptyset \to M (y) = M (\emptyset)$
97	96	adantl	$⊢ (φ \land y = \emptyset) \to M (y) = M (\emptyset)$
98	3	adantr	$⊢ (φ \land y = \emptyset) \to M (\emptyset) = 0$
99	97 98	eqtrd	$⊢ (φ \land y = \emptyset) \to M (y) = 0$
100	88 99	sylan2	$⊢ (φ \land y \in \{\emptyset\}) \to M (y) = 0$
101	100	mpteq2dva	$⊢ φ \to (y \in \{\emptyset\} ⟼ M (y)) = (y \in \{\emptyset\} ⟼ 0)$
102	101	fveq2d	$⊢ φ \to sum^((y \in \{\emptyset\} ⟼ M (y))) = sum^((y \in \{\emptyset\} ⟼ 0))$
103		nfv	$⊢ Ⅎ y φ$
104	80	a1i	$⊢ φ \to \{\emptyset\} \in V$
105	103 104	sge0z	$⊢ φ \to sum^((y \in \{\emptyset\} ⟼ 0)) = 0$
106	102 105	eqtrd	$⊢ φ \to sum^((y \in \{\emptyset\} ⟼ M (y))) = 0$
107	106	oveq2d	$⊢ φ \to sum^((y \in x ⟼ M (y))) +_{𝑒} sum^((y \in \{\emptyset\} ⟼ M (y))) = sum^((y \in x ⟼ M (y))) +_{𝑒} 0$
108	107	ad2antrr	$⊢ ((φ \land x \in 𝒫 dom M) \land \neg \emptyset \in x) \to sum^((y \in x ⟼ M (y))) +_{𝑒} sum^((y \in \{\emptyset\} ⟼ M (y))) = sum^((y \in x ⟼ M (y))) +_{𝑒} 0$
109		simpr	$⊢ (φ \land x \in 𝒫 dom M) \to x \in 𝒫 dom M$
110	66 68	eqtrd	$⊢ (φ \land x \in 𝒫 dom M) \to {M ↾}_{x} = (y \in x ⟼ M (y))$
111	2	adantr	$⊢ (φ \land x \in 𝒫 dom M) \to M : S ⟶ [0, +∞]$
112	111 51	fssresd	$⊢ (φ \land x \in 𝒫 dom M) \to ({M ↾}_{x}) : x ⟶ [0, +∞]$
113	110 112	feq1dd	$⊢ (φ \land x \in 𝒫 dom M) \to (y \in x ⟼ M (y)) : x ⟶ [0, +∞]$
114	109 113	sge0xrcl	$⊢ (φ \land x \in 𝒫 dom M) \to sum^((y \in x ⟼ M (y))) \in ℝ^{*}$
115	114	xaddridd	$⊢ (φ \land x \in 𝒫 dom M) \to sum^((y \in x ⟼ M (y))) +_{𝑒} 0 = sum^((y \in x ⟼ M (y)))$
116	110	fveq2d	$⊢ (φ \land x \in 𝒫 dom M) \to sum^({M ↾}_{x}) = sum^((y \in x ⟼ M (y)))$
117	116	eqcomd	$⊢ (φ \land x \in 𝒫 dom M) \to sum^((y \in x ⟼ M (y))) = sum^({M ↾}_{x})$
118	115 117	eqtrd	$⊢ (φ \land x \in 𝒫 dom M) \to sum^((y \in x ⟼ M (y))) +_{𝑒} 0 = sum^({M ↾}_{x})$
119	118	adantr	$⊢ ((φ \land x \in 𝒫 dom M) \land \neg \emptyset \in x) \to sum^((y \in x ⟼ M (y))) +_{𝑒} 0 = sum^({M ↾}_{x})$
120	95 108 119	3eqtrrd	$⊢ ((φ \land x \in 𝒫 dom M) \land \neg \emptyset \in x) \to sum^({M ↾}_{x}) = sum^((y \in (x \cup \{\emptyset\}) ⟼ M (y)))$
121	77 120	pm2.61dan	$⊢ (φ \land x \in 𝒫 dom M) \to sum^({M ↾}_{x}) = sum^((y \in (x \cup \{\emptyset\}) ⟼ M (y)))$
122	121	ad2antrr	$⊢ (((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n)) \to sum^({M ↾}_{x}) = sum^((y \in (x \cup \{\emptyset\}) ⟼ M (y)))$
123		nfv	$⊢ Ⅎ y (((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n))$
124		nfv	$⊢ Ⅎ n ((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\})$
125		nfdisj1	$⊢ Ⅎ n \underset{n \in ℕ}{Disj} e (n)$
126	124 125	nfan	$⊢ Ⅎ n (((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n))$
127		fveq2	$⊢ y = e (n) \to M (y) = M (e (n))$
128		nnex	$⊢ ℕ \in V$
129	128	a1i	$⊢ (((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n)) \to ℕ \in V$
130		simplr	$⊢ (((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n)) \to e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}$
131		eqidd	$⊢ ((((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n)) \land n \in ℕ) \to e (n) = e (n)$
132	2	ad2antrr	$⊢ ((φ \land x \in 𝒫 dom M) \land y \in (x \cup \{\emptyset\})) \to M : S ⟶ [0, +∞]$
133	57	sselda	$⊢ ((φ \land x \in 𝒫 dom M) \land y \in (x \cup \{\emptyset\})) \to y \in S$
134	132 133	ffvelcdmd	$⊢ ((φ \land x \in 𝒫 dom M) \land y \in (x \cup \{\emptyset\})) \to M (y) \in [0, +∞]$
135	134	ad4ant14	$⊢ ((((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n)) \land y \in (x \cup \{\emptyset\})) \to M (y) \in [0, +∞]$
136	45 99	sylan	$⊢ ((((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n)) \land y = \emptyset) \to M (y) = 0$
137	123 126 127 129 130 61 131 135 136	sge0fodjrn	$⊢ (((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n)) \to sum^((y \in (x \cup \{\emptyset\}) ⟼ M (y))) = sum^((n \in ℕ ⟼ M (e (n))))$
138	122 137	eqtr2d	$⊢ (((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n)) \to sum^((n \in ℕ ⟼ M (e (n)))) = sum^({M ↾}_{x})$
139	138	adantllr	$⊢ ((((φ \land x \in 𝒫 dom M) \land \underset{y \in x}{Disj} y) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n)) \to sum^((n \in ℕ ⟼ M (e (n)))) = sum^({M ↾}_{x})$
140	44 63 139	3eqtrd	$⊢ ((((φ \land x \in 𝒫 dom M) \land \underset{y \in x}{Disj} y) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n)) \to M (⋃ x) = sum^({M ↾}_{x})$
141	39 40 41 140	syl21anc	$⊢ (((φ \land x \in 𝒫 dom M) \land \underset{y \in x}{Disj} y) \land (e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\} \land \underset{n \in ℕ}{Disj} e (n))) \to M (⋃ x) = sum^({M ↾}_{x})$
142	141	ex	$⊢ ((φ \land x \in 𝒫 dom M) \land \underset{y \in x}{Disj} y) \to ((e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\} \land \underset{n \in ℕ}{Disj} e (n)) \to M (⋃ x) = sum^({M ↾}_{x}))$
143	142	exlimdv	$⊢ ((φ \land x \in 𝒫 dom M) \land \underset{y \in x}{Disj} y) \to (\exists e (e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\} \land \underset{n \in ℕ}{Disj} e (n)) \to M (⋃ x) = sum^({M ↾}_{x}))$
144	30 38 143	sylc	$⊢ (((φ \land x \in 𝒫 dom M) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land \neg x = \emptyset) \to M (⋃ x) = sum^({M ↾}_{x})$
145	27 144	pm2.61dan	$⊢ ((φ \land x \in 𝒫 dom M) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to M (⋃ x) = sum^({M ↾}_{x})$
146	145	ex	$⊢ (φ \land x \in 𝒫 dom M) \to ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = sum^({M ↾}_{x}))$
147	146	ralrimiva	$⊢ φ \to \forall x \in 𝒫 dom M ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = sum^({M ↾}_{x}))$
148	9 3 147	jca31	$⊢ φ \to (((M : dom M ⟶ [0, +∞] \land dom M \in SAlg) \land M (\emptyset) = 0) \land \forall x \in 𝒫 dom M ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = sum^({M ↾}_{x})))$
149		ismea	$⊢ M \in Meas \leftrightarrow (((M : dom M ⟶ [0, +∞] \land dom M \in SAlg) \land M (\emptyset) = 0) \land \forall x \in 𝒫 dom M ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = sum^({M ↾}_{x})))$
150	148 149	sylibr	$⊢ φ \to M \in Meas$

Metamath Proof Explorer

Theorem ismeannd

Proof