bddmulibl - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > bddmulibl		Structured version Unicode version

Theorem bddmulibl 21432

Description: A bounded function times an integrable function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.)

**Assertion**
Ref	Expression
bddmulibl	MblFn $/\$ $/\$

Distinct variable groups:

Proof of Theorem bddmulibl Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mbff 21221	. . . . . . 7 MblFn
2	1	ad2antrr 725	. . . . . 6 MblFn $/\$ $/\$ $/\$
3		ffn 5657	. . . . . 6
4	2, 3	syl 16	. . . . 5 MblFn $/\$ $/\$ $/\$
5		iblmbf 21361	. . . . . . . 8 MblFn
6	5	ad2antlr 726	. . . . . . 7 MblFn $/\$ $/\$ $/\$ MblFn
7		mbff 21221	. . . . . . 7 MblFn
8	6, 7	syl 16	. . . . . 6 MblFn $/\$ $/\$ $/\$
9		ffn 5657	. . . . . 6
10	8, 9	syl 16	. . . . 5 MblFn $/\$ $/\$ $/\$
11		mbfdm 21222	. . . . . 6 MblFn
12	11	ad2antrr 725	. . . . 5 MblFn $/\$ $/\$ $/\$
13		mbfdm 21222	. . . . . 6 MblFn
14	6, 13	syl 16	. . . . 5 MblFn $/\$ $/\$ $/\$
15		eqid 2451	. . . . 5
16		eqidd 2452	. . . . 5 MblFn $/\$ $/\$ $/\$ $/\$
17		eqidd 2452	. . . . 5 MblFn $/\$ $/\$ $/\$ $/\$
18	4, 10, 12, 14, 15, 16, 17	offval 6427	. . . 4 MblFn $/\$ $/\$ $/\$
19		ovex 6215	. . . . . 6
20	19	a1i 11	. . . . 5 MblFn $/\$ $/\$ $/\$ $/\$
21		simpll 753	. . . . . . 7 MblFn $/\$ $/\$ $/\$ MblFn
22	21, 6	mbfmul 21320	. . . . . 6 MblFn $/\$ $/\$ $/\$ MblFn
23	18, 22	eqeltrrd 2540	. . . . 5 MblFn $/\$ $/\$ $/\$ MblFn
24	23, 20	mbfmptcl 21231	. . . . . . . 8 MblFn $/\$ $/\$ $/\$ $/\$
25		eqidd 2452	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
26		absf 12927	. . . . . . . . . 10
27	26	a1i 11	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
28	27	feqmptd 5843	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
29		fveq2 5789	. . . . . . . 8
30	24, 25, 28, 29	fmptco 5975	. . . . . . 7 MblFn $/\$ $/\$ $/\$
31		eqid 2451	. . . . . . . . 9
32	24, 31	fmptd 5966	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
33		ax-resscn 9440	. . . . . . . . . . 11
34		ssid 3473	. . . . . . . . . . 11
35		cncfss 20591	. . . . . . . . . . 11 $/\$
36	33, 34, 35	mp2an 672	. . . . . . . . . 10
37		abscncf 20593	. . . . . . . . . 10
38	36, 37	sselii 3451	. . . . . . . . 9
39	38	a1i 11	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
40		cncombf 21252	. . . . . . . 8 MblFn $/\$ $/\$ MblFn
41	23, 32, 39, 40	syl3anc 1219	. . . . . . 7 MblFn $/\$ $/\$ $/\$ MblFn
42	30, 41	eqeltrrd 2540	. . . . . 6 MblFn $/\$ $/\$ $/\$ MblFn
43	24	abscld 13024	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
44	43	rexrd 9534	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
45	24	absge0d 13032	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
46		elxrge0 11495	. . . . . . . . . . 11 $/\$
47	44, 45, 46	sylanbrc 664	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
48		0e0iccpnf 11497	. . . . . . . . . . 11
49	48	a1i 11	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
50	47, 49	ifclda 3919	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
51	50	adantr 465	. . . . . . . 8 MblFn $/\$ $/\$ $/\$ $/\$
52		eqid 2451	. . . . . . . 8
53	51, 52	fmptd 5966	. . . . . . 7 MblFn $/\$ $/\$ $/\$
54		reex 9474	. . . . . . . . . . . . . . 15
55	54	a1i 11	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
56		simprl 755	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
57	56	ad2antrr 725	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$ $/\$
58		elin 3637	. . . . . . . . . . . . . . . . . . . 20 $/\$
59	58	simprbi 464	. . . . . . . . . . . . . . . . . . 19
60		ffvelrn 5940	. . . . . . . . . . . . . . . . . . 19 $/\$
61	8, 59, 60	syl2an 477	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
62	61	abscld 13024	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
63	61	absge0d 13032	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
64		elrege0 11493	. . . . . . . . . . . . . . . . 17 $/\$
65	62, 63, 64	sylanbrc 664	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$ $/\$
66		0e0icopnf 11496	. . . . . . . . . . . . . . . . 17
67	66	a1i 11	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$ $/\$
68	65, 67	ifclda 3919	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
69	68	ad2antrr 725	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$ $/\$
70		fconstmpt 4980	. . . . . . . . . . . . . . 15
71	70	a1i 11	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
72		eqidd 2452	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
73	55, 57, 69, 71, 72	offval2 6436	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
74		oveq2 6198	. . . . . . . . . . . . . . . 16
75		oveq2 6198	. . . . . . . . . . . . . . . 16
76	74, 75	ifsb 3900	. . . . . . . . . . . . . . 15
77	56	recnd 9513	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$
78	77	adantr 465	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
79	78	mul01d 9669	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$ $/\$
80	79	ifeq2d 3906	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$ $/\$
81	76, 80	syl5eq 2504	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
82	81	mpteq2dv 4477	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
83	73, 82	eqtrd 2492	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
84	83	fveq2d 5793	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
85	68	adantr 465	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
86		eqid 2451	. . . . . . . . . . . . . 14
87	85, 86	fmptd 5966	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$
88	87	adantr 465	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
89		inss2 3669	. . . . . . . . . . . . . . . . . 18
90	89	a1i 11	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$
91	23, 20	mbfdm2 21232	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$
92	8	ffvelrnda 5942	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
93	8	feqmptd 5843	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$
94		simplr 754	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$
95	93, 94	eqeltrrd 2540	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$
96	90, 91, 92, 95	iblss 21398	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$
97	61, 96	iblabs 21422	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
98	62, 63	iblpos 21386	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$ MblFn $/\$
99	97, 98	mpbid 210	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ MblFn $/\$
100	99	simprd 463	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$
101	100	adantr 465	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
102		simplrl 759	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
103		neq0 3745	. . . . . . . . . . . . . . 15
104		0re 9487	. . . . . . . . . . . . . . . . . . 19
105	104	a1i 11	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
106	58	simplbi 460	. . . . . . . . . . . . . . . . . . . 20
107		ffvelrn 5940	. . . . . . . . . . . . . . . . . . . 20 $/\$
108	2, 106, 107	syl2an 477	. . . . . . . . . . . . . . . . . . 19 MblFn $/\$ $/\$ $/\$ $/\$
109	108	abscld 13024	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
110		simplrl 759	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
111	108	absge0d 13032	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
112		simprr 756	. . . . . . . . . . . . . . . . . . 19 MblFn $/\$ $/\$ $/\$
113		fveq2 5789	. . . . . . . . . . . . . . . . . . . . . 22
114	113	fveq2d 5793	. . . . . . . . . . . . . . . . . . . . 21
115	114	breq1d 4400	. . . . . . . . . . . . . . . . . . . 20
116	115	rspccva 3168	. . . . . . . . . . . . . . . . . . 19 $/\$
117	112, 106, 116	syl2an 477	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
118	105, 109, 110, 111, 117	letrd 9629	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
119	118	ex 434	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$
120	119	exlimdv 1691	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
121	103, 120	syl5bi 217	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$
122	121	imp 429	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
123		elrege0 11493	. . . . . . . . . . . . 13 $/\$
124	102, 122, 123	sylanbrc 664	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
125	88, 101, 124	itg2mulc 21341	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
126	84, 125	eqtr3d 2494	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
127	102, 101	remulcld 9515	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
128	126, 127	eqeltrd 2539	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$ $/\$
129	128	ex 434	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
130		noel 3739	. . . . . . . . . . . . . 14
131		eleq2 2524	. . . . . . . . . . . . . 14
132	130, 131	mtbiri 303	. . . . . . . . . . . . 13
133		iffalse 3897	. . . . . . . . . . . . 13
134	132, 133	syl 16	. . . . . . . . . . . 12
135	134	mpteq2dv 4477	. . . . . . . . . . 11
136		fconstmpt 4980	. . . . . . . . . . 11
137	135, 136	syl6eqr 2510	. . . . . . . . . 10
138	137	fveq2d 5793	. . . . . . . . 9
139		itg20 21331	. . . . . . . . . 10
140	139, 104	eqeltri 2535	. . . . . . . . 9
141	138, 140	syl6eqel 2547	. . . . . . . 8
142	129, 141	pm2.61d2 160	. . . . . . 7 MblFn $/\$ $/\$ $/\$
143	110, 62	remulcld 9515	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
144	143	rexrd 9534	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
145	110, 62, 118, 63	mulge0d 10017	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
146		elxrge0 11495	. . . . . . . . . . . 12 $/\$
147	144, 145, 146	sylanbrc 664	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
148	147, 49	ifclda 3919	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
149	148	adantr 465	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$ $/\$
150		eqid 2451	. . . . . . . . 9
151	149, 150	fmptd 5966	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
152	108, 61	absmuld 13042	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
153		abscl 12869	. . . . . . . . . . . . . . . 16
154		absge0 12878	. . . . . . . . . . . . . . . 16
155	153, 154	jca 532	. . . . . . . . . . . . . . 15 $/\$
156	61, 155	syl 16	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$ $/\$
157		lemul1a 10284	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
158	109, 110, 156, 117, 157	syl31anc 1222	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
159	152, 158	eqbrtrd 4410	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
160		iftrue 3895	. . . . . . . . . . . . 13
161	160	adantl 466	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
162		iftrue 3895	. . . . . . . . . . . . 13
163	162	adantl 466	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
164	159, 161, 163	3brtr4d 4420	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
165		0le0 10512	. . . . . . . . . . . . . 14
166	165	a1i 11	. . . . . . . . . . . . 13
167		iffalse 3897	. . . . . . . . . . . . 13
168	166, 167, 133	3brtr4d 4420	. . . . . . . . . . . 12
169	168	adantl 466	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
170	164, 169	pm2.61dan 789	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
171	170	ralrimivw 2823	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
172	54	a1i 11	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
173		eqidd 2452	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
174		eqidd 2452	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
175	172, 51, 149, 173, 174	ofrfval2 6437	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
176	171, 175	mpbird 232	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
177		itg2le 21333	. . . . . . . 8 $/\$ $/\$
178	53, 151, 176, 177	syl3anc 1219	. . . . . . 7 MblFn $/\$ $/\$ $/\$
179		itg2lecl 21332	. . . . . . 7 $/\$ $/\$
180	53, 142, 178, 179	syl3anc 1219	. . . . . 6 MblFn $/\$ $/\$ $/\$
181	43, 45	iblpos 21386	. . . . . 6 MblFn $/\$ $/\$ $/\$ MblFn $/\$
182	42, 180, 181	mpbir2and 913	. . . . 5 MblFn $/\$ $/\$ $/\$
183	20, 23, 182	iblabsr 21423	. . . 4 MblFn $/\$ $/\$ $/\$
184	18, 183	eqeltrd 2539	. . 3 MblFn $/\$ $/\$ $/\$
185	184	rexlimdvaa 2938	. 2 MblFn $/\$
186	185	3impia 1185	1 MblFn $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 369 $/\$ w3a 965

