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	biimpi	$⊢ \underset{y \in x}{Disj} y \to \underset{w \in x}{Disj} w$
37	36	adantl	$⊢ (x ≼ ω \land \underset{y \in x}{Disj} y) \to \underset{w \in x}{Disj} w$
38	37	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$
39	31 33 38	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))$
40		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)$
41		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\}$
42		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)$
43		founiiun0	$⊢ e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\} \to ⋃ x = ⋃_{n \in ℕ} e (n)$
44	43	fveq2d	$⊢ e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\} \to M (⋃ x) = M (⋃_{n \in ℕ} e (n))$
45	44	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))$
46		simplll	$⊢ (((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n)) \to φ$
47		fof	$⊢ e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\} \to e : ℕ ⟶ x \cup \{\emptyset\}$
48	47	adantl	$⊢ ((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \to e : ℕ ⟶ x \cup \{\emptyset\}$
49		elpwi	$⊢ x \in 𝒫 dom M \to x \subseteq dom M$
50	49	adantl	$⊢ (φ \land x \in 𝒫 dom M) \to x \subseteq dom M$
51	5	adantr	$⊢ (φ \land x \in 𝒫 dom M) \to dom M = S$
52	50 51	sseqtrd	$⊢ (φ \land x \in 𝒫 dom M) \to x \subseteq S$
53		0sal	$⊢ S \in SAlg \to \emptyset \in S$
54	1 53	syl	$⊢ φ \to \emptyset \in S$
55		snssi	$⊢ \emptyset \in S \to \{\emptyset\} \subseteq S$
56	54 55	syl	$⊢ φ \to \{\emptyset\} \subseteq S$
57	56	adantr	$⊢ (φ \land x \in 𝒫 dom M) \to \{\emptyset\} \subseteq S$
58	52 57	unssd	$⊢ (φ \land x \in 𝒫 dom M) \to x \cup \{\emptyset\} \subseteq S$
59	58	adantr	$⊢ ((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \to x \cup \{\emptyset\} \subseteq S$
60	48 59	fssd	$⊢ ((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \to e : ℕ ⟶ S$
61	60	adantr	$⊢ (((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n)) \to e : ℕ ⟶ S$
62		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)$
63	46 61 62 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))))$
64	63	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))))$
65	2	feqmptd	$⊢ φ \to M = (y \in S ⟼ M (y))$
66	65	reseq1d	$⊢ φ \to {M ↾}_{x} = {(y \in S ⟼ M (y)) ↾}_{x}$
67	66	adantr	$⊢ (φ \land x \in 𝒫 dom M) \to {M ↾}_{x} = {(y \in S ⟼ M (y)) ↾}_{x}$
68	67	adantr	$⊢ ((φ \land x \in 𝒫 dom M) \land \emptyset \in x) \to {M ↾}_{x} = {(y \in S ⟼ M (y)) ↾}_{x}$
69	52	resmptd	$⊢ (φ \land x \in 𝒫 dom M) \to {(y \in S ⟼ M (y)) ↾}_{x} = (y \in x ⟼ M (y))$
70	69	adantr	$⊢ ((φ \land x \in 𝒫 dom M) \land \emptyset \in x) \to {(y \in S ⟼ M (y)) ↾}_{x} = (y \in x ⟼ M (y))$
71		snssi	$⊢ \emptyset \in x \to \{\emptyset\} \subseteq x$
72		ssequn2	$⊢ \{\emptyset\} \subseteq x \leftrightarrow x \cup \{\emptyset\} = x$
73	71 72	sylib	$⊢ \emptyset \in x \to x \cup \{\emptyset\} = x$
74	73	eqcomd	$⊢ \emptyset \in x \to x = x \cup \{\emptyset\}$
75	74	mpteq1d	$⊢ \emptyset \in x \to (y \in x ⟼ M (y)) = (y \in (x \cup \{\emptyset\}) ⟼ M (y))$
76	75	adantl	$⊢ ((φ \land x \in 𝒫 dom M) \land \emptyset \in x) \to (y \in x ⟼ M (y)) = (y \in (x \cup \{\emptyset\}) ⟼ M (y))$
77	68 70 76	3eqtrd	$⊢ ((φ \land x \in 𝒫 dom M) \land \emptyset \in x) \to {M ↾}_{x} = (y \in (x \cup \{\emptyset\}) ⟼ M (y))$
78	77	fveq2d	$⊢ ((φ \land x \in 𝒫 dom M) \land \emptyset \in x) \to sum^({M ↾}_{x}) = sum^((y \in (x \cup \{\emptyset\}) ⟼ M (y)))$
79		nfv	$⊢ Ⅎ y ((φ \land x \in 𝒫 dom M) \land \neg \emptyset \in x)$
80		simplr	$⊢ ((φ \land x \in 𝒫 dom M) \land \neg \emptyset \in x) \to x \in 𝒫 dom M$
81		p0ex	$⊢ \{\emptyset\} \in V$
82	81	a1i	$⊢ ((φ \land x \in 𝒫 dom M) \land \neg \emptyset \in x) \to \{\emptyset\} \in V$
83		disjsn	$⊢ x \cap \{\emptyset\} = \emptyset \leftrightarrow \neg \emptyset \in x$
84	83	biimpri	$⊢ \neg \emptyset \in x \to x \cap \{\emptyset\} = \emptyset$
85	84	adantl	$⊢ ((φ \land x \in 𝒫 dom M) \land \neg \emptyset \in x) \to x \cap \{\emptyset\} = \emptyset$
86	2	ad2antrr	$⊢ ((φ \land x \in 𝒫 dom M) \land y \in x) \to M : S ⟶ [0, +∞]$
87	52	sselda	$⊢ ((φ \land x \in 𝒫 dom M) \land y \in x) \to y \in S$
88	86 87	ffvelrnd	$⊢ ((φ \land x \in 𝒫 dom M) \land y \in x) \to M (y) \in [0, +∞]$
89	88	adantlr	$⊢ (((φ \land x \in 𝒫 dom M) \land \neg \emptyset \in x) \land y \in x) \to M (y) \in [0, +∞]$
90		elsni	$⊢ y \in \{\emptyset\} \to y = \emptyset$
91	90	fveq2d	$⊢ y \in \{\emptyset\} \to M (y) = M (\emptyset)$
92	91	adantl	$⊢ (φ \land y \in \{\emptyset\}) \to M (y) = M (\emptyset)$
93	2 54	ffvelrnd	$⊢ φ \to M (\emptyset) \in [0, +∞]$
94	93	adantr	$⊢ (φ \land y \in \{\emptyset\}) \to M (\emptyset) \in [0, +∞]$
95	92 94	eqeltrd	$⊢ (φ \land y \in \{\emptyset\}) \to M (y) \in [0, +∞]$
96	95	ad4ant14	$⊢ (((φ \land x \in 𝒫 dom M) \land \neg \emptyset \in x) \land y \in \{\emptyset\}) \to M (y) \in [0, +∞]$
97	79 80 82 85 89 96	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)))$
98		fveq2	$⊢ y = \emptyset \to M (y) = M (\emptyset)$
99	98	adantl	$⊢ (φ \land y = \emptyset) \to M (y) = M (\emptyset)$
100	3	adantr	$⊢ (φ \land y = \emptyset) \to M (\emptyset) = 0$
101	99 100	eqtrd	$⊢ (φ \land y = \emptyset) \to M (y) = 0$
102	90 101	sylan2	$⊢ (φ \land y \in \{\emptyset\}) \to M (y) = 0$
103	102	mpteq2dva	$⊢ φ \to (y \in \{\emptyset\} ⟼ M (y)) = (y \in \{\emptyset\} ⟼ 0)$
104	103	fveq2d	$⊢ φ \to sum^((y \in \{\emptyset\} ⟼ M (y))) = sum^((y \in \{\emptyset\} ⟼ 0))$
105		nfv	$⊢ Ⅎ y φ$
106	81	a1i	$⊢ φ \to \{\emptyset\} \in V$
107	105 106	sge0z	$⊢ φ \to sum^((y \in \{\emptyset\} ⟼ 0)) = 0$
108	104 107	eqtrd	$⊢ φ \to sum^((y \in \{\emptyset\} ⟼ M (y))) = 0$
109	108	oveq2d	$⊢ φ \to sum^((y \in x ⟼ M (y))) +_{𝑒} sum^((y \in \{\emptyset\} ⟼ M (y))) = sum^((y \in x ⟼ M (y))) +_{𝑒} 0$
110	109	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$
111		simpr	$⊢ (φ \land x \in 𝒫 dom M) \to x \in 𝒫 dom M$
112	67 69	eqtrd	$⊢ (φ \land x \in 𝒫 dom M) \to {M ↾}_{x} = (y \in x ⟼ M (y))$
113	2	adantr	$⊢ (φ \land x \in 𝒫 dom M) \to M : S ⟶ [0, +∞]$
114	113 52	fssresd	$⊢ (φ \land x \in 𝒫 dom M) \to ({M ↾}_{x}) : x ⟶ [0, +∞]$
115	112 114	feq1dd	$⊢ (φ \land x \in 𝒫 dom M) \to (y \in x ⟼ M (y)) : x ⟶ [0, +∞]$
116	111 115	sge0xrcl	$⊢ (φ \land x \in 𝒫 dom M) \to sum^((y \in x ⟼ M (y))) \in ℝ^{*}$
117	116	xaddid1d	$⊢ (φ \land x \in 𝒫 dom M) \to sum^((y \in x ⟼ M (y))) +_{𝑒} 0 = sum^((y \in x ⟼ M (y)))$
118	112	fveq2d	$⊢ (φ \land x \in 𝒫 dom M) \to sum^({M ↾}_{x}) = sum^((y \in x ⟼ M (y)))$
119	118	eqcomd	$⊢ (φ \land x \in 𝒫 dom M) \to sum^((y \in x ⟼ M (y))) = sum^({M ↾}_{x})$
120	117 119	eqtrd	$⊢ (φ \land x \in 𝒫 dom M) \to sum^((y \in x ⟼ M (y))) +_{𝑒} 0 = sum^({M ↾}_{x})$
121	120	adantr	$⊢ ((φ \land x \in 𝒫 dom M) \land \neg \emptyset \in x) \to sum^((y \in x ⟼ M (y))) +_{𝑒} 0 = sum^({M ↾}_{x})$
122	97 110 121	3eqtrrd	$⊢ ((φ \land x \in 𝒫 dom M) \land \neg \emptyset \in x) \to sum^({M ↾}_{x}) = sum^((y \in (x \cup \{\emptyset\}) ⟼ M (y)))$
123	78 122	pm2.61dan	$⊢ (φ \land x \in 𝒫 dom M) \to sum^({M ↾}_{x}) = sum^((y \in (x \cup \{\emptyset\}) ⟼ M (y)))$
124	123	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)))$
125		nfv	$⊢ Ⅎ y (((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n))$
126		nfv	$⊢ Ⅎ n ((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\})$
127		nfdisj1	$⊢ Ⅎ n \underset{n \in ℕ}{Disj} e (n)$
128	126 127	nfan	$⊢ Ⅎ n (((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n))$
129		fveq2	$⊢ y = e (n) \to M (y) = M (e (n))$
130		nnex	$⊢ ℕ \in V$
131	130	a1i	$⊢ (((φ \land x \in 𝒫 dom M) \land e : ℕ \underset{onto}{⟶} x \cup \{\emptyset\}) \land \underset{n \in ℕ}{Disj} e (n)) \to ℕ \in V$
132		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\}$
133		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)$
134	2	ad2antrr	$⊢ ((φ \land x \in 𝒫 dom M) \land y \in (x \cup \{\emptyset\})) \to M : S ⟶ [0, +∞]$
135	58	sselda	$⊢ ((φ \land x \in 𝒫 dom M) \land y \in (x \cup \{\emptyset\})) \to y \in S$
136	134 135	ffvelrnd	$⊢ ((φ \land x \in 𝒫 dom M) \land y \in (x \cup \{\emptyset\})) \to M (y) \in [0, +∞]$
137	136	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, +∞]$
138	46 101	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$
139	125 128 129 131 132 62 133 137 138	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))))$
140	124 139	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})$
141	140	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})$
142	45 64 141	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})$
143	40 41 42 142	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})$
144	143	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}))$
145	144	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}))$
146	30 39 145	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})$
147	27 146	pm2.61dan	$⊢ ((φ \land x \in 𝒫 dom M) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to M (⋃ x) = sum^({M ↾}_{x})$
148	147	ex	$⊢ (φ \land x \in 𝒫 dom M) \to ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = sum^({M ↾}_{x}))$
149	148	ralrimiva	$⊢ φ \to \forall x \in 𝒫 dom M ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = sum^({M ↾}_{x}))$
150	9 3 149	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})))$
151		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})))$
152	150 151	sylibr	$⊢ φ \to M \in Meas$

Metamath Proof Explorer

Theorem ismeannd

Proof