itg1climres - Metamath Proof Explorer

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

Theorem itg1climres 22751

Description: Restricting the simple function

to the increasing sequence

of measurable sets whose union is

yields a sequence of simple functions whose integrals approach the integral of

. (Contributed by Mario Carneiro, 15-Aug-2014.)

**Hypotheses**
Ref	Expression
itg1climres.1
itg1climres.2	$/\$
itg1climres.3
itg1climres.4
itg1climres.5

**Assertion**
Ref	Expression
itg1climres

Distinct variable groups:

Allowed substitution hints:

(

)

Proof of Theorem itg1climres Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnuz 11218	. . 3
2		1zzd 10992	. . 3
3		itg1climres.4	. . . . 5
4		i1frn 22714	. . . . 5
5	3, 4	syl 17	. . . 4
6		difss 3549	. . . 4 $\$
7		ssfi 7810	. . . 4 $/\$ $\$ $\$
8	5, 6, 7	sylancl 675	. . 3 $\$
9		1zzd 10992	. . . 4 $/\$ $\$
10		i1fima 22715	. . . . . . . . . . . 12
11	3, 10	syl 17	. . . . . . . . . . 11
12	11	ad2antrr 740	. . . . . . . . . 10 $/\$ $\$ $/\$
13		itg1climres.1	. . . . . . . . . . . 12
14	13	ffvelrnda 6037	. . . . . . . . . . 11 $/\$
15	14	adantlr 729	. . . . . . . . . 10 $/\$ $\$ $/\$
16		inmbl 22574	. . . . . . . . . 10 $/\$
17	12, 15, 16	syl2anc 673	. . . . . . . . 9 $/\$ $\$ $/\$
18		mblvol 22562	. . . . . . . . 9
19	17, 18	syl 17	. . . . . . . 8 $/\$ $\$ $/\$
20		inss1 3643	. . . . . . . . . 10
21	20	a1i 11	. . . . . . . . 9 $/\$ $\$ $/\$
22		mblss 22563	. . . . . . . . . 10
23	12, 22	syl 17	. . . . . . . . 9 $/\$ $\$ $/\$
24		mblvol 22562	. . . . . . . . . . 11
25	12, 24	syl 17	. . . . . . . . . 10 $/\$ $\$ $/\$
26		i1fima2sn 22717	. . . . . . . . . . . 12 $/\$ $\$
27	3, 26	sylan 479	. . . . . . . . . . 11 $/\$ $\$
28	27	adantr 472	. . . . . . . . . 10 $/\$ $\$ $/\$
29	25, 28	eqeltrrd 2550	. . . . . . . . 9 $/\$ $\$ $/\$
30		ovolsscl 22517	. . . . . . . . 9 $/\$ $/\$
31	21, 23, 29, 30	syl3anc 1292	. . . . . . . 8 $/\$ $\$ $/\$
32	19, 31	eqeltrd 2549	. . . . . . 7 $/\$ $\$ $/\$
33		eqid 2471	. . . . . . 7
34	32, 33	fmptd 6061	. . . . . 6 $/\$ $\$
35		itg1climres.2	. . . . . . . . . . . . 13 $/\$
36	35	adantlr 729	. . . . . . . . . . . 12 $/\$ $\$ $/\$
37		sslin 3649	. . . . . . . . . . . 12
38	36, 37	syl 17	. . . . . . . . . . 11 $/\$ $\$ $/\$
39	13	adantr 472	. . . . . . . . . . . . . 14 $/\$ $\$
40		peano2nn 10643	. . . . . . . . . . . . . 14
41		ffvelrn 6035	. . . . . . . . . . . . . 14 $/\$
42	39, 40, 41	syl2an 485	. . . . . . . . . . . . 13 $/\$ $\$ $/\$
43		inmbl 22574	. . . . . . . . . . . . 13 $/\$
44	12, 42, 43	syl2anc 673	. . . . . . . . . . . 12 $/\$ $\$ $/\$
45		mblss 22563	. . . . . . . . . . . 12
46	44, 45	syl 17	. . . . . . . . . . 11 $/\$ $\$ $/\$
47		ovolss 22516	. . . . . . . . . . 11 $/\$
48	38, 46, 47	syl2anc 673	. . . . . . . . . 10 $/\$ $\$ $/\$
49		mblvol 22562	. . . . . . . . . . 11
50	44, 49	syl 17	. . . . . . . . . 10 $/\$ $\$ $/\$
51	48, 19, 50	3brtr4d 4426	. . . . . . . . 9 $/\$ $\$ $/\$
52	51	ralrimiva 2809	. . . . . . . 8 $/\$ $\$
53		fveq2 5879	. . . . . . . . . . . . . 14
54	53	ineq2d 3625	. . . . . . . . . . . . 13
55	54	fveq2d 5883	. . . . . . . . . . . 12
56		fvex 5889	. . . . . . . . . . . 12
57	55, 33, 56	fvmpt 5963	. . . . . . . . . . 11
58		peano2nn 10643	. . . . . . . . . . . 12
59		fveq2 5879	. . . . . . . . . . . . . . 15
60	59	ineq2d 3625	. . . . . . . . . . . . . 14
61	60	fveq2d 5883	. . . . . . . . . . . . 13
62		fvex 5889	. . . . . . . . . . . . 13
63	61, 33, 62	fvmpt 5963	. . . . . . . . . . . 12
64	58, 63	syl 17	. . . . . . . . . . 11
65	57, 64	breq12d 4408	. . . . . . . . . 10
66	65	ralbiia 2822	. . . . . . . . 9
67		oveq1 6315	. . . . . . . . . . . . . 14
68	67	fveq2d 5883	. . . . . . . . . . . . 13
69	68	ineq2d 3625	. . . . . . . . . . . 12
70	69	fveq2d 5883	. . . . . . . . . . 11
71	55, 70	breq12d 4408	. . . . . . . . . 10
72	71	cbvralv 3005	. . . . . . . . 9
73	66, 72	bitr4i 260	. . . . . . . 8
74	52, 73	sylibr 217	. . . . . . 7 $/\$ $\$
75	74	r19.21bi 2776	. . . . . 6 $/\$ $\$ $/\$
76		ovolss 22516	. . . . . . . . . . 11 $/\$
77	20, 23, 76	sylancr 676	. . . . . . . . . 10 $/\$ $\$ $/\$
78	77, 19, 25	3brtr4d 4426	. . . . . . . . 9 $/\$ $\$ $/\$
79	78	ralrimiva 2809	. . . . . . . 8 $/\$ $\$
80	57	breq1d 4405	. . . . . . . . . 10
81	80	ralbiia 2822	. . . . . . . . 9
82	55	breq1d 4405	. . . . . . . . . 10
83	82	cbvralv 3005	. . . . . . . . 9
84	81, 83	bitr4i 260	. . . . . . . 8
85	79, 84	sylibr 217	. . . . . . 7 $/\$ $\$
86		breq2 4399	. . . . . . . . 9
87	86	ralbidv 2829	. . . . . . . 8
88	87	rspcev 3136	. . . . . . 7 $/\$
89	27, 85, 88	syl2anc 673	. . . . . 6 $/\$ $\$
90	1, 9, 34, 75, 89	climsup 13810	. . . . 5 $/\$ $\$
91		eqid 2471	. . . . . . . 8
92	17, 91	fmptd 6061	. . . . . . 7 $/\$ $\$
93	38	ralrimiva 2809	. . . . . . . 8 $/\$ $\$
94		fvex 5889	. . . . . . . . . . . . 13
95	94	inex2 4538	. . . . . . . . . . . 12
96	54, 91, 95	fvmpt 5963	. . . . . . . . . . 11
97		fvex 5889	. . . . . . . . . . . . . 14
98	97	inex2 4538	. . . . . . . . . . . . 13
99	60, 91, 98	fvmpt 5963	. . . . . . . . . . . 12
100	58, 99	syl 17	. . . . . . . . . . 11
101	96, 100	sseq12d 3447	. . . . . . . . . 10
102	101	ralbiia 2822	. . . . . . . . 9
103	54, 69	sseq12d 3447	. . . . . . . . . 10
104	103	cbvralv 3005	. . . . . . . . 9
105	102, 104	bitr4i 260	. . . . . . . 8
106	93, 105	sylibr 217	. . . . . . 7 $/\$ $\$
107		volsup 22588	. . . . . . 7 $/\$
108	92, 106, 107	syl2anc 673	. . . . . 6 $/\$ $\$
109	96	iuneq2i 4288	. . . . . . . . . 10
110	54	cbviunv 4308	. . . . . . . . . 10
111		iunin2 4333	. . . . . . . . . 10
112	109, 110, 111	3eqtr2i 2499	. . . . . . . . 9
113		ffn 5739	. . . . . . . . . . . . . 14
114		fniunfv 6170	. . . . . . . . . . . . . 14
115	13, 113, 114	3syl 18	. . . . . . . . . . . . 13
116		itg1climres.3	. . . . . . . . . . . . 13
117	115, 116	eqtrd 2505	. . . . . . . . . . . 12
118	117	adantr 472	. . . . . . . . . . 11 $/\$ $\$
119	118	ineq2d 3625	. . . . . . . . . 10 $/\$ $\$
120	11	adantr 472	. . . . . . . . . . . 12 $/\$ $\$
121	120, 22	syl 17	. . . . . . . . . . 11 $/\$ $\$
122		df-ss 3404	. . . . . . . . . . 11
123	121, 122	sylib 201	. . . . . . . . . 10 $/\$ $\$
124	119, 123	eqtrd 2505	. . . . . . . . 9 $/\$ $\$
125	112, 124	syl5eq 2517	. . . . . . . 8 $/\$ $\$
126		ffn 5739	. . . . . . . . 9
127		fniunfv 6170	. . . . . . . . 9
128	92, 126, 127	3syl 18	. . . . . . . 8 $/\$ $\$
129	125, 128	eqtr3d 2507	. . . . . . 7 $/\$ $\$
130	129	fveq2d 5883	. . . . . 6 $/\$ $\$
131		frn 5747	. . . . . . . . 9
132	34, 131	syl 17	. . . . . . . 8 $/\$ $\$
133		fdm 5745	. . . . . . . . . . 11
134	34, 133	syl 17	. . . . . . . . . 10 $/\$ $\$
135		1nn 10642	. . . . . . . . . . 11
136		ne0i 3728	. . . . . . . . . . 11
137	135, 136	mp1i 13	. . . . . . . . . 10 $/\$ $\$
138	134, 137	eqnetrd 2710	. . . . . . . . 9 $/\$ $\$
139		dm0rn0 5057	. . . . . . . . . 10
140	139	necon3bii 2695	. . . . . . . . 9
141	138, 140	sylib 201	. . . . . . . 8 $/\$ $\$
142		ffn 5739	. . . . . . . . . . 11
143		breq1 4398	. . . . . . . . . . . 12
144	143	ralrn 6040	. . . . . . . . . . 11
145	34, 142, 144	3syl 18	. . . . . . . . . 10 $/\$ $\$
146	145	rexbidv 2892	. . . . . . . . 9 $/\$ $\$
147	89, 146	mpbird 240	. . . . . . . 8 $/\$ $\$
148		supxrre 11638	. . . . . . . 8 $/\$ $/\$
149	132, 141, 147, 148	syl3anc 1292	. . . . . . 7 $/\$ $\$
150		rnco2 5349	. . . . . . . . 9
151		eqidd 2472	. . . . . . . . . . 11 $/\$ $\$
152		volf 22561	. . . . . . . . . . . . 13
153	152	a1i 11	. . . . . . . . . . . 12 $/\$ $\$
154	153	feqmptd 5932	. . . . . . . . . . 11 $/\$ $\$
155		fveq2 5879	. . . . . . . . . . 11
156	17, 151, 154, 155	fmptco 6072	. . . . . . . . . 10 $/\$ $\$
157	156	rneqd 5068	. . . . . . . . 9 $/\$ $\$
158	150, 157	syl5reqr 2520	. . . . . . . 8 $/\$ $\$
159	158	supeq1d 7978	. . . . . . 7 $/\$ $\$
160	149, 159	eqtr3d 2507	. . . . . 6 $/\$ $\$
161	108, 130, 160	3eqtr4d 2515	. . . . 5 $/\$ $\$
162	90, 161	breqtrrd 4422	. . . 4 $/\$ $\$
163		i1ff 22713	. . . . . . . 8
164		frn 5747	. . . . . . . 8
165	3, 163, 164	3syl 18	. . . . . . 7
166	165	ssdifssd 3560	. . . . . 6 $\$
167	166	sselda 3418	. . . . 5 $/\$ $\$
168	167	recnd 9687	. . . 4 $/\$ $\$
169		nnex 10637	. . . . . 6
170	169	mptex 6152	. . . . 5
171	170	a1i 11	. . . 4 $/\$ $\$
172	34	ffvelrnda 6037	. . . . 5 $/\$ $\$ $/\$
173	172	recnd 9687	. . . 4 $/\$ $\$ $/\$
174	55	oveq2d 6324	. . . . . . 7
175		eqid 2471	. . . . . . 7
176		ovex 6336	. . . . . . 7
177	174, 175, 176	fvmpt 5963	. . . . . 6
178	57	oveq2d 6324	. . . . . 6
179	177, 178	eqtr4d 2508	. . . . 5
180	179	adantl 473	. . . 4 $/\$ $\$ $/\$
181	1, 9, 162, 168, 171, 173, 180	climmulc2 13777	. . 3 $/\$ $\$
182	169	mptex 6152	. . . 4
183	182	a1i 11	. . 3
184	167	adantr 472	. . . . . . . 8 $/\$ $\$ $/\$
185	184, 32	remulcld 9689	. . . . . . 7 $/\$ $\$ $/\$
186	185, 175	fmptd 6061	. . . . . 6 $/\$ $\$
187	186	ffvelrnda 6037	. . . . 5 $/\$ $\$ $/\$
188	187	recnd 9687	. . . 4 $/\$ $\$ $/\$
189	188	anasss 659	. . 3 $/\$ $\$ $/\$
190	3	adantr 472	. . . . . . . . 9 $/\$
191		itg1climres.5	. . . . . . . . . 10
192	191	i1fres 22742	. . . . . . . . 9 $/\$
193	190, 14, 192	syl2anc 673	. . . . . . . 8 $/\$
194	8	adantr 472	. . . . . . . 8 $/\$ $\$
195		ffn 5739	. . . . . . . . . . . . . 14
196	3, 163, 195	3syl 18	. . . . . . . . . . . . 13
197	196	adantr 472	. . . . . . . . . . . 12 $/\$
198		fnfvelrn 6034	. . . . . . . . . . . 12 $/\$
199	197, 198	sylan 479	. . . . . . . . . . 11 $/\$ $/\$
200		i1f0rn 22719	. . . . . . . . . . . . 13
201	3, 200	syl 17	. . . . . . . . . . . 12
202	201	ad2antrr 740	. . . . . . . . . . 11 $/\$ $/\$
203	199, 202	ifcld 3915	. . . . . . . . . 10 $/\$ $/\$
204	203, 191	fmptd 6061	. . . . . . . . 9 $/\$
205		frn 5747	. . . . . . . . 9
206		ssdif 3557	. . . . . . . . 9 $\$ $\$
207	204, 205, 206	3syl 18	. . . . . . . 8 $/\$ $\$ $\$
208	165	adantr 472	. . . . . . . . 9 $/\$
209	208	ssdifd 3558	. . . . . . . 8 $/\$ $\$ $\$
210		itg1val2 22721	. . . . . . . 8 $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$
211	193, 194, 207, 209, 210	syl13anc 1294	. . . . . . 7 $/\$ $\$
212		fvex 5889	. . . . . . . . . . . . . . . . . . . . 21
213		c0ex 9655	. . . . . . . . . . . . . . . . . . . . 21
214	212, 213	ifex 3940	. . . . . . . . . . . . . . . . . . . 20
215	191	fvmpt2 5972	. . . . . . . . . . . . . . . . . . . 20 $/\$
216	214, 215	mpan2 685	. . . . . . . . . . . . . . . . . . 19
217	216	adantl 473	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $/\$
218	217	eqeq1d 2473	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $/\$
219		eldifsni 4089	. . . . . . . . . . . . . . . . . . . . 21 $\$
220	219	ad2antlr 741	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $/\$
221		neeq1 2705	. . . . . . . . . . . . . . . . . . . 20
222	220, 221	syl5ibrcom 230	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\$ $/\$
223		iffalse 3881	. . . . . . . . . . . . . . . . . . . 20
224	223	necon1ai 2670	. . . . . . . . . . . . . . . . . . 19
225	222, 224	syl6 33	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $/\$
226	225	pm4.71rd 647	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $/\$ $/\$
227	218, 226	bitrd 261	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$ $/\$
228		iftrue 3878	. . . . . . . . . . . . . . . . . . 19
229	228	eqeq1d 2473	. . . . . . . . . . . . . . . . . 18
230	229	pm5.32i 649	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
231		ancom 457	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
232	230, 231	bitri 257	. . . . . . . . . . . . . . . 16 $/\$ $/\$
233	227, 232	syl6bb 269	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $/\$ $/\$
234	233	pm5.32da 653	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $/\$ $/\$ $/\$
235		anass 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
236	234, 235	syl6bbr 271	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $/\$ $/\$
237		i1ff 22713	. . . . . . . . . . . . . . . 16
238		ffn 5739	. . . . . . . . . . . . . . . 16
239	193, 237, 238	3syl 18	. . . . . . . . . . . . . . 15 $/\$
240	239	adantr 472	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
241		fniniseg 6018	. . . . . . . . . . . . . 14 $/\$
242	240, 241	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$
243		elin 3608	. . . . . . . . . . . . . 14 $/\$
244	197	adantr 472	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
245		fniniseg 6018	. . . . . . . . . . . . . . . 16 $/\$
246	244, 245	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $/\$
247	246	anbi1d 719	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $/\$ $/\$ $/\$
248	243, 247	syl5bb 265	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $/\$
249	236, 242, 248	3bitr4d 293	. . . . . . . . . . . 12 $/\$ $/\$ $\$
250	249	alrimiv 1781	. . . . . . . . . . 11 $/\$ $/\$ $\$
251		nfmpt1 4485	. . . . . . . . . . . . . . 15
252	191, 251	nfcxfr 2610	. . . . . . . . . . . . . 14
253	252	nfcnv 5018	. . . . . . . . . . . . 13
254		nfcv 2612	. . . . . . . . . . . . 13
255	253, 254	nfima 5182	. . . . . . . . . . . 12
256		nfcv 2612	. . . . . . . . . . . 12
257	255, 256	cleqf 2637	. . . . . . . . . . 11
258	250, 257	sylibr 217	. . . . . . . . . 10 $/\$ $/\$ $\$
259	258	fveq2d 5883	. . . . . . . . 9 $/\$ $/\$ $\$
260	259	oveq2d 6324	. . . . . . . 8 $/\$ $/\$ $\$
261	260	sumeq2dv 13846	. . . . . . 7 $/\$ $\$ $\$
262	211, 261	eqtrd 2505	. . . . . 6 $/\$ $\$
263	262	mpteq2dva 4482	. . . . 5 $\$
264	263	fveq1d 5881	. . . 4 $\$
265	174	sumeq2sdv 13847	. . . . . 6 $\$ $\$
266		eqid 2471	. . . . . 6 $\$ $\$
267		sumex 13831	. . . . . 6 $\$
268	265, 266, 267	fvmpt 5963	. . . . 5 $\$ $\$
269	177	sumeq2sdv 13847	. . . . 5 $\$ $\$
270	268, 269	eqtr4d 2508	. . . 4 $\$ $\$
271	264, 270	sylan9eq 2525	. . 3 $/\$ $\$
272	1, 2, 8, 181, 183, 189, 271	climfsum 13957	. 2 $\$
273		itg1val 22720	. . 3 $\$
274	3, 273	syl 17	. 2 $\$
275	272, 274	breqtrrd 4422	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $/\$ wa 376

