itg1climres - Metamath Proof Explorer

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

Theorem itg1climres 21853

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 11113	. . 3
2		1zzd 10891	. . 3
3		itg1climres.4	. . . . 5
4		i1frn 21816	. . . . 5
5	3, 4	syl 16	. . . 4
6		difss 3631	. . . 4 $\$
7		ssfi 7737	. . . 4 $/\$ $\$ $\$
8	5, 6, 7	sylancl 662	. . 3 $\$
9		1zzd 10891	. . . 4 $/\$ $\$
10		i1fima 21817	. . . . . . . . . . . 12
11	3, 10	syl 16	. . . . . . . . . . 11
12	11	ad2antrr 725	. . . . . . . . . 10 $/\$ $\$ $/\$
13		itg1climres.1	. . . . . . . . . . . 12
14	13	ffvelrnda 6019	. . . . . . . . . . 11 $/\$
15	14	adantlr 714	. . . . . . . . . 10 $/\$ $\$ $/\$
16		inmbl 21684	. . . . . . . . . 10 $/\$
17	12, 15, 16	syl2anc 661	. . . . . . . . 9 $/\$ $\$ $/\$
18		mblvol 21673	. . . . . . . . 9
19	17, 18	syl 16	. . . . . . . 8 $/\$ $\$ $/\$
20		inss1 3718	. . . . . . . . . 10
21	20	a1i 11	. . . . . . . . 9 $/\$ $\$ $/\$
22		mblss 21674	. . . . . . . . . 10
23	12, 22	syl 16	. . . . . . . . 9 $/\$ $\$ $/\$
24		mblvol 21673	. . . . . . . . . . 11
25	12, 24	syl 16	. . . . . . . . . 10 $/\$ $\$ $/\$
26		i1fima2sn 21819	. . . . . . . . . . . 12 $/\$ $\$
27	3, 26	sylan 471	. . . . . . . . . . 11 $/\$ $\$
28	27	adantr 465	. . . . . . . . . 10 $/\$ $\$ $/\$
29	25, 28	eqeltrrd 2556	. . . . . . . . 9 $/\$ $\$ $/\$
30		ovolsscl 21629	. . . . . . . . 9 $/\$ $/\$
31	21, 23, 29, 30	syl3anc 1228	. . . . . . . 8 $/\$ $\$ $/\$
32	19, 31	eqeltrd 2555	. . . . . . 7 $/\$ $\$ $/\$
33		eqid 2467	. . . . . . 7
34	32, 33	fmptd 6043	. . . . . 6 $/\$ $\$
35		itg1climres.2	. . . . . . . . . . . . 13 $/\$
36	35	adantlr 714	. . . . . . . . . . . 12 $/\$ $\$ $/\$
37		sslin 3724	. . . . . . . . . . . 12
38	36, 37	syl 16	. . . . . . . . . . 11 $/\$ $\$ $/\$
39	13	adantr 465	. . . . . . . . . . . . . 14 $/\$ $\$
40		peano2nn 10544	. . . . . . . . . . . . . 14
41		ffvelrn 6017	. . . . . . . . . . . . . 14 $/\$
42	39, 40, 41	syl2an 477	. . . . . . . . . . . . 13 $/\$ $\$ $/\$
43		inmbl 21684	. . . . . . . . . . . . 13 $/\$
44	12, 42, 43	syl2anc 661	. . . . . . . . . . . 12 $/\$ $\$ $/\$
45		mblss 21674	. . . . . . . . . . . 12
46	44, 45	syl 16	. . . . . . . . . . 11 $/\$ $\$ $/\$
47		ovolss 21628	. . . . . . . . . . 11 $/\$
48	38, 46, 47	syl2anc 661	. . . . . . . . . 10 $/\$ $\$ $/\$
49		mblvol 21673	. . . . . . . . . . 11
50	44, 49	syl 16	. . . . . . . . . 10 $/\$ $\$ $/\$
51	48, 19, 50	3brtr4d 4477	. . . . . . . . 9 $/\$ $\$ $/\$
52	51	ralrimiva 2878	. . . . . . . 8 $/\$ $\$
53		fveq2 5864	. . . . . . . . . . . . . 14
54	53	ineq2d 3700	. . . . . . . . . . . . 13
55	54	fveq2d 5868	. . . . . . . . . . . 12
56		fvex 5874	. . . . . . . . . . . 12
57	55, 33, 56	fvmpt 5948	. . . . . . . . . . 11
58		peano2nn 10544	. . . . . . . . . . . 12
59		fveq2 5864	. . . . . . . . . . . . . . 15
60	59	ineq2d 3700	. . . . . . . . . . . . . 14
61	60	fveq2d 5868	. . . . . . . . . . . . 13
62		fvex 5874	. . . . . . . . . . . . 13
63	61, 33, 62	fvmpt 5948	. . . . . . . . . . . 12
64	58, 63	syl 16	. . . . . . . . . . 11
65	57, 64	breq12d 4460	. . . . . . . . . 10
66	65	ralbiia 2894	. . . . . . . . 9
67		oveq1 6289	. . . . . . . . . . . . . 14
68	67	fveq2d 5868	. . . . . . . . . . . . 13
69	68	ineq2d 3700	. . . . . . . . . . . 12
70	69	fveq2d 5868	. . . . . . . . . . 11
71	55, 70	breq12d 4460	. . . . . . . . . 10
72	71	cbvralv 3088	. . . . . . . . 9
73	66, 72	bitr4i 252	. . . . . . . 8
74	52, 73	sylibr 212	. . . . . . 7 $/\$ $\$
75	74	r19.21bi 2833	. . . . . 6 $/\$ $\$ $/\$
76		ovolss 21628	. . . . . . . . . . 11 $/\$
77	20, 23, 76	sylancr 663	. . . . . . . . . 10 $/\$ $\$ $/\$
78	77, 19, 25	3brtr4d 4477	. . . . . . . . 9 $/\$ $\$ $/\$
79	78	ralrimiva 2878	. . . . . . . 8 $/\$ $\$
80	57	breq1d 4457	. . . . . . . . . 10
81	80	ralbiia 2894	. . . . . . . . 9
82	55	breq1d 4457	. . . . . . . . . 10
83	82	cbvralv 3088	. . . . . . . . 9
84	81, 83	bitr4i 252	. . . . . . . 8
85	79, 84	sylibr 212	. . . . . . 7 $/\$ $\$
86		breq2 4451	. . . . . . . . 9
87	86	ralbidv 2903	. . . . . . . 8
88	87	rspcev 3214	. . . . . . 7 $/\$
89	27, 85, 88	syl2anc 661	. . . . . 6 $/\$ $\$
90	1, 9, 34, 75, 89	climsup 13448	. . . . 5 $/\$ $\$
91		eqid 2467	. . . . . . . 8
92	17, 91	fmptd 6043	. . . . . . 7 $/\$ $\$
93	38	ralrimiva 2878	. . . . . . . 8 $/\$ $\$
94		fvex 5874	. . . . . . . . . . . . 13
95	94	inex2 4589	. . . . . . . . . . . 12
96	54, 91, 95	fvmpt 5948	. . . . . . . . . . 11
97		fvex 5874	. . . . . . . . . . . . . 14
98	97	inex2 4589	. . . . . . . . . . . . 13
99	60, 91, 98	fvmpt 5948	. . . . . . . . . . . 12
100	58, 99	syl 16	. . . . . . . . . . 11
101	96, 100	sseq12d 3533	. . . . . . . . . 10
102	101	ralbiia 2894	. . . . . . . . 9
103	54, 69	sseq12d 3533	. . . . . . . . . 10
104	103	cbvralv 3088	. . . . . . . . 9
105	102, 104	bitr4i 252	. . . . . . . 8
106	93, 105	sylibr 212	. . . . . . 7 $/\$ $\$
107		volsup 21698	. . . . . . 7 $/\$
108	92, 106, 107	syl2anc 661	. . . . . 6 $/\$ $\$
109	96	iuneq2i 4344	. . . . . . . . . 10
110	54	cbviunv 4364	. . . . . . . . . 10
111		iunin2 4389	. . . . . . . . . 10
112	109, 110, 111	3eqtr2i 2502	. . . . . . . . 9
113		ffn 5729	. . . . . . . . . . . . . 14
114		fniunfv 6145	. . . . . . . . . . . . . 14
115	13, 113, 114	3syl 20	. . . . . . . . . . . . 13
116		itg1climres.3	. . . . . . . . . . . . 13
117	115, 116	eqtrd 2508	. . . . . . . . . . . 12
118	117	adantr 465	. . . . . . . . . . 11 $/\$ $\$
119	118	ineq2d 3700	. . . . . . . . . 10 $/\$ $\$
120	11	adantr 465	. . . . . . . . . . . 12 $/\$ $\$
121	120, 22	syl 16	. . . . . . . . . . 11 $/\$ $\$
122		df-ss 3490	. . . . . . . . . . 11
123	121, 122	sylib 196	. . . . . . . . . 10 $/\$ $\$
124	119, 123	eqtrd 2508	. . . . . . . . 9 $/\$ $\$
125	112, 124	syl5eq 2520	. . . . . . . 8 $/\$ $\$
126		ffn 5729	. . . . . . . . 9
127		fniunfv 6145	. . . . . . . . 9
128	92, 126, 127	3syl 20	. . . . . . . 8 $/\$ $\$
129	125, 128	eqtr3d 2510	. . . . . . 7 $/\$ $\$
130	129	fveq2d 5868	. . . . . 6 $/\$ $\$
131		frn 5735	. . . . . . . . 9
132	34, 131	syl 16	. . . . . . . 8 $/\$ $\$
133		fdm 5733	. . . . . . . . . . 11
134	34, 133	syl 16	. . . . . . . . . 10 $/\$ $\$
135		1nn 10543	. . . . . . . . . . 11
136		ne0i 3791	. . . . . . . . . . 11
137	135, 136	mp1i 12	. . . . . . . . . 10 $/\$ $\$
138	134, 137	eqnetrd 2760	. . . . . . . . 9 $/\$ $\$
139		dm0rn0 5217	. . . . . . . . . 10
140	139	necon3bii 2735	. . . . . . . . 9
141	138, 140	sylib 196	. . . . . . . 8 $/\$ $\$
142		ffn 5729	. . . . . . . . . . 11
143		breq1 4450	. . . . . . . . . . . 12
144	143	ralrn 6022	. . . . . . . . . . 11
145	34, 142, 144	3syl 20	. . . . . . . . . 10 $/\$ $\$
146	145	rexbidv 2973	. . . . . . . . 9 $/\$ $\$
147	89, 146	mpbird 232	. . . . . . . 8 $/\$ $\$
148		supxrre 11515	. . . . . . . 8 $/\$ $/\$
149	132, 141, 147, 148	syl3anc 1228	. . . . . . 7 $/\$ $\$
150		rnco2 5512	. . . . . . . . 9
151		eqidd 2468	. . . . . . . . . . 11 $/\$ $\$
152		volf 21672	. . . . . . . . . . . . 13
153	152	a1i 11	. . . . . . . . . . . 12 $/\$ $\$
154	153	feqmptd 5918	. . . . . . . . . . 11 $/\$ $\$
155		fveq2 5864	. . . . . . . . . . 11
156	17, 151, 154, 155	fmptco 6052	. . . . . . . . . 10 $/\$ $\$
157	156	rneqd 5228	. . . . . . . . 9 $/\$ $\$
158	150, 157	syl5reqr 2523	. . . . . . . 8 $/\$ $\$
159	158	supeq1d 7902	. . . . . . 7 $/\$ $\$
160	149, 159	eqtr3d 2510	. . . . . 6 $/\$ $\$
161	108, 130, 160	3eqtr4d 2518	. . . . 5 $/\$ $\$
162	90, 161	breqtrrd 4473	. . . 4 $/\$ $\$
163		i1ff 21815	. . . . . . . 8
164		frn 5735	. . . . . . . 8
165	3, 163, 164	3syl 20	. . . . . . 7
166	165	ssdifssd 3642	. . . . . 6 $\$
167	166	sselda 3504	. . . . 5 $/\$ $\$
168	167	recnd 9618	. . . 4 $/\$ $\$
169		nnex 10538	. . . . . 6
170	169	mptex 6129	. . . . 5
171	170	a1i 11	. . . 4 $/\$ $\$
172	34	ffvelrnda 6019	. . . . 5 $/\$ $\$ $/\$
173	172	recnd 9618	. . . 4 $/\$ $\$ $/\$
174	55	oveq2d 6298	. . . . . . 7
175		eqid 2467	. . . . . . 7
176		ovex 6307	. . . . . . 7
177	174, 175, 176	fvmpt 5948	. . . . . 6
178	57	oveq2d 6298	. . . . . 6
179	177, 178	eqtr4d 2511	. . . . 5
180	179	adantl 466	. . . 4 $/\$ $\$ $/\$
181	1, 9, 162, 168, 171, 173, 180	climmulc2 13415	. . 3 $/\$ $\$
182	169	mptex 6129	. . . 4
183	182	a1i 11	. . 3
184	167	adantr 465	. . . . . . . 8 $/\$ $\$ $/\$
185	184, 32	remulcld 9620	. . . . . . 7 $/\$ $\$ $/\$
186	185, 175	fmptd 6043	. . . . . 6 $/\$ $\$
187	186	ffvelrnda 6019	. . . . 5 $/\$ $\$ $/\$
188	187	recnd 9618	. . . 4 $/\$ $\$ $/\$
189	188	anasss 647	. . 3 $/\$ $\$ $/\$
190	3	adantr 465	. . . . . . . . 9 $/\$
191		itg1climres.5	. . . . . . . . . 10
192	191	i1fres 21844	. . . . . . . . 9 $/\$
193	190, 14, 192	syl2anc 661	. . . . . . . 8 $/\$
194	8	adantr 465	. . . . . . . 8 $/\$ $\$
195		ffn 5729	. . . . . . . . . . . . . 14
196	3, 163, 195	3syl 20	. . . . . . . . . . . . 13
197	196	adantr 465	. . . . . . . . . . . 12 $/\$
198		fnfvelrn 6016	. . . . . . . . . . . 12 $/\$
199	197, 198	sylan 471	. . . . . . . . . . 11 $/\$ $/\$
200		i1f0rn 21821	. . . . . . . . . . . . 13
201	3, 200	syl 16	. . . . . . . . . . . 12
202	201	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$
203		ifcl 3981	. . . . . . . . . . 11 $/\$
204	199, 202, 203	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$
205	204, 191	fmptd 6043	. . . . . . . . 9 $/\$
206		frn 5735	. . . . . . . . 9
207		ssdif 3639	. . . . . . . . 9 $\$ $\$
208	205, 206, 207	3syl 20	. . . . . . . 8 $/\$ $\$ $\$
209	165	adantr 465	. . . . . . . . 9 $/\$
210	209	ssdifd 3640	. . . . . . . 8 $/\$ $\$ $\$
211		itg1val2 21823	. . . . . . . 8 $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$
212	193, 194, 208, 210, 211	syl13anc 1230	. . . . . . 7 $/\$ $\$
213		fvex 5874	. . . . . . . . . . . . . . . . . . . . 21
214		c0ex 9586	. . . . . . . . . . . . . . . . . . . . 21
215	213, 214	ifex 4008	. . . . . . . . . . . . . . . . . . . 20
216	191	fvmpt2 5955	. . . . . . . . . . . . . . . . . . . 20 $/\$
217	215, 216	mpan2 671	. . . . . . . . . . . . . . . . . . 19
218	217	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $/\$
219	218	eqeq1d 2469	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $/\$
220		eldifsni 4153	. . . . . . . . . . . . . . . . . . . . 21 $\$
221	220	ad2antlr 726	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $/\$
222		neeq1 2748	. . . . . . . . . . . . . . . . . . . 20
223	221, 222	syl5ibrcom 222	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\$ $/\$
224		iffalse 3948	. . . . . . . . . . . . . . . . . . . 20
225	224	necon1ai 2698	. . . . . . . . . . . . . . . . . . 19
226	223, 225	syl6 33	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $/\$
227	226	pm4.71rd 635	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $/\$ $/\$
228	219, 227	bitrd 253	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$ $/\$
229		iftrue 3945	. . . . . . . . . . . . . . . . . . 19
230	229	eqeq1d 2469	. . . . . . . . . . . . . . . . . 18
231	230	pm5.32i 637	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
232		ancom 450	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
233	231, 232	bitri 249	. . . . . . . . . . . . . . . 16 $/\$ $/\$
234	228, 233	syl6bb 261	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $/\$ $/\$
235	234	pm5.32da 641	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $/\$ $/\$ $/\$
236		anass 649	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
237	235, 236	syl6bbr 263	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $/\$ $/\$
238		i1ff 21815	. . . . . . . . . . . . . . . 16
239		ffn 5729	. . . . . . . . . . . . . . . 16
240	193, 238, 239	3syl 20	. . . . . . . . . . . . . . 15 $/\$
241	240	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
242		fniniseg 6000	. . . . . . . . . . . . . 14 $/\$
243	241, 242	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$
244		elin 3687	. . . . . . . . . . . . . 14 $/\$
245	197	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
246		fniniseg 6000	. . . . . . . . . . . . . . . 16 $/\$
247	245, 246	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $/\$
248	247	anbi1d 704	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $/\$ $/\$ $/\$
249	244, 248	syl5bb 257	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $/\$
250	237, 243, 249	3bitr4d 285	. . . . . . . . . . . 12 $/\$ $/\$ $\$
251	250	alrimiv 1695	. . . . . . . . . . 11 $/\$ $/\$ $\$
252		nfmpt1 4536	. . . . . . . . . . . . . . 15
253	191, 252	nfcxfr 2627	. . . . . . . . . . . . . 14
254	253	nfcnv 5179	. . . . . . . . . . . . 13
255		nfcv 2629	. . . . . . . . . . . . 13
256	254, 255	nfima 5343	. . . . . . . . . . . 12
257		nfcv 2629	. . . . . . . . . . . 12
258	256, 257	cleqf 2656	. . . . . . . . . . 11
259	251, 258	sylibr 212	. . . . . . . . . 10 $/\$ $/\$ $\$
260	259	fveq2d 5868	. . . . . . . . 9 $/\$ $/\$ $\$
261	260	oveq2d 6298	. . . . . . . 8 $/\$ $/\$ $\$
262	261	sumeq2dv 13481	. . . . . . 7 $/\$ $\$ $\$
263	212, 262	eqtrd 2508	. . . . . 6 $/\$ $\$
264	263	mpteq2dva 4533	. . . . 5 $\$
265	264	fveq1d 5866	. . . 4 $\$
266	174	sumeq2sdv 13482	. . . . . 6 $\$ $\$
267		eqid 2467	. . . . . 6 $\$ $\$
268		sumex 13466	. . . . . 6 $\$
269	266, 267, 268	fvmpt 5948	. . . . 5 $\$ $\$
270	177	sumeq2sdv 13482	. . . . 5 $\$ $\$
271	269, 270	eqtr4d 2511	. . . 4 $\$ $\$
272	265, 271	sylan9eq 2528	. . 3 $/\$ $\$
273	1, 2, 8, 181, 183, 189, 272	climfsum 13590	. 2 $\$
274		itg1val 21822	. . 3 $\$
275	3, 274	syl 16	. 2 $\$
276	273, 275	breqtrrd 4473	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369

