itg1climres - Metamath Proof Explorer

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

Theorem itg1climres 19559

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 10477	. . 3
2		1z 10267	. . . 4
3	2	a1i 11	. . 3
4		itg1climres.4	. . . . 5
5		i1frn 19522	. . . . 5
6	4, 5	syl 16	. . . 4
7		difss 3434	. . . 4 $\$
8		ssfi 7288	. . . 4 $/\$ $\$ $\$
9	6, 7, 8	sylancl 644	. . 3 $\$
10	2	a1i 11	. . . 4 $/\$ $\$
11		i1fima 19523	. . . . . . . . . . . 12
12	4, 11	syl 16	. . . . . . . . . . 11
13	12	ad2antrr 707	. . . . . . . . . 10 $/\$ $\$ $/\$
14		itg1climres.1	. . . . . . . . . . . 12
15	14	ffvelrnda 5829	. . . . . . . . . . 11 $/\$
16	15	adantlr 696	. . . . . . . . . 10 $/\$ $\$ $/\$
17		inmbl 19389	. . . . . . . . . 10 $/\$
18	13, 16, 17	syl2anc 643	. . . . . . . . 9 $/\$ $\$ $/\$
19		mblvol 19379	. . . . . . . . 9
20	18, 19	syl 16	. . . . . . . 8 $/\$ $\$ $/\$
21		inss1 3521	. . . . . . . . . 10
22	21	a1i 11	. . . . . . . . 9 $/\$ $\$ $/\$
23		mblss 19380	. . . . . . . . . 10
24	13, 23	syl 16	. . . . . . . . 9 $/\$ $\$ $/\$
25		mblvol 19379	. . . . . . . . . . 11
26	13, 25	syl 16	. . . . . . . . . 10 $/\$ $\$ $/\$
27		i1fima2sn 19525	. . . . . . . . . . . 12 $/\$ $\$
28	4, 27	sylan 458	. . . . . . . . . . 11 $/\$ $\$
29	28	adantr 452	. . . . . . . . . 10 $/\$ $\$ $/\$
30	26, 29	eqeltrrd 2479	. . . . . . . . 9 $/\$ $\$ $/\$
31		ovolsscl 19335	. . . . . . . . 9 $/\$ $/\$
32	22, 24, 30, 31	syl3anc 1184	. . . . . . . 8 $/\$ $\$ $/\$
33	20, 32	eqeltrd 2478	. . . . . . 7 $/\$ $\$ $/\$
34		eqid 2404	. . . . . . 7
35	33, 34	fmptd 5852	. . . . . 6 $/\$ $\$
36		itg1climres.2	. . . . . . . . . . . . 13 $/\$
37	36	adantlr 696	. . . . . . . . . . . 12 $/\$ $\$ $/\$
38		sslin 3527	. . . . . . . . . . . 12
39	37, 38	syl 16	. . . . . . . . . . 11 $/\$ $\$ $/\$
40	14	adantr 452	. . . . . . . . . . . . . 14 $/\$ $\$
41		peano2nn 9968	. . . . . . . . . . . . . 14
42		ffvelrn 5827	. . . . . . . . . . . . . 14 $/\$
43	40, 41, 42	syl2an 464	. . . . . . . . . . . . 13 $/\$ $\$ $/\$
44		inmbl 19389	. . . . . . . . . . . . 13 $/\$
45	13, 43, 44	syl2anc 643	. . . . . . . . . . . 12 $/\$ $\$ $/\$
46		mblss 19380	. . . . . . . . . . . 12
47	45, 46	syl 16	. . . . . . . . . . 11 $/\$ $\$ $/\$
48		ovolss 19334	. . . . . . . . . . 11 $/\$
49	39, 47, 48	syl2anc 643	. . . . . . . . . 10 $/\$ $\$ $/\$
50		mblvol 19379	. . . . . . . . . . 11
51	45, 50	syl 16	. . . . . . . . . 10 $/\$ $\$ $/\$
52	49, 20, 51	3brtr4d 4202	. . . . . . . . 9 $/\$ $\$ $/\$
53	52	ralrimiva 2749	. . . . . . . 8 $/\$ $\$
54		fveq2 5687	. . . . . . . . . . . . . 14
55	54	ineq2d 3502	. . . . . . . . . . . . 13
56	55	fveq2d 5691	. . . . . . . . . . . 12
57		fvex 5701	. . . . . . . . . . . 12
58	56, 34, 57	fvmpt 5765	. . . . . . . . . . 11
59		peano2nn 9968	. . . . . . . . . . . 12
60		fveq2 5687	. . . . . . . . . . . . . . 15
61	60	ineq2d 3502	. . . . . . . . . . . . . 14
62	61	fveq2d 5691	. . . . . . . . . . . . 13
63		fvex 5701	. . . . . . . . . . . . 13
64	62, 34, 63	fvmpt 5765	. . . . . . . . . . . 12
65	59, 64	syl 16	. . . . . . . . . . 11
66	58, 65	breq12d 4185	. . . . . . . . . 10
67	66	ralbiia 2698	. . . . . . . . 9
68		oveq1 6047	. . . . . . . . . . . . . 14
69	68	fveq2d 5691	. . . . . . . . . . . . 13
70	69	ineq2d 3502	. . . . . . . . . . . 12
71	70	fveq2d 5691	. . . . . . . . . . 11
72	56, 71	breq12d 4185	. . . . . . . . . 10
73	72	cbvralv 2892	. . . . . . . . 9
74	67, 73	bitr4i 244	. . . . . . . 8
75	53, 74	sylibr 204	. . . . . . 7 $/\$ $\$
76	75	r19.21bi 2764	. . . . . 6 $/\$ $\$ $/\$
77		ovolss 19334	. . . . . . . . . . 11 $/\$
78	21, 24, 77	sylancr 645	. . . . . . . . . 10 $/\$ $\$ $/\$
79	78, 20, 26	3brtr4d 4202	. . . . . . . . 9 $/\$ $\$ $/\$
80	79	ralrimiva 2749	. . . . . . . 8 $/\$ $\$
81	58	breq1d 4182	. . . . . . . . . 10
82	81	ralbiia 2698	. . . . . . . . 9
83	56	breq1d 4182	. . . . . . . . . 10
84	83	cbvralv 2892	. . . . . . . . 9
85	82, 84	bitr4i 244	. . . . . . . 8
86	80, 85	sylibr 204	. . . . . . 7 $/\$ $\$
87		breq2 4176	. . . . . . . . 9
88	87	ralbidv 2686	. . . . . . . 8
89	88	rspcev 3012	. . . . . . 7 $/\$
90	28, 86, 89	syl2anc 643	. . . . . 6 $/\$ $\$
91	1, 10, 35, 76, 90	climsup 12418	. . . . 5 $/\$ $\$
92		eqid 2404	. . . . . . . 8
93	18, 92	fmptd 5852	. . . . . . 7 $/\$ $\$
94	39	ralrimiva 2749	. . . . . . . 8 $/\$ $\$
95		fvex 5701	. . . . . . . . . . . . 13
96	95	inex2 4305	. . . . . . . . . . . 12
97	55, 92, 96	fvmpt 5765	. . . . . . . . . . 11
98		fvex 5701	. . . . . . . . . . . . . 14
99	98	inex2 4305	. . . . . . . . . . . . 13
100	61, 92, 99	fvmpt 5765	. . . . . . . . . . . 12
101	59, 100	syl 16	. . . . . . . . . . 11
102	97, 101	sseq12d 3337	. . . . . . . . . 10
103	102	ralbiia 2698	. . . . . . . . 9
104	55, 70	sseq12d 3337	. . . . . . . . . 10
105	104	cbvralv 2892	. . . . . . . . 9
106	103, 105	bitr4i 244	. . . . . . . 8
107	94, 106	sylibr 204	. . . . . . 7 $/\$ $\$
108		volsup 19403	. . . . . . 7 $/\$
109	93, 107, 108	syl2anc 643	. . . . . 6 $/\$ $\$
110	97	iuneq2i 4071	. . . . . . . . . 10
111	55	cbviunv 4090	. . . . . . . . . 10
112		iunin2 4115	. . . . . . . . . 10
113	110, 111, 112	3eqtr2i 2430	. . . . . . . . 9
114		ffn 5550	. . . . . . . . . . . . . 14
115		fniunfv 5953	. . . . . . . . . . . . . 14
116	14, 114, 115	3syl 19	. . . . . . . . . . . . 13
117		itg1climres.3	. . . . . . . . . . . . 13
118	116, 117	eqtrd 2436	. . . . . . . . . . . 12
119	118	adantr 452	. . . . . . . . . . 11 $/\$ $\$
120	119	ineq2d 3502	. . . . . . . . . 10 $/\$ $\$
121	12	adantr 452	. . . . . . . . . . . 12 $/\$ $\$
122	121, 23	syl 16	. . . . . . . . . . 11 $/\$ $\$
123		df-ss 3294	. . . . . . . . . . 11
124	122, 123	sylib 189	. . . . . . . . . 10 $/\$ $\$
125	120, 124	eqtrd 2436	. . . . . . . . 9 $/\$ $\$
126	113, 125	syl5eq 2448	. . . . . . . 8 $/\$ $\$
127		ffn 5550	. . . . . . . . 9
128		fniunfv 5953	. . . . . . . . 9
129	93, 127, 128	3syl 19	. . . . . . . 8 $/\$ $\$
130	126, 129	eqtr3d 2438	. . . . . . 7 $/\$ $\$
131	130	fveq2d 5691	. . . . . 6 $/\$ $\$
132		frn 5556	. . . . . . . . 9
133	35, 132	syl 16	. . . . . . . 8 $/\$ $\$
134		fdm 5554	. . . . . . . . . . 11
135	35, 134	syl 16	. . . . . . . . . 10 $/\$ $\$
136		1nn 9967	. . . . . . . . . . 11
137		ne0i 3594	. . . . . . . . . . 11
138	136, 137	mp1i 12	. . . . . . . . . 10 $/\$ $\$
139	135, 138	eqnetrd 2585	. . . . . . . . 9 $/\$ $\$
140		dm0rn0 5045	. . . . . . . . . 10
141	140	necon3bii 2599	. . . . . . . . 9
142	139, 141	sylib 189	. . . . . . . 8 $/\$ $\$
143		ffn 5550	. . . . . . . . . . 11
144		breq1 4175	. . . . . . . . . . . 12
145	144	ralrn 5832	. . . . . . . . . . 11
146	35, 143, 145	3syl 19	. . . . . . . . . 10 $/\$ $\$
147	146	rexbidv 2687	. . . . . . . . 9 $/\$ $\$
148	90, 147	mpbird 224	. . . . . . . 8 $/\$ $\$
149		supxrre 10862	. . . . . . . 8 $/\$ $/\$
150	133, 142, 148, 149	syl3anc 1184	. . . . . . 7 $/\$ $\$
151		rnco2 5336	. . . . . . . . 9
152		eqidd 2405	. . . . . . . . . . 11 $/\$ $\$
153		volf 19378	. . . . . . . . . . . . 13
154	153	a1i 11	. . . . . . . . . . . 12 $/\$ $\$
155	154	feqmptd 5738	. . . . . . . . . . 11 $/\$ $\$
156		fveq2 5687	. . . . . . . . . . 11
157	18, 152, 155, 156	fmptco 5860	. . . . . . . . . 10 $/\$ $\$
158	157	rneqd 5056	. . . . . . . . 9 $/\$ $\$
159	151, 158	syl5reqr 2451	. . . . . . . 8 $/\$ $\$
160	159	supeq1d 7409	. . . . . . 7 $/\$ $\$
161	150, 160	eqtr3d 2438	. . . . . 6 $/\$ $\$
162	109, 131, 161	3eqtr4d 2446	. . . . 5 $/\$ $\$
163	91, 162	breqtrrd 4198	. . . 4 $/\$ $\$
164		i1ff 19521	. . . . . . . 8
165		frn 5556	. . . . . . . 8
166	4, 164, 165	3syl 19	. . . . . . 7
167	166	ssdifssd 3445	. . . . . 6 $\$
168	167	sselda 3308	. . . . 5 $/\$ $\$
169	168	recnd 9070	. . . 4 $/\$ $\$
170		nnex 9962	. . . . . 6
171	170	mptex 5925	. . . . 5
172	171	a1i 11	. . . 4 $/\$ $\$
173	35	ffvelrnda 5829	. . . . 5 $/\$ $\$ $/\$
174	173	recnd 9070	. . . 4 $/\$ $\$ $/\$
175	56	oveq2d 6056	. . . . . . 7
176		eqid 2404	. . . . . . 7
177		ovex 6065	. . . . . . 7
178	175, 176, 177	fvmpt 5765	. . . . . 6
179	58	oveq2d 6056	. . . . . 6
180	178, 179	eqtr4d 2439	. . . . 5
181	180	adantl 453	. . . 4 $/\$ $\$ $/\$
182	1, 10, 163, 169, 172, 174, 181	climmulc2 12385	. . 3 $/\$ $\$
183	170	mptex 5925	. . . 4
184	183	a1i 11	. . 3
185	168	adantr 452	. . . . . . . 8 $/\$ $\$ $/\$
186	185, 33	remulcld 9072	. . . . . . 7 $/\$ $\$ $/\$
187	186, 176	fmptd 5852	. . . . . 6 $/\$ $\$
188	187	ffvelrnda 5829	. . . . 5 $/\$ $\$ $/\$
189	188	recnd 9070	. . . 4 $/\$ $\$ $/\$
190	189	anasss 629	. . 3 $/\$ $\$ $/\$
191	4	adantr 452	. . . . . . . . 9 $/\$
192		itg1climres.5	. . . . . . . . . 10
193	192	i1fres 19550	. . . . . . . . 9 $/\$
194	191, 15, 193	syl2anc 643	. . . . . . . 8 $/\$
195	9	adantr 452	. . . . . . . 8 $/\$ $\$
196		ffn 5550	. . . . . . . . . . . . . 14
197	4, 164, 196	3syl 19	. . . . . . . . . . . . 13
198	197	adantr 452	. . . . . . . . . . . 12 $/\$
199		fnfvelrn 5826	. . . . . . . . . . . 12 $/\$
200	198, 199	sylan 458	. . . . . . . . . . 11 $/\$ $/\$
201		i1f0rn 19527	. . . . . . . . . . . . 13
202	4, 201	syl 16	. . . . . . . . . . . 12
203	202	ad2antrr 707	. . . . . . . . . . 11 $/\$ $/\$
204		ifcl 3735	. . . . . . . . . . 11 $/\$
205	200, 203, 204	syl2anc 643	. . . . . . . . . 10 $/\$ $/\$
206	205, 192	fmptd 5852	. . . . . . . . 9 $/\$
207		frn 5556	. . . . . . . . 9
208		ssdif 3442	. . . . . . . . 9 $\$ $\$
209	206, 207, 208	3syl 19	. . . . . . . 8 $/\$ $\$ $\$
210	166	adantr 452	. . . . . . . . 9 $/\$
211	210	ssdifd 3443	. . . . . . . 8 $/\$ $\$ $\$
212		itg1val2 19529	. . . . . . . 8 $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$
213	194, 195, 209, 211, 212	syl13anc 1186	. . . . . . 7 $/\$ $\$
214		fvex 5701	. . . . . . . . . . . . . . . . . . . . 21
215		c0ex 9041	. . . . . . . . . . . . . . . . . . . . 21
216	214, 215	ifex 3757	. . . . . . . . . . . . . . . . . . . 20
217	192	fvmpt2 5771	. . . . . . . . . . . . . . . . . . . 20 $/\$
218	216, 217	mpan2 653	. . . . . . . . . . . . . . . . . . 19
219	218	adantl 453	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $/\$
220	219	eqeq1d 2412	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $/\$
221		eldifsni 3888	. . . . . . . . . . . . . . . . . . . . 21 $\$
222	221	ad2antlr 708	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $/\$
223		neeq1 2575	. . . . . . . . . . . . . . . . . . . 20
224	222, 223	syl5ibrcom 214	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\$ $/\$
225		iffalse 3706	. . . . . . . . . . . . . . . . . . . 20
226	225	necon1ai 2609	. . . . . . . . . . . . . . . . . . 19
227	224, 226	syl6 31	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $/\$
228	227	pm4.71rd 617	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $/\$ $/\$
229	220, 228	bitrd 245	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$ $/\$
230		iftrue 3705	. . . . . . . . . . . . . . . . . . 19
231	230	eqeq1d 2412	. . . . . . . . . . . . . . . . . 18
232	231	pm5.32i 619	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
233		ancom 438	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
234	232, 233	bitri 241	. . . . . . . . . . . . . . . 16 $/\$ $/\$
235	229, 234	syl6bb 253	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $/\$ $/\$
236	235	pm5.32da 623	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $/\$ $/\$ $/\$
237		anass 631	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
238	236, 237	syl6bbr 255	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $/\$ $/\$
239		i1ff 19521	. . . . . . . . . . . . . . . 16
240		ffn 5550	. . . . . . . . . . . . . . . 16
241	194, 239, 240	3syl 19	. . . . . . . . . . . . . . 15 $/\$
242	241	adantr 452	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
243		fniniseg 5810	. . . . . . . . . . . . . 14 $/\$
244	242, 243	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$
245		elin 3490	. . . . . . . . . . . . . 14 $/\$
246	198	adantr 452	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
247		fniniseg 5810	. . . . . . . . . . . . . . . 16 $/\$
248	246, 247	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $/\$
249	248	anbi1d 686	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $/\$ $/\$ $/\$
250	245, 249	syl5bb 249	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $/\$
251	238, 244, 250	3bitr4d 277	. . . . . . . . . . . 12 $/\$ $/\$ $\$
252	251	alrimiv 1638	. . . . . . . . . . 11 $/\$ $/\$ $\$
253		nfmpt1 4258	. . . . . . . . . . . . . . 15
254	192, 253	nfcxfr 2537	. . . . . . . . . . . . . 14
255	254	nfcnv 5010	. . . . . . . . . . . . 13
256		nfcv 2540	. . . . . . . . . . . . 13
257	255, 256	nfima 5170	. . . . . . . . . . . 12
258		nfcv 2540	. . . . . . . . . . . 12
259	257, 258	cleqf 2564	. . . . . . . . . . 11
260	252, 259	sylibr 204	. . . . . . . . . 10 $/\$ $/\$ $\$
261	260	fveq2d 5691	. . . . . . . . 9 $/\$ $/\$ $\$
262	261	oveq2d 6056	. . . . . . . 8 $/\$ $/\$ $\$
263	262	sumeq2dv 12452	. . . . . . 7 $/\$ $\$ $\$
264	213, 263	eqtrd 2436	. . . . . 6 $/\$ $\$
265	264	mpteq2dva 4255	. . . . 5 $\$
266	265	fveq1d 5689	. . . 4 $\$
267	175	sumeq2sdv 12453	. . . . . 6 $\$ $\$
268		eqid 2404	. . . . . 6 $\$ $\$
269		sumex 12436	. . . . . 6 $\$
270	267, 268, 269	fvmpt 5765	. . . . 5 $\$ $\$
271	178	sumeq2sdv 12453	. . . . 5 $\$ $\$
272	270, 271	eqtr4d 2439	. . . 4 $\$ $\$
273	266, 272	sylan9eq 2456	. . 3 $/\$ $\$
274	1, 3, 9, 182, 184, 190, 273	climfsum 12554	. 2 $\$
275		itg1val 19528	. . 3 $\$
276	4, 275	syl 16	. 2 $\$
277	274, 276	breqtrrd 4198	1

