meaiuninclem - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > meaiuninclem		Structured version Visualization version Unicode version

Theorem meaiuninclem 40697

Description: Measures are continuous from below (bounded case): if

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.)

**Hypotheses**
Ref	Expression
meaiuninclem.m	Meas
meaiuninclem.n
meaiuninclem.z
meaiuninclem.e
meaiuninclem.i	$/\$
meaiuninclem.b
meaiuninclem.s
meaiuninclem.f	$\$ ..^

**Assertion**
Ref	Expression
meaiuninclem

Distinct variable groups:

Allowed substitution hint:

(

)

Proof of Theorem meaiuninclem Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		meaiuninclem.z	. . 3
2		meaiuninclem.n	. . 3
3		0xr 10086	. . . . . . 7
4	3	a1i 11	. . . . . 6 $/\$
5		pnfxr 10092	. . . . . . 7
6	5	a1i 11	. . . . . 6 $/\$
7		meaiuninclem.m	. . . . . . . 8 Meas
8	7	adantr 481	. . . . . . 7 $/\$ Meas
9		eqid 2622	. . . . . . 7
10		meaiuninclem.e	. . . . . . . 8
11	10	ffvelrnda 6359	. . . . . . 7 $/\$
12	8, 9, 11	meaxrcl 40678	. . . . . 6 $/\$
13	8, 11	meage0 40692	. . . . . 6 $/\$
14		meaiuninclem.b	. . . . . . . 8
15	14	adantr 481	. . . . . . 7 $/\$
16		simp1 1061	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
17		simp2 1062	. . . . . . . . . 10 $/\$ $/\$ $/\$
18		simp3 1063	. . . . . . . . . . 11 $/\$ $/\$ $/\$
19	16	simprd 479	. . . . . . . . . . 11 $/\$ $/\$ $/\$
20		rspa 2930	. . . . . . . . . . 11 $/\$
21	18, 19, 20	syl2anc 693	. . . . . . . . . 10 $/\$ $/\$ $/\$
22	12	3ad2ant1 1082	. . . . . . . . . . 11 $/\$ $/\$ $/\$
23		rexr 10085	. . . . . . . . . . . 12
24	23	3ad2ant2 1083	. . . . . . . . . . 11 $/\$ $/\$ $/\$
25	5	a1i 11	. . . . . . . . . . 11 $/\$ $/\$ $/\$
26		simp3 1063	. . . . . . . . . . 11 $/\$ $/\$ $/\$
27		ltpnf 11954	. . . . . . . . . . . 12
28	27	3ad2ant2 1083	. . . . . . . . . . 11 $/\$ $/\$ $/\$
29	22, 24, 25, 26, 28	xrlelttrd 11991	. . . . . . . . . 10 $/\$ $/\$ $/\$
30	16, 17, 21, 29	syl3anc 1326	. . . . . . . . 9 $/\$ $/\$ $/\$
31	30	3exp 1264	. . . . . . . 8 $/\$
32	31	rexlimdv 3030	. . . . . . 7 $/\$
33	15, 32	mpd 15	. . . . . 6 $/\$
34	4, 6, 12, 13, 33	elicod 12224	. . . . 5 $/\$
35		meaiuninclem.s	. . . . 5
36	34, 35	fmptd 6385	. . . 4
37		rge0ssre 12280	. . . . 5
38	37	a1i 11	. . . 4
39	36, 38	fssd 6057	. . 3
40	1	peano2uzs 11742	. . . . . . 7
41	40	adantl 482	. . . . . 6 $/\$
42	10	ffvelrnda 6359	. . . . . 6 $/\$
43	41, 42	syldan 487	. . . . 5 $/\$
44		meaiuninclem.i	. . . . 5 $/\$
45	8, 9, 11, 43, 44	meassle 40680	. . . 4 $/\$
46	35	a1i 11	. . . . . 6
47		fvexd 6203	. . . . . 6 $/\$
48	46, 47	fvmpt2d 6293	. . . . 5 $/\$
49		fveq2 6191	. . . . . . . . . 10
50	49	fveq2d 6195	. . . . . . . . 9
51	50	cbvmptv 4750	. . . . . . . 8
52	35, 51	eqtri 2644	. . . . . . 7
53	52	a1i 11	. . . . . 6 $/\$
54		fveq2 6191	. . . . . . . 8
55	54	fveq2d 6195	. . . . . . 7
56	55	adantl 482	. . . . . 6 $/\$ $/\$
57		fvexd 6203	. . . . . 6 $/\$
58	53, 56, 41, 57	fvmptd 6288	. . . . 5 $/\$
59	48, 58	breq12d 4666	. . . 4 $/\$
60	45, 59	mpbird 247	. . 3 $/\$
61	48	eqcomd 2628	. . . . . . . . 9 $/\$
62	61	breq1d 4663	. . . . . . . 8 $/\$
63	62	ralbidva 2985	. . . . . . 7
64	63	biimpd 219	. . . . . 6
65	64	adantr 481	. . . . 5 $/\$
66	65	reximdva 3017	. . . 4
67	14, 66	mpd 15	. . 3
68	1, 2, 39, 60, 67	climsup 14400	. 2
69		nfv 1843	. . . . . 6
70		nfv 1843	. . . . . 6
71		id 22	. . . . . . . . . . 11
72		fvex 6201	. . . . . . . . . . . . 13
73	72	difexi 4809	. . . . . . . . . . . 12 $\$ ..^
74	73	a1i 11	. . . . . . . . . . 11 $\$ ..^
75		meaiuninclem.f	. . . . . . . . . . . 12 $\$ ..^
76	75	fvmpt2 6291	. . . . . . . . . . 11 $/\$ $\$ ..^ $\$ ..^
77	71, 74, 76	syl2anc 693	. . . . . . . . . 10 $\$ ..^
78	77	adantl 482	. . . . . . . . 9 $/\$ $\$ ..^
79	7, 9	dmmeasal 40669	. . . . . . . . . . 11 SAlg
80	79	adantr 481	. . . . . . . . . 10 $/\$ SAlg
81		fzoct 39603	. . . . . . . . . . . 12 ..^
82	81	a1i 11	. . . . . . . . . . 11 $/\$ ..^
83	10	adantr 481	. . . . . . . . . . . . 13 $/\$ ..^
84		fzossuz 39598	. . . . . . . . . . . . . . . 16 ..^
85	1	eqcomi 2631	. . . . . . . . . . . . . . . 16
86	84, 85	sseqtri 3637	. . . . . . . . . . . . . . 15 ..^
87	86	sseli 3599	. . . . . . . . . . . . . 14 ..^
88	87	adantl 482	. . . . . . . . . . . . 13 $/\$ ..^
89	83, 88	ffvelrnd 6360	. . . . . . . . . . . 12 $/\$ ..^
90	89	adantlr 751	. . . . . . . . . . 11 $/\$ $/\$ ..^
91	80, 82, 90	saliuncl 40542	. . . . . . . . . 10 $/\$ ..^
92		saldifcl2 40546	. . . . . . . . . 10 SAlg $/\$ $/\$ ..^ $\$ ..^
93	80, 11, 91, 92	syl3anc 1326	. . . . . . . . 9 $/\$ $\$ ..^
94	78, 93	eqeltrd 2701	. . . . . . . 8 $/\$
95	8, 9, 94	meaxrcl 40678	. . . . . . 7 $/\$
96	8, 94	meage0 40692	. . . . . . 7 $/\$
97		difssd 3738	. . . . . . . . . 10 $/\$ $\$ ..^
98	78, 97	eqsstrd 3639	. . . . . . . . 9 $/\$
99	8, 9, 94, 11, 98	meassle 40680	. . . . . . . 8 $/\$
100	95, 12, 6, 99, 33	xrlelttrd 11991	. . . . . . 7 $/\$
101	4, 6, 95, 96, 100	elicod 12224	. . . . . 6 $/\$
102		fveq2 6191	. . . . . . . . . . . . . . 15
103	102	fveq2d 6195	. . . . . . . . . . . . . 14
104	103	breq1d 4663	. . . . . . . . . . . . 13
105	104	cbvralv 3171	. . . . . . . . . . . 12
106	105	biimpi 206	. . . . . . . . . . 11
107	106	adantl 482	. . . . . . . . . 10 $/\$
108		eleq1 2689	. . . . . . . . . . . . . . . . . 18
109	108	anbi2d 740	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
110		oveq2 6658	. . . . . . . . . . . . . . . . . . 19
111	110	sumeq1d 14431	. . . . . . . . . . . . . . . . . 18
112	103, 111	eqeq12d 2637	. . . . . . . . . . . . . . . . 17
113	109, 112	imbi12d 334	. . . . . . . . . . . . . . . 16 $/\$ $/\$
114		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . 22
115	114	anbi2d 740	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
116		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . 23
117	116	iuneq1d 4545	. . . . . . . . . . . . . . . . . . . . . 22
118	116	iuneq1d 4545	. . . . . . . . . . . . . . . . . . . . . 22
119	117, 118	eqeq12d 2637	. . . . . . . . . . . . . . . . . . . . 21
120	115, 119	imbi12d 334	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
121		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . 23
122	121	cbviunv 4559	. . . . . . . . . . . . . . . . . . . . . 22
123	122	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$
124	69, 1, 10, 75	iundjiun 40677	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ Disj
125	124	simplld 791	. . . . . . . . . . . . . . . . . . . . . . 23
126	125	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
127		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
128		rspa 2930	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
129	126, 127, 128	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 $/\$
130	102	cbviunv 4559	. . . . . . . . . . . . . . . . . . . . . 22
131	130	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$
132	123, 129, 131	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . 20 $/\$
133	120, 132	chvarv 2263	. . . . . . . . . . . . . . . . . . 19 $/\$
134	71, 1	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . 21
135	134	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$
136		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . 26
137	136	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . 25
138	102, 137	sseq12d 3634	. . . . . . . . . . . . . . . . . . . . . . . 24
139	109, 138	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
140	139, 44	chvarv 2263	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
141	88, 140	syldan 487	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^
142	141	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ ..^
143	135, 142	iunincfi 39272	. . . . . . . . . . . . . . . . . . 19 $/\$
144	133, 143	eqtr2d 2657	. . . . . . . . . . . . . . . . . 18 $/\$
145	144	fveq2d 6195	. . . . . . . . . . . . . . . . 17 $/\$
146		nfv 1843	. . . . . . . . . . . . . . . . . 18 $/\$
147		elfzuz 12338	. . . . . . . . . . . . . . . . . . . . . 22
148	147, 85	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . 21
149	148	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$
150		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . 23
151	150	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . 22
152	109, 151	imbi12d 334	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
153	152, 94	chvarv 2263	. . . . . . . . . . . . . . . . . . . 20 $/\$
154	149, 153	syldan 487	. . . . . . . . . . . . . . . . . . 19 $/\$
155	154	adantlr 751	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
156		fzct 39596	. . . . . . . . . . . . . . . . . . 19
157	156	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$
158	149	ssd 39252	. . . . . . . . . . . . . . . . . . . 20
159	124	simprd 479	. . . . . . . . . . . . . . . . . . . . 21 Disj
160	150	cbvdisjv 4631	. . . . . . . . . . . . . . . . . . . . 21 Disj Disj
161	159, 160	sylib 208	. . . . . . . . . . . . . . . . . . . 20 Disj
162		disjss1 4626	. . . . . . . . . . . . . . . . . . . 20 Disj Disj
163	158, 161, 162	sylc 65	. . . . . . . . . . . . . . . . . . 19 Disj
164	163	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ Disj
165	146, 8, 9, 155, 157, 164	meadjiun 40683	. . . . . . . . . . . . . . . . 17 $/\$ Σ^{^}
166		fzfid 12772	. . . . . . . . . . . . . . . . . . 19 $/\$
167	150	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . 24
168	167	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . 23
169	109, 168	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
170	169, 101	chvarv 2263	. . . . . . . . . . . . . . . . . . . . 21 $/\$
171	149, 170	syldan 487	. . . . . . . . . . . . . . . . . . . 20 $/\$
172	171	adantlr 751	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
173	166, 172	sge0fsummpt 40607	. . . . . . . . . . . . . . . . . 18 $/\$ Σ^{^}
174		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21
175	174	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20
176	175	cbvsumv 14426	. . . . . . . . . . . . . . . . . . 19
177	176	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$
178	173, 177	eqtrd 2656	. . . . . . . . . . . . . . . . 17 $/\$ Σ^{^}
179	145, 165, 178	3eqtrd 2660	. . . . . . . . . . . . . . . 16 $/\$
180	113, 179	chvarv 2263	. . . . . . . . . . . . . . 15 $/\$
181		fveq2 6191	. . . . . . . . . . . . . . . . . 18
182	181	fveq2d 6195	. . . . . . . . . . . . . . . . 17
183	182	cbvsumv 14426	. . . . . . . . . . . . . . . 16
184	183	a1i 11	. . . . . . . . . . . . . . 15 $/\$
185	180, 184	eqtrd 2656	. . . . . . . . . . . . . 14 $/\$
186	185	breq1d 4663	. . . . . . . . . . . . 13 $/\$
187	186	ralbidva 2985	. . . . . . . . . . . 12
188	187	biimpd 219	. . . . . . . . . . 11
189	188	imp 445	. . . . . . . . . 10 $/\$
190	107, 189	syldan 487	. . . . . . . . 9 $/\$
191	190	ex 450	. . . . . . . 8
192	191	reximdv 3016	. . . . . . 7
193	14, 192	mpd 15	. . . . . 6
194	69, 70, 2, 1, 101, 193	sge0reuzb 40665	. . . . 5 Σ^{^}
195	103	cbvmptv 4750	. . . . . . . . . 10
196	35, 195	eqtri 2644	. . . . . . . . 9
197	196	a1i 11	. . . . . . . 8
198	185	mpteq2dva 4744	. . . . . . . 8
199	197, 198	eqtrd 2656	. . . . . . 7
200	199	rneqd 5353	. . . . . 6
201	200	supeq1d 8352	. . . . 5
202	194, 201	eqtr4d 2659	. . . 4 Σ^{^}
203	202	eqcomd 2628	. . 3 Σ^{^}
204	1	uzct 39232	. . . . . 6
205	204	a1i 11	. . . . 5
206	69, 7, 9, 94, 205, 159	meadjiun 40683	. . . 4 Σ^{^}
207	206	eqcomd 2628	. . 3 Σ^{^}
208	124	simplrd 793	. . . 4
209	208	fveq2d 6195	. . 3
210	203, 207, 209	3eqtrd 2660	. 2
211	68, 210	breqtrd 4679	1

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wcel 1990

wral 2912

wrex 2913

cvv 3200 $\$ cdif 3571

wss 3574

ciun 4520 Disj wdisj 4620 class class class wbr 4653

cmpt 4729

cdm 5114

crn 5115

wf 5884

cfv 5888 (class class class)co 6650

com 7065

cdom 7953

csup 8346

cr 9935

cc0 9936

c1 9937

caddc 9939

cpnf 10071

cxr 10073

clt 10074

cle 10075

cz 11377

cuz 11687

cico 12177

cfz 12326 ..^cfzo 12465

cli 14215

csu 14416 SAlgcsalg 40528 Σ^{^}csumge0 40579 Meascmea 40666

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-disj 4621 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-omul 7565 df-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-oi 8415 df-card 8765 df-acn 8768 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-xadd 11947 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-sum 14417 df-salg 40529 df-sumge0 40580 df-mea 40667

This theorem is referenced by: meaiuninc 40698

W3C validator