wal 1377

wceq 1379

wcel 1767

wne 2662

wral 2814

wrex 2815

cvv 3113 $\$ cdif 3473

cin 3475

wss 3476

c0 3785

cif 3939

csn 4027

cuni 4245

ciun 4325 class class class wbr 4447

cmpt 4505

ccnv 4998

cdm 4999

crn 5000

cima 5002

ccom 5003

wfn 5581

wf 5582

cfv 5586 (class class class)co 6282

cfn 7513

csup 7896

cc 9486

cr 9487

cc0 9488

c1 9489

caddc 9491

cmul 9493

cpnf 9621

cxr 9623

clt 9624

cle 9625

cn 10532

cicc 11528

cli 13263

csu 13464

covol 21606

cvol 21607

citg1 21756

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-inf2 8054 ax-cc 8811 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565 ax-pre-sup 9566 ax-addf 9567

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-disj 4418 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-isom 5595 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-of 6522 df-om 6679 df-1st 6781 df-2nd 6782 df-recs 7039 df-rdg 7073 df-1o 7127 df-2o 7128 df-oadd 7131 df-er 7308 df-map 7419 df-pm 7420 df-en 7514 df-dom 7515 df-sdom 7516 df-fin 7517 df-fi 7867 df-sup 7897 df-oi 7931 df-card 8316 df-cda 8544 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-div 10203 df-nn 10533 df-2 10590 df-3 10591 df-n0 10792 df-z 10861 df-uz 11079 df-q 11179 df-rp 11217 df-xneg 11314 df-xadd 11315 df-xmul 11316 df-ioo 11529 df-ico 11531 df-icc 11532 df-fz 11669 df-fzo 11789 df-fl 11893 df-seq 12071 df-exp 12130 df-hash 12368 df-cj 12889 df-re 12890 df-im 12891 df-sqrt 13025 df-abs 13026 df-clim 13267 df-rlim 13268 df-sum 13465 df-rest 14671 df-topgen 14692 df-psmet 18179 df-xmet 18180 df-met 18181 df-bl 18182 df-mopn 18183 df-top 19163 df-bases 19165 df-topon 19166 df-cmp 19650 df-ovol 21608 df-vol 21609 df-mbf 21760 df-itg1 21761

This theorem is referenced by: itg2monolem1 21889

W3C validator