wceq 1370

wex 1587

wcel 1758

wral 2795

wrex 2796

cvv 3068

cin 3425

wss 3426

c0 3735

cif 3889

csn 3975 class class class wbr 4390

cmpt 4448

cxp 4936

cdm 4938

ccom 4942

wfn 5511

wf 5512

cfv 5516 (class class class)co 6190

cof 6418

cofr 6419

cc 9381

cr 9382

cc0 9383

cmul 9388

cpnf 9516

cxr 9518

cle 9520

cico 11403

cicc 11404

cabs 12825

ccncf 20568

cvol 21063 MblFncmbf 21210

citg2 21212

cibl 21213

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-rep 4501 ax-sep 4511 ax-nul 4519 ax-pow 4568 ax-pr 4629 ax-un 6472 ax-inf2 7948 ax-cc 8705 ax-cnex 9439 ax-resscn 9440 ax-1cn 9441 ax-icn 9442 ax-addcl 9443 ax-addrcl 9444 ax-mulcl 9445 ax-mulrcl 9446 ax-mulcom 9447 ax-addass 9448 ax-mulass 9449 ax-distr 9450 ax-i2m1 9451 ax-1ne0 9452 ax-1rid 9453 ax-rnegex 9454 ax-rrecex 9455 ax-cnre 9456 ax-pre-lttri 9457 ax-pre-lttrn 9458 ax-pre-ltadd 9459 ax-pre-mulgt0 9460 ax-pre-sup 9461 ax-addf 9462 ax-mulf 9463

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-fal 1376 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-nel 2647 df-ral 2800 df-rex 2801 df-reu 2802 df-rmo 2803 df-rab 2804 df-v 3070 df-sbc 3285 df-csb 3387 df-dif 3429 df-un 3431 df-in 3433 df-ss 3440 df-pss 3442 df-nul 3736 df-if 3890 df-pw 3960 df-sn 3976 df-pr 3978 df-tp 3980 df-op 3982 df-uni 4190 df-int 4227 df-iun 4271 df-iin 4272 df-disj 4361 df-br 4391 df-opab 4449 df-mpt 4450 df-tr 4484 df-eprel 4730 df-id 4734 df-po 4739 df-so 4740 df-fr 4777 df-se 4778 df-we 4779 df-ord 4820 df-on 4821 df-lim 4822 df-suc 4823 df-xp 4944 df-rel 4945 df-cnv 4946 df-co 4947 df-dm 4948 df-rn 4949 df-res 4950 df-ima 4951 df-iota 5479 df-fun 5518 df-fn 5519 df-f 5520 df-f1 5521 df-fo 5522 df-f1o 5523 df-fv 5524 df-isom 5525 df-riota 6151 df-ov 6193 df-oprab 6194 df-mpt2 6195 df-of 6420 df-ofr 6421 df-om 6577 df-1st 6677 df-2nd 6678 df-supp 6791 df-recs 6932 df-rdg 6966 df-1o 7020 df-2o 7021 df-oadd 7024 df-omul 7025 df-er 7201 df-map 7316 df-pm 7317 df-ixp 7364 df-en 7411 df-dom 7412 df-sdom 7413 df-fin 7414 df-fsupp 7722 df-fi 7762 df-sup 7792 df-oi 7825 df-card 8210 df-acn 8213 df-cda 8438 df-pnf 9521 df-mnf 9522 df-xr 9523 df-ltxr 9524 df-le 9525 df-sub 9698 df-neg 9699 df-div 10095 df-nn 10424 df-2 10481 df-3 10482 df-4 10483 df-5 10484 df-6 10485 df-7 10486 df-8 10487 df-9 10488 df-10 10489 df-n0 10681 df-z 10748 df-dec 10857 df-uz 10963 df-q 11055 df-rp 11093 df-xneg 11190 df-xadd 11191 df-xmul 11192 df-ioo 11405 df-ioc 11406 df-ico 11407 df-icc 11408 df-fz 11539 df-fzo 11650 df-fl 11743 df-mod 11810 df-seq 11908 df-exp 11967 df-hash 12205 df-cj 12690 df-re 12691 df-im 12692 df-sqr 12826 df-abs 12827 df-limsup 13051 df-clim 13068 df-rlim 13069 df-sum 13266 df-struct 14278 df-ndx 14279 df-slot 14280 df-base 14281 df-sets 14282 df-ress 14283 df-plusg 14353 df-mulr 14354 df-starv 14355 df-sca 14356 df-vsca 14357 df-ip 14358 df-tset 14359 df-ple 14360 df-ds 14362 df-unif 14363 df-hom 14364 df-cco 14365 df-rest 14463 df-topn 14464 df-0g 14482 df-gsum 14483 df-topgen 14484 df-pt 14485 df-prds 14488 df-xrs 14542 df-qtop 14547 df-imas 14548 df-xps 14550 df-mre 14626 df-mrc 14627 df-acs 14629 df-mnd 15517 df-submnd 15567 df-mulg 15650 df-cntz 15937 df-cmn 16383 df-psmet 17918 df-xmet 17919 df-met 17920 df-bl 17921 df-mopn 17922 df-cnfld 17928 df-top 18619 df-bases 18621 df-topon 18622 df-topsp 18623 df-cn 18947 df-cnp 18948 df-cmp 19106 df-tx 19251 df-hmeo 19444 df-xms 20011 df-ms 20012 df-tms 20013 df-cncf 20570 df-ovol 21064 df-vol 21065 df-mbf 21215 df-itg1 21216 df-itg2 21217 df-ibl 21218 df-0p 21264

This theorem is referenced by: bddibl 21433 itgsubstlem 21636

W3C validator