meaiuninclem

Description: Measures are continuous from below (bounded case): if E is a sequence of increasing measurable sets (with uniformly bounded measure) then the measure of the union is the union of the measure. This is Proposition 112C (e) of Fremlin1 p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	meaiuninclem.m	$⊢ φ \to M \in Meas$
	meaiuninclem.n	$⊢ φ \to N \in ℤ$
	meaiuninclem.z	$⊢ Z = ℤ_{\geq N}$
	meaiuninclem.e	$⊢ φ \to E : Z ⟶ dom M$
	meaiuninclem.i	$⊢ (φ \land n \in Z) \to E (n) \subseteq E (n + 1)$
	meaiuninclem.b	$⊢ φ \to \exists x \in ℝ \forall n \in Z M (E (n)) \leq x$
	meaiuninclem.s	$⊢ S = (n \in Z ⟼ M (E (n)))$
	meaiuninclem.f	$⊢ F = (n \in Z ⟼ E (n) ∖ ⋃_{i \in (N ..^n)} E (i))$
Assertion	meaiuninclem	$⊢ φ \to S ⇝ M (⋃_{n \in Z} E (n))$

Proof

Step	Hyp	Ref	Expression
1		meaiuninclem.m	$⊢ φ \to M \in Meas$
2		meaiuninclem.n	$⊢ φ \to N \in ℤ$
3		meaiuninclem.z	$⊢ Z = ℤ_{\geq N}$
4		meaiuninclem.e	$⊢ φ \to E : Z ⟶ dom M$
5		meaiuninclem.i	$⊢ (φ \land n \in Z) \to E (n) \subseteq E (n + 1)$
6		meaiuninclem.b	$⊢ φ \to \exists x \in ℝ \forall n \in Z M (E (n)) \leq x$
7		meaiuninclem.s	$⊢ S = (n \in Z ⟼ M (E (n)))$
8		meaiuninclem.f	$⊢ F = (n \in Z ⟼ E (n) ∖ ⋃_{i \in (N ..^n)} E (i))$
9		0xr	$⊢ 0 \in ℝ^{*}$
10	9	a1i	$⊢ (φ \land n \in Z) \to 0 \in ℝ^{*}$
11		pnfxr	$⊢ +∞ \in ℝ^{*}$
12	11	a1i	$⊢ (φ \land n \in Z) \to +∞ \in ℝ^{*}$
13	1	adantr	$⊢ (φ \land n \in Z) \to M \in Meas$
14		eqid	$⊢ dom M = dom M$
15	4	ffvelrnda	$⊢ (φ \land n \in Z) \to E (n) \in dom M$
16	13 14 15	meaxrcl	$⊢ (φ \land n \in Z) \to M (E (n)) \in ℝ^{*}$
17	13 15	meage0	$⊢ (φ \land n \in Z) \to 0 \leq M (E (n))$
18	6	adantr	$⊢ (φ \land n \in Z) \to \exists x \in ℝ \forall n \in Z M (E (n)) \leq x$
19		simp1	$⊢ ((φ \land n \in Z) \land x \in ℝ \land \forall n \in Z M (E (n)) \leq x) \to (φ \land n \in Z)$
20		simp2	$⊢ ((φ \land n \in Z) \land x \in ℝ \land \forall n \in Z M (E (n)) \leq x) \to x \in ℝ$
21		simp3	$⊢ ((φ \land n \in Z) \land x \in ℝ \land \forall n \in Z M (E (n)) \leq x) \to \forall n \in Z M (E (n)) \leq x$
22	19	simprd	$⊢ ((φ \land n \in Z) \land x \in ℝ \land \forall n \in Z M (E (n)) \leq x) \to n \in Z$
23		rspa	$⊢ (\forall n \in Z M (E (n)) \leq x \land n \in Z) \to M (E (n)) \leq x$
24	21 22 23	syl2anc	$⊢ ((φ \land n \in Z) \land x \in ℝ \land \forall n \in Z M (E (n)) \leq x) \to M (E (n)) \leq x$
25	16	3ad2ant1	$⊢ ((φ \land n \in Z) \land x \in ℝ \land M (E (n)) \leq x) \to M (E (n)) \in ℝ^{*}$
26		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
27	26	3ad2ant2	$⊢ ((φ \land n \in Z) \land x \in ℝ \land M (E (n)) \leq x) \to x \in ℝ^{*}$
28	11	a1i	$⊢ ((φ \land n \in Z) \land x \in ℝ \land M (E (n)) \leq x) \to +∞ \in ℝ^{*}$
29		simp3	$⊢ ((φ \land n \in Z) \land x \in ℝ \land M (E (n)) \leq x) \to M (E (n)) \leq x$
30		ltpnf	$⊢ x \in ℝ \to x < +∞$
31	30	3ad2ant2	$⊢ ((φ \land n \in Z) \land x \in ℝ \land M (E (n)) \leq x) \to x < +∞$
32	25 27 28 29 31	xrlelttrd	$⊢ ((φ \land n \in Z) \land x \in ℝ \land M (E (n)) \leq x) \to M (E (n)) < +∞$
33	19 20 24 32	syl3anc	$⊢ ((φ \land n \in Z) \land x \in ℝ \land \forall n \in Z M (E (n)) \leq x) \to M (E (n)) < +∞$
34	33	3exp	$⊢ (φ \land n \in Z) \to (x \in ℝ \to (\forall n \in Z M (E (n)) \leq x \to M (E (n)) < +∞))$
35	34	rexlimdv	$⊢ (φ \land n \in Z) \to (\exists x \in ℝ \forall n \in Z M (E (n)) \leq x \to M (E (n)) < +∞)$
36	18 35	mpd	$⊢ (φ \land n \in Z) \to M (E (n)) < +∞$
37	10 12 16 17 36	elicod	$⊢ (φ \land n \in Z) \to M (E (n)) \in [0, +∞)$
38	37 7	fmptd	$⊢ φ \to S : Z ⟶ [0, +∞)$
39		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
40	39	a1i	$⊢ φ \to [0, +∞) \subseteq ℝ$
41	38 40	fssd	$⊢ φ \to S : Z ⟶ ℝ$
42	3	peano2uzs	$⊢ n \in Z \to n + 1 \in Z$
43	42	adantl	$⊢ (φ \land n \in Z) \to n + 1 \in Z$
44	4	ffvelrnda	$⊢ (φ \land n + 1 \in Z) \to E (n + 1) \in dom M$
45	43 44	syldan	$⊢ (φ \land n \in Z) \to E (n + 1) \in dom M$
46	13 14 15 45 5	meassle	$⊢ (φ \land n \in Z) \to M (E (n)) \leq M (E (n + 1))$
47	7	a1i	$⊢ φ \to S = (n \in Z ⟼ M (E (n)))$
48		fvexd	$⊢ (φ \land n \in Z) \to M (E (n)) \in V$
49	47 48	fvmpt2d	$⊢ (φ \land n \in Z) \to S (n) = M (E (n))$
50		2fveq3	$⊢ n = m \to M (E (n)) = M (E (m))$
51	50	cbvmptv	$⊢ (n \in Z ⟼ M (E (n))) = (m \in Z ⟼ M (E (m)))$
52	7 51	eqtri	$⊢ S = (m \in Z ⟼ M (E (m)))$
53		2fveq3	$⊢ m = n + 1 \to M (E (m)) = M (E (n + 1))$
54		fvexd	$⊢ (φ \land n \in Z) \to M (E (n + 1)) \in V$
55	52 53 43 54	fvmptd3	$⊢ (φ \land n \in Z) \to S (n + 1) = M (E (n + 1))$
56	49 55	breq12d	$⊢ (φ \land n \in Z) \to (S (n) \leq S (n + 1) \leftrightarrow M (E (n)) \leq M (E (n + 1)))$
57	46 56	mpbird	$⊢ (φ \land n \in Z) \to S (n) \leq S (n + 1)$
58	49	eqcomd	$⊢ (φ \land n \in Z) \to M (E (n)) = S (n)$
59	58	breq1d	$⊢ (φ \land n \in Z) \to (M (E (n)) \leq x \leftrightarrow S (n) \leq x)$
60	59	ralbidva	$⊢ φ \to (\forall n \in Z M (E (n)) \leq x \leftrightarrow \forall n \in Z S (n) \leq x)$
61	60	biimpd	$⊢ φ \to (\forall n \in Z M (E (n)) \leq x \to \forall n \in Z S (n) \leq x)$
62	61	adantr	$⊢ (φ \land x \in ℝ) \to (\forall n \in Z M (E (n)) \leq x \to \forall n \in Z S (n) \leq x)$
63	62	reximdva	$⊢ φ \to (\exists x \in ℝ \forall n \in Z M (E (n)) \leq x \to \exists x \in ℝ \forall n \in Z S (n) \leq x)$
64	6 63	mpd	$⊢ φ \to \exists x \in ℝ \forall n \in Z S (n) \leq x$
65	3 2 41 57 64	climsup	$⊢ φ \to S ⇝ sup (ran S ℝ <)$
66		nfv	$⊢ Ⅎ n φ$
67		nfv	$⊢ Ⅎ x φ$
68		id	$⊢ n \in Z \to n \in Z$
69		fvex	$⊢ E (n) \in V$
70	69	difexi	$⊢ E (n) ∖ ⋃_{i \in (N ..^n)} E (i) \in V$
71	70	a1i	$⊢ n \in Z \to E (n) ∖ ⋃_{i \in (N ..^n)} E (i) \in V$
72	8	fvmpt2	$⊢ (n \in Z \land E (n) ∖ ⋃_{i \in (N ..^n)} E (i) \in V) \to F (n) = E (n) ∖ ⋃_{i \in (N ..^n)} E (i)$
73	68 71 72	syl2anc	$⊢ n \in Z \to F (n) = E (n) ∖ ⋃_{i \in (N ..^n)} E (i)$
74	73	adantl	$⊢ (φ \land n \in Z) \to F (n) = E (n) ∖ ⋃_{i \in (N ..^n)} E (i)$
75	1 14	dmmeasal	$⊢ φ \to dom M \in SAlg$
76	75	adantr	$⊢ (φ \land n \in Z) \to dom M \in SAlg$
77		fzoct	$⊢ (N ..^n) ≼ ω$
78	77	a1i	$⊢ (φ \land n \in Z) \to (N ..^n) ≼ ω$
79	4	adantr	$⊢ (φ \land i \in (N ..^n)) \to E : Z ⟶ dom M$
80		fzossuz	$⊢ (N ..^n) \subseteq ℤ_{\geq N}$
81	3	eqcomi	$⊢ ℤ_{\geq N} = Z$
82	80 81	sseqtri	$⊢ (N ..^n) \subseteq Z$
83	82	sseli	$⊢ i \in (N ..^n) \to i \in Z$
84	83	adantl	$⊢ (φ \land i \in (N ..^n)) \to i \in Z$
85	79 84	ffvelrnd	$⊢ (φ \land i \in (N ..^n)) \to E (i) \in dom M$
86	85	adantlr	$⊢ ((φ \land n \in Z) \land i \in (N ..^n)) \to E (i) \in dom M$
87	76 78 86	saliuncl	$⊢ (φ \land n \in Z) \to ⋃_{i \in (N ..^n)} E (i) \in dom M$
88		saldifcl2	$⊢ (dom M \in SAlg \land E (n) \in dom M \land ⋃_{i \in (N ..^n)} E (i) \in dom M) \to E (n) ∖ ⋃_{i \in (N ..^n)} E (i) \in dom M$
89	76 15 87 88	syl3anc	$⊢ (φ \land n \in Z) \to E (n) ∖ ⋃_{i \in (N ..^n)} E (i) \in dom M$
90	74 89	eqeltrd	$⊢ (φ \land n \in Z) \to F (n) \in dom M$
91	13 14 90	meaxrcl	$⊢ (φ \land n \in Z) \to M (F (n)) \in ℝ^{*}$
92	13 90	meage0	$⊢ (φ \land n \in Z) \to 0 \leq M (F (n))$
93		difssd	$⊢ (φ \land n \in Z) \to E (n) ∖ ⋃_{i \in (N ..^n)} E (i) \subseteq E (n)$
94	74 93	eqsstrd	$⊢ (φ \land n \in Z) \to F (n) \subseteq E (n)$
95	13 14 90 15 94	meassle	$⊢ (φ \land n \in Z) \to M (F (n)) \leq M (E (n))$
96	91 16 12 95 36	xrlelttrd	$⊢ (φ \land n \in Z) \to M (F (n)) < +∞$
97	10 12 91 92 96	elicod	$⊢ (φ \land n \in Z) \to M (F (n)) \in [0, +∞)$
98		2fveq3	$⊢ n = i \to M (E (n)) = M (E (i))$
99	98	breq1d	$⊢ n = i \to (M (E (n)) \leq x \leftrightarrow M (E (i)) \leq x)$
100	99	cbvralvw	$⊢ \forall n \in Z M (E (n)) \leq x \leftrightarrow \forall i \in Z M (E (i)) \leq x$
101	100	biimpi	$⊢ \forall n \in Z M (E (n)) \leq x \to \forall i \in Z M (E (i)) \leq x$
102	101	adantl	$⊢ (φ \land \forall n \in Z M (E (n)) \leq x) \to \forall i \in Z M (E (i)) \leq x$
103		eleq1w	$⊢ n = i \to (n \in Z \leftrightarrow i \in Z)$
104	103	anbi2d	$⊢ n = i \to ((φ \land n \in Z) \leftrightarrow (φ \land i \in Z))$
105		oveq2	$⊢ n = i \to (N \dots n) = (N \dots i)$
106	105	sumeq1d	$⊢ n = i \to \sum_{m = N}^{n} M (F (m)) = \sum_{m = N}^{i} M (F (m))$
107	98 106	eqeq12d	$⊢ n = i \to (M (E (n)) = \sum_{m = N}^{n} M (F (m)) \leftrightarrow M (E (i)) = \sum_{m = N}^{i} M (F (m)))$
108	104 107	imbi12d	$⊢ n = i \to (((φ \land n \in Z) \to M (E (n)) = \sum_{m = N}^{n} M (F (m))) \leftrightarrow ((φ \land i \in Z) \to M (E (i)) = \sum_{m = N}^{i} M (F (m))))$
109		eleq1w	$⊢ m = n \to (m \in Z \leftrightarrow n \in Z)$
110	109	anbi2d	$⊢ m = n \to ((φ \land m \in Z) \leftrightarrow (φ \land n \in Z))$
111		oveq2	$⊢ m = n \to (N \dots m) = (N \dots n)$
112	111	iuneq1d	$⊢ m = n \to ⋃_{i = N}^{m} F (i) = ⋃_{i = N}^{n} F (i)$
113	111	iuneq1d	$⊢ m = n \to ⋃_{i = N}^{m} E (i) = ⋃_{i = N}^{n} E (i)$
114	112 113	eqeq12d	$⊢ m = n \to (⋃_{i = N}^{m} F (i) = ⋃_{i = N}^{m} E (i) \leftrightarrow ⋃_{i = N}^{n} F (i) = ⋃_{i = N}^{n} E (i))$
115	110 114	imbi12d	$⊢ m = n \to (((φ \land m \in Z) \to ⋃_{i = N}^{m} F (i) = ⋃_{i = N}^{m} E (i)) \leftrightarrow ((φ \land n \in Z) \to ⋃_{i = N}^{n} F (i) = ⋃_{i = N}^{n} E (i)))$
116		fveq2	$⊢ i = n \to F (i) = F (n)$
117	116	cbviunv	$⊢ ⋃_{i = N}^{m} F (i) = ⋃_{n = N}^{m} F (n)$
118	117	a1i	$⊢ (φ \land m \in Z) \to ⋃_{i = N}^{m} F (i) = ⋃_{n = N}^{m} F (n)$
119	66 3 4 8	iundjiun	$⊢ φ \to ((\forall m \in Z ⋃_{n = N}^{m} F (n) = ⋃_{n = N}^{m} E (n) \land ⋃_{n \in Z} F (n) = ⋃_{n \in Z} E (n)) \land \underset{n \in Z}{Disj} F (n))$
120	119	simplld	$⊢ φ \to \forall m \in Z ⋃_{n = N}^{m} F (n) = ⋃_{n = N}^{m} E (n)$
121	120	adantr	$⊢ (φ \land m \in Z) \to \forall m \in Z ⋃_{n = N}^{m} F (n) = ⋃_{n = N}^{m} E (n)$
122		simpr	$⊢ (φ \land m \in Z) \to m \in Z$
123		rspa	$⊢ (\forall m \in Z ⋃_{n = N}^{m} F (n) = ⋃_{n = N}^{m} E (n) \land m \in Z) \to ⋃_{n = N}^{m} F (n) = ⋃_{n = N}^{m} E (n)$
124	121 122 123	syl2anc	$⊢ (φ \land m \in Z) \to ⋃_{n = N}^{m} F (n) = ⋃_{n = N}^{m} E (n)$
125		fveq2	$⊢ n = i \to E (n) = E (i)$
126	125	cbviunv	$⊢ ⋃_{n = N}^{m} E (n) = ⋃_{i = N}^{m} E (i)$
127	126	a1i	$⊢ (φ \land m \in Z) \to ⋃_{n = N}^{m} E (n) = ⋃_{i = N}^{m} E (i)$
128	118 124 127	3eqtrd	$⊢ (φ \land m \in Z) \to ⋃_{i = N}^{m} F (i) = ⋃_{i = N}^{m} E (i)$
129	115 128	chvarvv	$⊢ (φ \land n \in Z) \to ⋃_{i = N}^{n} F (i) = ⋃_{i = N}^{n} E (i)$
130	68 3	eleqtrdi	$⊢ n \in Z \to n \in ℤ_{\geq N}$
131	130	adantl	$⊢ (φ \land n \in Z) \to n \in ℤ_{\geq N}$
132		fvoveq1	$⊢ n = i \to E (n + 1) = E (i + 1)$
133	125 132	sseq12d	$⊢ n = i \to (E (n) \subseteq E (n + 1) \leftrightarrow E (i) \subseteq E (i + 1))$
134	104 133	imbi12d	$⊢ n = i \to (((φ \land n \in Z) \to E (n) \subseteq E (n + 1)) \leftrightarrow ((φ \land i \in Z) \to E (i) \subseteq E (i + 1)))$
135	134 5	chvarvv	$⊢ (φ \land i \in Z) \to E (i) \subseteq E (i + 1)$
136	84 135	syldan	$⊢ (φ \land i \in (N ..^n)) \to E (i) \subseteq E (i + 1)$
137	136	adantlr	$⊢ ((φ \land n \in Z) \land i \in (N ..^n)) \to E (i) \subseteq E (i + 1)$
138	131 137	iunincfi	$⊢ (φ \land n \in Z) \to ⋃_{i = N}^{n} E (i) = E (n)$
139	129 138	eqtr2d	$⊢ (φ \land n \in Z) \to E (n) = ⋃_{i = N}^{n} F (i)$
140	139	fveq2d	$⊢ (φ \land n \in Z) \to M (E (n)) = M (⋃_{i = N}^{n} F (i))$
141		nfv	$⊢ Ⅎ i (φ \land n \in Z)$
142		elfzuz	$⊢ i \in (N \dots n) \to i \in ℤ_{\geq N}$
143	142 81	eleqtrdi	$⊢ i \in (N \dots n) \to i \in Z$
144	143	adantl	$⊢ (φ \land i \in (N \dots n)) \to i \in Z$
145		fveq2	$⊢ n = i \to F (n) = F (i)$
146	145	eleq1d	$⊢ n = i \to (F (n) \in dom M \leftrightarrow F (i) \in dom M)$
147	104 146	imbi12d	$⊢ n = i \to (((φ \land n \in Z) \to F (n) \in dom M) \leftrightarrow ((φ \land i \in Z) \to F (i) \in dom M))$
148	147 90	chvarvv	$⊢ (φ \land i \in Z) \to F (i) \in dom M$
149	144 148	syldan	$⊢ (φ \land i \in (N \dots n)) \to F (i) \in dom M$
150	149	adantlr	$⊢ ((φ \land n \in Z) \land i \in (N \dots n)) \to F (i) \in dom M$
151		fzct	$⊢ (N \dots n) ≼ ω$
152	151	a1i	$⊢ (φ \land n \in Z) \to (N \dots n) ≼ ω$
153	144	ssd	$⊢ φ \to (N \dots n) \subseteq Z$
154	119	simprd	$⊢ φ \to \underset{n \in Z}{Disj} F (n)$
155	145	cbvdisjv	$⊢ \underset{n \in Z}{Disj} F (n) \leftrightarrow \underset{i \in Z}{Disj} F (i)$
156	154 155	sylib	$⊢ φ \to \underset{i \in Z}{Disj} F (i)$
157		disjss1	$⊢ (N \dots n) \subseteq Z \to (\underset{i \in Z}{Disj} F (i) \to {Disj}_{i = N}^{n} F (i))$
158	153 156 157	sylc	$⊢ φ \to {Disj}_{i = N}^{n} F (i)$
159	158	adantr	$⊢ (φ \land n \in Z) \to {Disj}_{i = N}^{n} F (i)$
160	141 13 14 150 152 159	meadjiun	$⊢ (φ \land n \in Z) \to M (⋃_{i = N}^{n} F (i)) = sum^((i \in (N \dots n) ⟼ M (F (i))))$
161		fzfid	$⊢ (φ \land n \in Z) \to (N \dots n) \in Fin$
162		2fveq3	$⊢ n = i \to M (F (n)) = M (F (i))$
163	162	eleq1d	$⊢ n = i \to (M (F (n)) \in [0, +∞) \leftrightarrow M (F (i)) \in [0, +∞))$
164	104 163	imbi12d	$⊢ n = i \to (((φ \land n \in Z) \to M (F (n)) \in [0, +∞)) \leftrightarrow ((φ \land i \in Z) \to M (F (i)) \in [0, +∞)))$
165	164 97	chvarvv	$⊢ (φ \land i \in Z) \to M (F (i)) \in [0, +∞)$
166	144 165	syldan	$⊢ (φ \land i \in (N \dots n)) \to M (F (i)) \in [0, +∞)$
167	166	adantlr	$⊢ ((φ \land n \in Z) \land i \in (N \dots n)) \to M (F (i)) \in [0, +∞)$
168	161 167	sge0fsummpt	$⊢ (φ \land n \in Z) \to sum^((i \in (N \dots n) ⟼ M (F (i)))) = \sum_{i = N}^{n} M (F (i))$
169		2fveq3	$⊢ i = m \to M (F (i)) = M (F (m))$
170	169	cbvsumv	$⊢ \sum_{i = N}^{n} M (F (i)) = \sum_{m = N}^{n} M (F (m))$
171	170	a1i	$⊢ (φ \land n \in Z) \to \sum_{i = N}^{n} M (F (i)) = \sum_{m = N}^{n} M (F (m))$
172	168 171	eqtrd	$⊢ (φ \land n \in Z) \to sum^((i \in (N \dots n) ⟼ M (F (i)))) = \sum_{m = N}^{n} M (F (m))$
173	140 160 172	3eqtrd	$⊢ (φ \land n \in Z) \to M (E (n)) = \sum_{m = N}^{n} M (F (m))$
174	108 173	chvarvv	$⊢ (φ \land i \in Z) \to M (E (i)) = \sum_{m = N}^{i} M (F (m))$
175		2fveq3	$⊢ m = n \to M (F (m)) = M (F (n))$
176	175	cbvsumv	$⊢ \sum_{m = N}^{i} M (F (m)) = \sum_{n = N}^{i} M (F (n))$
177	176	a1i	$⊢ (φ \land i \in Z) \to \sum_{m = N}^{i} M (F (m)) = \sum_{n = N}^{i} M (F (n))$
178	174 177	eqtrd	$⊢ (φ \land i \in Z) \to M (E (i)) = \sum_{n = N}^{i} M (F (n))$
179	178	breq1d	$⊢ (φ \land i \in Z) \to (M (E (i)) \leq x \leftrightarrow \sum_{n = N}^{i} M (F (n)) \leq x)$
180	179	ralbidva	$⊢ φ \to (\forall i \in Z M (E (i)) \leq x \leftrightarrow \forall i \in Z \sum_{n = N}^{i} M (F (n)) \leq x)$
181	180	biimpd	$⊢ φ \to (\forall i \in Z M (E (i)) \leq x \to \forall i \in Z \sum_{n = N}^{i} M (F (n)) \leq x)$
182	181	imp	$⊢ (φ \land \forall i \in Z M (E (i)) \leq x) \to \forall i \in Z \sum_{n = N}^{i} M (F (n)) \leq x$
183	102 182	syldan	$⊢ (φ \land \forall n \in Z M (E (n)) \leq x) \to \forall i \in Z \sum_{n = N}^{i} M (F (n)) \leq x$
184	183	ex	$⊢ φ \to (\forall n \in Z M (E (n)) \leq x \to \forall i \in Z \sum_{n = N}^{i} M (F (n)) \leq x)$
185	184	reximdv	$⊢ φ \to (\exists x \in ℝ \forall n \in Z M (E (n)) \leq x \to \exists x \in ℝ \forall i \in Z \sum_{n = N}^{i} M (F (n)) \leq x)$
186	6 185	mpd	$⊢ φ \to \exists x \in ℝ \forall i \in Z \sum_{n = N}^{i} M (F (n)) \leq x$
187	66 67 2 3 97 186	sge0reuzb	$⊢ φ \to sum^((n \in Z ⟼ M (F (n)))) = sup (ran (i \in Z ⟼ \sum_{n = N}^{i} M (F (n))) ℝ <)$
188	98	cbvmptv	$⊢ (n \in Z ⟼ M (E (n))) = (i \in Z ⟼ M (E (i)))$
189	7 188	eqtri	$⊢ S = (i \in Z ⟼ M (E (i)))$
190	189	a1i	$⊢ φ \to S = (i \in Z ⟼ M (E (i)))$
191	178	mpteq2dva	$⊢ φ \to (i \in Z ⟼ M (E (i))) = (i \in Z ⟼ \sum_{n = N}^{i} M (F (n)))$
192	190 191	eqtrd	$⊢ φ \to S = (i \in Z ⟼ \sum_{n = N}^{i} M (F (n)))$
193	192	rneqd	$⊢ φ \to ran S = ran (i \in Z ⟼ \sum_{n = N}^{i} M (F (n)))$
194	193	supeq1d	$⊢ φ \to sup (ran S ℝ <) = sup (ran (i \in Z ⟼ \sum_{n = N}^{i} M (F (n))) ℝ <)$
195	187 194	eqtr4d	$⊢ φ \to sum^((n \in Z ⟼ M (F (n)))) = sup (ran S ℝ <)$
196	195	eqcomd	$⊢ φ \to sup (ran S ℝ <) = sum^((n \in Z ⟼ M (F (n))))$
197	3	uzct	$⊢ Z ≼ ω$
198	197	a1i	$⊢ φ \to Z ≼ ω$
199	66 1 14 90 198 154	meadjiun	$⊢ φ \to M (⋃_{n \in Z} F (n)) = sum^((n \in Z ⟼ M (F (n))))$
200	199	eqcomd	$⊢ φ \to sum^((n \in Z ⟼ M (F (n)))) = M (⋃_{n \in Z} F (n))$
201	119	simplrd	$⊢ φ \to ⋃_{n \in Z} F (n) = ⋃_{n \in Z} E (n)$
202	201	fveq2d	$⊢ φ \to M (⋃_{n \in Z} F (n)) = M (⋃_{n \in Z} E (n))$
203	196 200 202	3eqtrd	$⊢ φ \to sup (ran S ℝ <) = M (⋃_{n \in Z} E (n))$
204	65 203	breqtrd	$⊢ φ \to S ⇝ M (⋃_{n \in Z} E (n))$

Metamath Proof Explorer

Theorem meaiuninclem

Proof