bddmulibl - Metamath Proof Explorer

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

Theorem bddmulibl 21158

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 20947	. . . . . . 7 MblFn
2	1	ad2antrr 718	. . . . . 6 MblFn $/\$ $/\$ $/\$
3		ffn 5547	. . . . . 6
4	2, 3	syl 16	. . . . 5 MblFn $/\$ $/\$ $/\$
5		iblmbf 21087	. . . . . . . 8 MblFn
6	5	ad2antlr 719	. . . . . . 7 MblFn $/\$ $/\$ $/\$ MblFn
7		mbff 20947	. . . . . . 7 MblFn
8	6, 7	syl 16	. . . . . 6 MblFn $/\$ $/\$ $/\$
9		ffn 5547	. . . . . 6
10	8, 9	syl 16	. . . . 5 MblFn $/\$ $/\$ $/\$
11		mbfdm 20948	. . . . . 6 MblFn
12	11	ad2antrr 718	. . . . 5 MblFn $/\$ $/\$ $/\$
13		mbfdm 20948	. . . . . 6 MblFn
14	6, 13	syl 16	. . . . 5 MblFn $/\$ $/\$ $/\$
15		eqid 2433	. . . . 5
16		eqidd 2434	. . . . 5 MblFn $/\$ $/\$ $/\$ $/\$
17		eqidd 2434	. . . . 5 MblFn $/\$ $/\$ $/\$ $/\$
18	4, 10, 12, 14, 15, 16, 17	offval 6316	. . . 4 MblFn $/\$ $/\$ $/\$
19		ovex 6105	. . . . . 6
20	19	a1i 11	. . . . 5 MblFn $/\$ $/\$ $/\$ $/\$
21		simpll 746	. . . . . . 7 MblFn $/\$ $/\$ $/\$ MblFn
22	21, 6	mbfmul 21046	. . . . . 6 MblFn $/\$ $/\$ $/\$ MblFn
23	18, 22	eqeltrrd 2508	. . . . 5 MblFn $/\$ $/\$ $/\$ MblFn
24	23, 20	mbfmptcl 20957	. . . . . . . 8 MblFn $/\$ $/\$ $/\$ $/\$
25		eqidd 2434	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
26		absf 12809	. . . . . . . . . 10
27	26	a1i 11	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
28	27	feqmptd 5732	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
29		fveq2 5679	. . . . . . . 8
30	24, 25, 28, 29	fmptco 5863	. . . . . . 7 MblFn $/\$ $/\$ $/\$
31		eqid 2433	. . . . . . . . 9
32	24, 31	fmptd 5855	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
33		ax-resscn 9327	. . . . . . . . . . 11
34		ssid 3363	. . . . . . . . . . 11
35		cncfss 20317	. . . . . . . . . . 11 $/\$
36	33, 34, 35	mp2an 665	. . . . . . . . . 10
37		abscncf 20319	. . . . . . . . . 10
38	36, 37	sselii 3341	. . . . . . . . 9
39	38	a1i 11	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
40		cncombf 20978	. . . . . . . 8 MblFn $/\$ $/\$ MblFn
41	23, 32, 39, 40	syl3anc 1211	. . . . . . 7 MblFn $/\$ $/\$ $/\$ MblFn
42	30, 41	eqeltrrd 2508	. . . . . 6 MblFn $/\$ $/\$ $/\$ MblFn
43	24	abscld 12906	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
44	43	rexrd 9421	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
45	24	absge0d 12914	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
46		elxrge0 11381	. . . . . . . . . . 11 $/\$
47	44, 45, 46	sylanbrc 657	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
48		0e0iccpnf 11383	. . . . . . . . . . 11
49	48	a1i 11	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
50	47, 49	ifclda 3809	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
51	50	adantr 462	. . . . . . . 8 MblFn $/\$ $/\$ $/\$ $/\$
52		eqid 2433	. . . . . . . 8
53	51, 52	fmptd 5855	. . . . . . 7 MblFn $/\$ $/\$ $/\$
54		reex 9361	. . . . . . . . . . . . . . 15
55	54	a1i 11	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
56		simprl 748	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
57	56	ad2antrr 718	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$ $/\$
58		elin 3527	. . . . . . . . . . . . . . . . . . . 20 $/\$
59	58	simprbi 461	. . . . . . . . . . . . . . . . . . 19
60		ffvelrn 5829	. . . . . . . . . . . . . . . . . . 19 $/\$
61	8, 59, 60	syl2an 474	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
62	61	abscld 12906	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
63	61	absge0d 12914	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
64		elrege0 11380	. . . . . . . . . . . . . . . . 17 $/\$
65	62, 63, 64	sylanbrc 657	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$ $/\$
66		0e0icopnf 11382	. . . . . . . . . . . . . . . . 17
67	66	a1i 11	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$ $/\$
68	65, 67	ifclda 3809	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
69	68	ad2antrr 718	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$ $/\$
70		fconstmpt 4869	. . . . . . . . . . . . . . 15
71	70	a1i 11	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
72		eqidd 2434	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
73	55, 57, 69, 71, 72	offval2 6325	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
74		oveq2 6088	. . . . . . . . . . . . . . . 16
75		oveq2 6088	. . . . . . . . . . . . . . . 16
76	74, 75	ifsb 3790	. . . . . . . . . . . . . . 15
77	56	recnd 9400	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$
78	77	adantr 462	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
79	78	mul01d 9556	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$ $/\$
80	79	ifeq2d 3796	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$ $/\$
81	76, 80	syl5eq 2477	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
82	81	mpteq2dv 4367	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
83	73, 82	eqtrd 2465	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
84	83	fveq2d 5683	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
85	68	adantr 462	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
86		eqid 2433	. . . . . . . . . . . . . 14
87	85, 86	fmptd 5855	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$
88	87	adantr 462	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
89		inss2 3559	. . . . . . . . . . . . . . . . . 18
90	89	a1i 11	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$
91	23, 20	mbfdm2 20958	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$
92	8	ffvelrnda 5831	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
93	8	feqmptd 5732	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$
94		simplr 747	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$
95	93, 94	eqeltrrd 2508	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$
96	90, 91, 92, 95	iblss 21124	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$
97	61, 96	iblabs 21148	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
98	62, 63	iblpos 21112	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$ MblFn $/\$
99	97, 98	mpbid 210	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ MblFn $/\$
100	99	simprd 460	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$
101	100	adantr 462	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
102		simplrl 752	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
103		neq0 3635	. . . . . . . . . . . . . . 15
104		0re 9374	. . . . . . . . . . . . . . . . . . 19
105	104	a1i 11	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
106	58	simplbi 457	. . . . . . . . . . . . . . . . . . . 20
107		ffvelrn 5829	. . . . . . . . . . . . . . . . . . . 20 $/\$
108	2, 106, 107	syl2an 474	. . . . . . . . . . . . . . . . . . 19 MblFn $/\$ $/\$ $/\$ $/\$
109	108	abscld 12906	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
110		simplrl 752	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
111	108	absge0d 12914	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
112		simprr 749	. . . . . . . . . . . . . . . . . . 19 MblFn $/\$ $/\$ $/\$
113		fveq2 5679	. . . . . . . . . . . . . . . . . . . . . 22
114	113	fveq2d 5683	. . . . . . . . . . . . . . . . . . . . 21
115	114	breq1d 4290	. . . . . . . . . . . . . . . . . . . 20
116	115	rspccva 3061	. . . . . . . . . . . . . . . . . . 19 $/\$
117	112, 106, 116	syl2an 474	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
118	105, 109, 110, 111, 117	letrd 9516	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
119	118	ex 434	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$
120	119	exlimdv 1689	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
121	103, 120	syl5bi 217	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$
122	121	imp 429	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
123		elrege0 11380	. . . . . . . . . . . . 13 $/\$
124	102, 122, 123	sylanbrc 657	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
125	88, 101, 124	itg2mulc 21067	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
126	84, 125	eqtr3d 2467	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
127	102, 101	remulcld 9402	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
128	126, 127	eqeltrd 2507	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$ $/\$
129	128	ex 434	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
130		noel 3629	. . . . . . . . . . . . . 14
131		eleq2 2494	. . . . . . . . . . . . . 14
132	130, 131	mtbiri 303	. . . . . . . . . . . . 13
133		iffalse 3787	. . . . . . . . . . . . 13
134	132, 133	syl 16	. . . . . . . . . . . 12
135	134	mpteq2dv 4367	. . . . . . . . . . 11
136		fconstmpt 4869	. . . . . . . . . . 11
137	135, 136	syl6eqr 2483	. . . . . . . . . 10
138	137	fveq2d 5683	. . . . . . . . 9
139		itg20 21057	. . . . . . . . . 10
140	139, 104	eqeltri 2503	. . . . . . . . 9
141	138, 140	syl6eqel 2521	. . . . . . . 8
142	129, 141	pm2.61d2 160	. . . . . . 7 MblFn $/\$ $/\$ $/\$
143	110, 62	remulcld 9402	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
144	143	rexrd 9421	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
145	110, 62, 118, 63	mulge0d 9904	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
146		elxrge0 11381	. . . . . . . . . . . 12 $/\$
147	144, 145, 146	sylanbrc 657	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
148	147, 49	ifclda 3809	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
149	148	adantr 462	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$ $/\$
150		eqid 2433	. . . . . . . . 9
151	149, 150	fmptd 5855	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
152	108, 61	absmuld 12924	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
153		abscl 12751	. . . . . . . . . . . . . . . 16
154		absge0 12760	. . . . . . . . . . . . . . . 16
155	153, 154	jca 529	. . . . . . . . . . . . . . 15 $/\$
156	61, 155	syl 16	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$ $/\$
157		lemul1a 10171	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
158	109, 110, 156, 117, 157	syl31anc 1214	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
159	152, 158	eqbrtrd 4300	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
160		iftrue 3785	. . . . . . . . . . . . 13
161	160	adantl 463	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
162		iftrue 3785	. . . . . . . . . . . . 13
163	162	adantl 463	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
164	159, 161, 163	3brtr4d 4310	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
165		0le0 10399	. . . . . . . . . . . . . 14
166	165	a1i 11	. . . . . . . . . . . . 13
167		iffalse 3787	. . . . . . . . . . . . 13
168	166, 167, 133	3brtr4d 4310	. . . . . . . . . . . 12
169	168	adantl 463	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
170	164, 169	pm2.61dan 782	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
171	170	ralrimivw 2790	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
172	54	a1i 11	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
173		eqidd 2434	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
174		eqidd 2434	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
175	172, 51, 149, 173, 174	ofrfval2 6326	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
176	171, 175	mpbird 232	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
177		itg2le 21059	. . . . . . . 8 $/\$ $/\$
178	53, 151, 176, 177	syl3anc 1211	. . . . . . 7 MblFn $/\$ $/\$ $/\$
179		itg2lecl 21058	. . . . . . 7 $/\$ $/\$
180	53, 142, 178, 179	syl3anc 1211	. . . . . 6 MblFn $/\$ $/\$ $/\$
181	43, 45	iblpos 21112	. . . . . 6 MblFn $/\$ $/\$ $/\$ MblFn $/\$
182	42, 180, 181	mpbir2and 906	. . . . 5 MblFn $/\$ $/\$ $/\$
183	20, 23, 182	iblabsr 21149	. . . 4 MblFn $/\$ $/\$ $/\$
184	18, 183	eqeltrd 2507	. . 3 MblFn $/\$ $/\$ $/\$
185	184	rexlimdvaa 2832	. 2 MblFn $/\$
186	185	3impia 1177	1 MblFn $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

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