Colors of variables: wff set class

Syntax hints:

wi 4

wb 177 $/\$ wa 359

wal 1546

wceq 1649

wcel 1721

wne 2567

wral 2666

wrex 2667

cvv 2916 $\$ cdif 3277

cin 3279

wss 3280

c0 3588

cif 3699

csn 3774

cuni 3975

ciun 4053 class class class wbr 4172

cmpt 4226

ccnv 4836

cdm 4837

crn 4838

cima 4840

ccom 4841

wfn 5408

wf 5409

cfv 5413 (class class class)co 6040

cfn 7068

csup 7403

cc 8944

cr 8945

cc0 8946

c1 8947

caddc 8949

cmul 8951

cpnf 9073

cxr 9075

clt 9076

cle 9077

cn 9956

cz 10238

cicc 10875

cli 12233

csu 12434

covol 19312

cvol 19313

citg1 19460

This theorem is referenced by: itg2monolem1 19595

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-cc 8271 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024 ax-addf 9025

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-disj 4143 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-of 6264 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-2o 6684 df-oadd 6687 df-er 6864 df-map 6979 df-pm 6980 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-fi 7374 df-sup 7404 df-oi 7435 df-card 7782 df-cda 8004 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-n0 10178 df-z 10239 df-uz 10445 df-q 10531 df-rp 10569 df-xneg 10666 df-xadd 10667 df-xmul 10668 df-ioo 10876 df-ico 10878 df-icc 10879 df-fz 11000 df-fzo 11091 df-fl 11157 df-seq 11279 df-exp 11338 df-hash 11574 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-clim 12237 df-rlim 12238 df-sum 12435 df-rest 13605 df-topgen 13622 df-psmet 16649 df-xmet 16650 df-met 16651 df-bl 16652 df-mopn 16653 df-top 16918 df-bases 16920 df-topon 16921 df-cmp 17404 df-ovol 19314 df-vol 19315 df-mbf 19465 df-itg1 19466

W3C validator