wal 1450

wceq 1452

wcel 1904

wne 2641

wral 2756

wrex 2757

cvv 3031 $\$ cdif 3387

cin 3389

wss 3390

c0 3722

cif 3872

csn 3959

cuni 4190

ciun 4269 class class class wbr 4395

cmpt 4454

ccnv 4838

cdm 4839

crn 4840

cima 4842

ccom 4843

wfn 5584

wf 5585

cfv 5589 (class class class)co 6308

cfn 7587

csup 7972

cc 9555

cr 9556

cc0 9557

c1 9558

caddc 9560

cmul 9562

cpnf 9690

cxr 9692

clt 9693

cle 9694

cn 10631

cicc 11663

cli 13625

csu 13829

covol 22491

cvol 22493

citg1 22652

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cc 8883 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635 ax-addf 9636

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-disj 4367 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-of 6550 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-er 7381 df-map 7492 df-pm 7493 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-fi 7943 df-sup 7974 df-inf 7975 df-oi 8043 df-card 8391 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-n0 10894 df-z 10962 df-uz 11183 df-q 11288 df-rp 11326 df-xneg 11432 df-xadd 11433 df-xmul 11434 df-ioo 11664 df-ico 11666 df-icc 11667 df-fz 11811 df-fzo 11943 df-fl 12061 df-seq 12252 df-exp 12311 df-hash 12554 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-clim 13629 df-rlim 13630 df-sum 13830 df-rest 15399 df-topgen 15420 df-psmet 19039 df-xmet 19040 df-met 19041 df-bl 19042 df-mopn 19043 df-top 19998 df-bases 19999 df-topon 20000 df-cmp 20479 df-ovol 22494 df-vol 22496 df-mbf 22656 df-itg1 22657

This theorem is referenced by: itg2monolem1 22787

W3C validator