wceq 1362

wex 1589

wcel 1755

wral 2705

wrex 2706

cvv 2962

cin 3315

wss 3316

c0 3625

cif 3779

csn 3865 class class class wbr 4280

cmpt 4338

cxp 4825

cdm 4827

ccom 4831

wfn 5401

wf 5402

cfv 5406 (class class class)co 6080

cof 6307

cofr 6308

cc 9268

cr 9269

cc0 9270

cmul 9275

cpnf 9403

cxr 9405

cle 9407

cico 11290

cicc 11291

cabs 12707

ccncf 20294

cvol 20789 MblFncmbf 20936

citg2 20938

cibl 20939

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1594 ax-4 1605 ax-5 1669 ax-6 1707 ax-7 1727 ax-8 1757 ax-9 1759 ax-10 1774 ax-11 1779 ax-12 1791 ax-13 1942 ax-ext 2414 ax-rep 4391 ax-sep 4401 ax-nul 4409 ax-pow 4458 ax-pr 4519 ax-un 6361 ax-inf2 7835 ax-cc 8592 ax-cnex 9326 ax-resscn 9327 ax-1cn 9328 ax-icn 9329 ax-addcl 9330 ax-addrcl 9331 ax-mulcl 9332 ax-mulrcl 9333 ax-mulcom 9334 ax-addass 9335 ax-mulass 9336 ax-distr 9337 ax-i2m1 9338 ax-1ne0 9339 ax-1rid 9340 ax-rnegex 9341 ax-rrecex 9342 ax-cnre 9343 ax-pre-lttri 9344 ax-pre-lttrn 9345 ax-pre-ltadd 9346 ax-pre-mulgt0 9347 ax-pre-sup 9348 ax-addf 9349 ax-mulf 9350

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 959 df-3an 960 df-tru 1365 df-fal 1368 df-ex 1590 df-nf 1593 df-sb 1700 df-eu 2258 df-mo 2259 df-clab 2420 df-cleq 2426 df-clel 2429 df-nfc 2558 df-ne 2598 df-nel 2599 df-ral 2710 df-rex 2711 df-reu 2712 df-rmo 2713 df-rab 2714 df-v 2964 df-sbc 3176 df-csb 3277 df-dif 3319 df-un 3321 df-in 3323 df-ss 3330 df-pss 3332 df-nul 3626 df-if 3780 df-pw 3850 df-sn 3866 df-pr 3868 df-tp 3870 df-op 3872 df-uni 4080 df-int 4117 df-iun 4161 df-iin 4162 df-disj 4251 df-br 4281 df-opab 4339 df-mpt 4340 df-tr 4374 df-eprel 4619 df-id 4623 df-po 4628 df-so 4629 df-fr 4666 df-se 4667 df-we 4668 df-ord 4709 df-on 4710 df-lim 4711 df-suc 4712 df-xp 4833 df-rel 4834 df-cnv 4835 df-co 4836 df-dm 4837 df-rn 4838 df-res 4839 df-ima 4840 df-iota 5369 df-fun 5408 df-fn 5409 df-f 5410 df-f1 5411 df-fo 5412 df-f1o 5413 df-fv 5414 df-isom 5415 df-riota 6039 df-ov 6083 df-oprab 6084 df-mpt2 6085 df-of 6309 df-ofr 6310 df-om 6466 df-1st 6566 df-2nd 6567 df-supp 6680 df-recs 6818 df-rdg 6852 df-1o 6908 df-2o 6909 df-oadd 6912 df-omul 6913 df-er 7089 df-map 7204 df-pm 7205 df-ixp 7252 df-en 7299 df-dom 7300 df-sdom 7301 df-fin 7302 df-fsupp 7609 df-fi 7649 df-sup 7679 df-oi 7712 df-card 8097 df-acn 8100 df-cda 8325 df-pnf 9408 df-mnf 9409 df-xr 9410 df-ltxr 9411 df-le 9412 df-sub 9585 df-neg 9586 df-div 9982 df-nn 10311 df-2 10368 df-3 10369 df-4 10370 df-5 10371 df-6 10372 df-7 10373 df-8 10374 df-9 10375 df-10 10376 df-n0 10568 df-z 10635 df-dec 10744 df-uz 10850 df-q 10942 df-rp 10980 df-xneg 11077 df-xadd 11078 df-xmul 11079 df-ioo 11292 df-ioc 11293 df-ico 11294 df-icc 11295 df-fz 11425 df-fzo 11533 df-fl 11626 df-mod 11693 df-seq 11791 df-exp 11850 df-hash 12088 df-cj 12572 df-re 12573 df-im 12574 df-sqr 12708 df-abs 12709 df-limsup 12933 df-clim 12950 df-rlim 12951 df-sum 13148 df-struct 14159 df-ndx 14160 df-slot 14161 df-base 14162 df-sets 14163 df-ress 14164 df-plusg 14234 df-mulr 14235 df-starv 14236 df-sca 14237 df-vsca 14238 df-ip 14239 df-tset 14240 df-ple 14241 df-ds 14243 df-unif 14244 df-hom 14245 df-cco 14246 df-rest 14344 df-topn 14345 df-0g 14363 df-gsum 14364 df-topgen 14365 df-pt 14366 df-prds 14369 df-xrs 14423 df-qtop 14428 df-imas 14429 df-xps 14431 df-mre 14507 df-mrc 14508 df-acs 14510 df-mnd 15398 df-submnd 15448 df-mulg 15528 df-cntz 15815 df-cmn 16259 df-psmet 17653 df-xmet 17654 df-met 17655 df-bl 17656 df-mopn 17657 df-cnfld 17663 df-top 18345 df-bases 18347 df-topon 18348 df-topsp 18349 df-cn 18673 df-cnp 18674 df-cmp 18832 df-tx 18977 df-hmeo 19170 df-xms 19737 df-ms 19738 df-tms 19739 df-cncf 20296 df-ovol 20790 df-vol 20791 df-mbf 20941 df-itg1 20942 df-itg2 20943 df-ibl 20944 df-0p 20990

This theorem is referenced by: bddibl 21159 itgsubstlem 21362

W3C validator