voliunnfl - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > voliunnfl		Structured version Unicode version

Theorem voliunnfl 29622

Description: voliun 21692 is incompatible with the Feferman-Levy model; in that model, therefore, the Lebesgue measure as we've defined it isn't actually a measure. (Contributed by Brendan Leahy, 16-Dec-2017.)

**Hypotheses**
Ref	Expression
voliunnfl.1
voliunnfl.2
voliunnfl.3	$/\$ $/\$ Disj

**Assertion**
Ref	Expression
voliunnfl	$/\$

Distinct variable group:

Allowed substitution hints:

(

)

(

)

Proof of Theorem voliunnfl Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		unieq 4246	. . . . . . . . 9
2		uni0 4265	. . . . . . . . 9
3	1, 2	syl6eq 2517	. . . . . . . 8
4	3	fveq2d 5861	. . . . . . 7
5		0mbl 21678	. . . . . . . . 9
6		mblvol 21669	. . . . . . . . 9
7	5, 6	ax-mp 5	. . . . . . . 8
8		ovol0 21632	. . . . . . . 8
9	7, 8	eqtri 2489	. . . . . . 7
10	4, 9	syl6req 2518	. . . . . 6
11	10	a1d 25	. . . . 5 $/\$ $/\$
12		reldom 7512	. . . . . . . . . . 11
13	12	brrelexi 5032	. . . . . . . . . 10
14		0sdomg 7636	. . . . . . . . . 10
15	13, 14	syl 16	. . . . . . . . 9
16	15	biimparc 487	. . . . . . . 8 $/\$
17		fodomr 7658	. . . . . . . 8 $/\$
18	16, 17	sylancom 667	. . . . . . 7 $/\$
19		unissb 4270	. . . . . . . . . . . . 13
20	19	anbi1i 695	. . . . . . . . . . . 12 $/\$ $/\$
21		r19.26 2982	. . . . . . . . . . . 12 $/\$ $/\$
22	20, 21	bitr4i 252	. . . . . . . . . . 11 $/\$ $/\$
23		ovolctb2 21631	. . . . . . . . . . . . . 14 $/\$
24	23	ex 434	. . . . . . . . . . . . 13
25	24	imdistani 690	. . . . . . . . . . . 12 $/\$ $/\$
26	25	ralimi 2850	. . . . . . . . . . 11 $/\$ $/\$
27	22, 26	sylbi 195	. . . . . . . . . 10 $/\$ $/\$
28	27	ancoms 453	. . . . . . . . 9 $/\$ $/\$
29		foima 5791	. . . . . . . . . . . 12
30	29	raleqdv 3057	. . . . . . . . . . 11 $/\$ $/\$
31		fofn 5788	. . . . . . . . . . . 12
32		ssid 3516	. . . . . . . . . . . 12
33		sseq1 3518	. . . . . . . . . . . . . 14
34		fveq2 5857	. . . . . . . . . . . . . . 15
35	34	eqeq1d 2462	. . . . . . . . . . . . . 14
36	33, 35	anbi12d 710	. . . . . . . . . . . . 13 $/\$ $/\$
37	36	ralima 6131	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
38	31, 32, 37	sylancl 662	. . . . . . . . . . 11 $/\$ $/\$
39	30, 38	bitr3d 255	. . . . . . . . . 10 $/\$ $/\$
40		difss 3624	. . . . . . . . . . . . . . . . . 18 $\$ ..^
41		ovolssnul 21626	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $/\$ $/\$ $\$ ..^
42	40, 41	mp3an1 1306	. . . . . . . . . . . . . . . . 17 $/\$ $\$ ..^
43		ssdifss 3628	. . . . . . . . . . . . . . . . . 18 $\$ ..^
44		nulmbl 21674	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
45		mblvol 21669	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ ..^ $\$ ..^ $\$ ..^
46	45	eqeq1d 2462	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ ..^ $\$ ..^ $\$ ..^
47	46	biimpar 485	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
48		0re 9585	. . . . . . . . . . . . . . . . . . . . . . 23
49	47, 48	syl6eqel 2556	. . . . . . . . . . . . . . . . . . . . . 22 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
50	49	expcom 435	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^ $\$ ..^
51	50	ancld 553	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
52	51	adantl 466	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
53	44, 52	mpd 15	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
54	43, 53	sylan 471	. . . . . . . . . . . . . . . . 17 $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
55	42, 54	syldan 470	. . . . . . . . . . . . . . . 16 $/\$ $\$ ..^ $/\$ $\$ ..^
56	55	ralimi 2850	. . . . . . . . . . . . . . 15 $/\$ $\$ ..^ $/\$ $\$ ..^
57		fveq2 5857	. . . . . . . . . . . . . . . . . . . . 21
58		oveq2 6283	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
59	58	iuneq1d 4343	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
60	57, 59	difeq12d 3616	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
61		eqid 2460	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
62		fvex 5867	. . . . . . . . . . . . . . . . . . . . 21
63		difexg 4588	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^
64	62, 63	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^
65	60, 61, 64	fvmpt 5941	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
66	65	eleq1d 2529	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
67	65	fveq2d 5861	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
68	67	eleq1d 2529	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
69	66, 68	anbi12d 710	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
70	69	ralbiia 2887	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
71		fveq2 5857	. . . . . . . . . . . . . . . . . . . 20
72		oveq2 6283	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
73	72	iuneq1d 4343	. . . . . . . . . . . . . . . . . . . 20 ..^ ..^
74	71, 73	difeq12d 3616	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
75	74	eleq1d 2529	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
76	74	fveq2d 5861	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
77	76	eleq1d 2529	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
78	75, 77	anbi12d 710	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
79	78	cbvralv 3081	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
80	70, 79	bitri 249	. . . . . . . . . . . . . . 15 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
81	56, 80	sylibr 212	. . . . . . . . . . . . . 14 $/\$ $\$ ..^ $/\$ $\$ ..^
82		fveq2 5857	. . . . . . . . . . . . . . . 16
83	82	iundisj2 21687	. . . . . . . . . . . . . . 15 Disj $\$ ..^
84		disjeq2 4414	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^ Disj $\$ ..^ Disj $\$ ..^
85	84, 65	mprg 2820	. . . . . . . . . . . . . . 15 Disj $\$ ..^ Disj $\$ ..^
86	83, 85	mpbir 209	. . . . . . . . . . . . . 14 Disj $\$ ..^
87		nnex 10531	. . . . . . . . . . . . . . . . 17
88	87	mptex 6122	. . . . . . . . . . . . . . . 16 $\$ ..^
89		fveq1 5856	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
90	89	eleq1d 2529	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
91	89	fveq2d 5861	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
92	91	eleq1d 2529	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
93	90, 92	anbi12d 710	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^ $/\$ $\$ ..^
94	93	ralbidv 2896	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $/\$ $\$ ..^ $/\$ $\$ ..^
95	89	adantr 465	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^
96	95	disjeq2dv 4415	. . . . . . . . . . . . . . . . . 18 $\$ ..^ Disj Disj $\$ ..^
97	94, 96	anbi12d 710	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $/\$ Disj $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^
98	89	iuneq2d 4345	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
99	98	fveq2d 5861	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
100		voliunnfl.1	. . . . . . . . . . . . . . . . . . . . . 22
101		voliunnfl.2	. . . . . . . . . . . . . . . . . . . . . . 23
102		seqeq3 12068	. . . . . . . . . . . . . . . . . . . . . . 23
103	101, 102	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
104	100, 103	eqtri 2489	. . . . . . . . . . . . . . . . . . . . 21
105	104	rneqi 5220	. . . . . . . . . . . . . . . . . . . 20
106	105	supeq1i 7896	. . . . . . . . . . . . . . . . . . 19
107	91	mpteq2dv 4527	. . . . . . . . . . . . . . . . . . . . . 22 $\$ ..^ $\$ ..^
108	107	seqeq3d 12071	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
109	108	rneqd 5221	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
110	109	supeq1d 7895	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
111	106, 110	syl5eq 2513	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
112	99, 111	eqeq12d 2482	. . . . . . . . . . . . . . . . 17 $\$ ..^ $\$ ..^ $\$ ..^
113	97, 112	imbi12d 320	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $/\$ Disj $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
114		voliunnfl.3	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Disj
115	88, 113, 114	vtocl 3158	. . . . . . . . . . . . . . 15 $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
116	65	iuneq2i 4337	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^
117	116	fveq2i 5860	. . . . . . . . . . . . . . 15 $\$ ..^ $\$ ..^
118	67	mpteq2ia 4522	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
119		seqeq3 12068	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^ $\$ ..^ $\$ ..^
120	118, 119	ax-mp 5	. . . . . . . . . . . . . . . . 17 $\$ ..^ $\$ ..^
121	120	rneqi 5220	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^
122	121	supeq1i 7896	. . . . . . . . . . . . . . 15 $\$ ..^ $\$ ..^
123	115, 117, 122	3eqtr3g 2524	. . . . . . . . . . . . . 14 $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
124	81, 86, 123	sylancl 662	. . . . . . . . . . . . 13 $/\$ $\$ ..^ $\$ ..^
125	124	adantl 466	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^ $\$ ..^
126	82	iundisj 21686	. . . . . . . . . . . . . . . 16 $\$ ..^
127		fofun 5787	. . . . . . . . . . . . . . . . 17
128		funiunfv 6139	. . . . . . . . . . . . . . . . 17
129	127, 128	syl 16	. . . . . . . . . . . . . . . 16
130	126, 129	syl5eqr 2515	. . . . . . . . . . . . . . 15 $\$ ..^
131	29	unieqd 4248	. . . . . . . . . . . . . . 15
132	130, 131	eqtrd 2501	. . . . . . . . . . . . . 14 $\$ ..^
133	132	fveq2d 5861	. . . . . . . . . . . . 13 $\$ ..^
134	133	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^
135	57	sseq1d 3524	. . . . . . . . . . . . . . . . . . . . 21
136	57	fveq2d 5861	. . . . . . . . . . . . . . . . . . . . . 22
137	136	eqeq1d 2462	. . . . . . . . . . . . . . . . . . . . 21
138	135, 137	anbi12d 710	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
139	138	rspccva 3206	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
140		ssdifss 3628	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^
141	140	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ ..^
142		difss 3624	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^
143		ovolssnul 21626	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^ $/\$ $/\$ $\$ ..^
144	142, 143	mp3an1 1306	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ ..^
145	141, 144	jca 532	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ ..^ $/\$ $\$ ..^
146		nulmbl 21674	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
147		mblvol 21669	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^ $\$ ..^
148	145, 146, 147	3syl 20	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ ..^ $\$ ..^
149	148, 144	eqtrd 2501	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ ..^
150	139, 149	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ ..^
151	150	mpteq2dva 4526	. . . . . . . . . . . . . . . . 17 $/\$ $\$ ..^
152	151	seqeq3d 12071	. . . . . . . . . . . . . . . 16 $/\$ $\$ ..^
153	152	rneqd 5221	. . . . . . . . . . . . . . 15 $/\$ $\$ ..^
154	153	supeq1d 7895	. . . . . . . . . . . . . 14 $/\$ $\$ ..^
155		0cn 9577	. . . . . . . . . . . . . . . . . . . . . 22
156		ser1const 12119	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
157	155, 156	mpan 670	. . . . . . . . . . . . . . . . . . . . 21
158		nncn 10533	. . . . . . . . . . . . . . . . . . . . . 22
159	158	mul01d 9767	. . . . . . . . . . . . . . . . . . . . 21
160	157, 159	eqtrd 2501	. . . . . . . . . . . . . . . . . . . 20
161	160	mpteq2ia 4522	. . . . . . . . . . . . . . . . . . 19
162		fconstmpt 5035	. . . . . . . . . . . . . . . . . . . . 21
163		seqeq3 12068	. . . . . . . . . . . . . . . . . . . . 21
164	162, 163	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
165		1z 10883	. . . . . . . . . . . . . . . . . . . . . 22
166		seqfn 12075	. . . . . . . . . . . . . . . . . . . . . 22
167	165, 166	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
168		nnuz 11106	. . . . . . . . . . . . . . . . . . . . . . 23
169	168	fneq2i 5667	. . . . . . . . . . . . . . . . . . . . . 22
170		dffn5 5904	. . . . . . . . . . . . . . . . . . . . . 22
171	169, 170	bitr3i 251	. . . . . . . . . . . . . . . . . . . . 21
172	167, 171	mpbi 208	. . . . . . . . . . . . . . . . . . . 20
173	164, 172	eqtr3i 2491	. . . . . . . . . . . . . . . . . . 19
174		fconstmpt 5035	. . . . . . . . . . . . . . . . . . 19
175	161, 173, 174	3eqtr4i 2499	. . . . . . . . . . . . . . . . . 18
176	175	rneqi 5220	. . . . . . . . . . . . . . . . 17
177		1nn 10536	. . . . . . . . . . . . . . . . . 18
178		ne0i 3784	. . . . . . . . . . . . . . . . . 18
179		rnxp 5428	. . . . . . . . . . . . . . . . . 18
180	177, 178, 179	mp2b 10	. . . . . . . . . . . . . . . . 17
181	176, 180	eqtri 2489	. . . . . . . . . . . . . . . 16
182	181	supeq1i 7896	. . . . . . . . . . . . . . 15
183		xrltso 11336	. . . . . . . . . . . . . . . 16
184		0xr 9629	. . . . . . . . . . . . . . . 16
185		supsn 7919	. . . . . . . . . . . . . . . 16 $/\$
186	183, 184, 185	mp2an 672	. . . . . . . . . . . . . . 15
187	182, 186	eqtri 2489	. . . . . . . . . . . . . 14
188	154, 187	syl6eq 2517	. . . . . . . . . . . . 13 $/\$ $\$ ..^
189	188	adantl 466	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^
190	125, 134, 189	3eqtr3rd 2510	. . . . . . . . . . 11 $/\$ $/\$
191	190	ex 434	. . . . . . . . . 10 $/\$
192	39, 191	sylbid 215	. . . . . . . . 9 $/\$
193	28, 192	syl5 32	. . . . . . . 8 $/\$
194	193	exlimiv 1693	. . . . . . 7 $/\$
195	18, 194	syl 16	. . . . . 6 $/\$ $/\$
196	195	expimpd 603	. . . . 5 $/\$ $/\$
197	11, 196	pm2.61ine 2773	. . . 4 $/\$ $/\$
198		renepnf 9630	. . . . . . 7
199	48, 198	mp1i 12	. . . . . 6
200		fveq2 5857	. . . . . . 7
201		rembl 21679	. . . . . . . . 9
202		mblvol 21669	. . . . . . . . 9
203	201, 202	ax-mp 5	. . . . . . . 8
204		ovolre 21664	. . . . . . . 8
205	203, 204	eqtri 2489	. . . . . . 7
206	200, 205	syl6eq 2517	. . . . . 6
207	199, 206	neeqtrrd 2760	. . . . 5
208	207	necon2i 2703	. . . 4
209	197, 208	syl 16	. . 3 $/\$ $/\$
210	209	expr 615	. 2 $/\$
211		eqimss 3549	. . 3
212	211	necon3bi 2689	. 2
213	210, 212	pm2.61d1 159	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369

wceq 1374

wex 1591

wcel 1762

wne 2655

wral 2807

cvv 3106 $\$ cdif 3466

wss 3469

c0 3778

csn 4020

cuni 4238

ciun 4318 Disj wdisj 4410 class class class wbr 4440

cmpt 4498

wor 4792

cxp 4990

cdm 4992

crn 4993

cima 4995

wfun 5573

wfn 5574

wfo 5577

cfv 5579 (class class class)co 6275

cdom 7504

csdm 7505

csup 7889

cc 9479

cr 9480

cc0 9481

c1 9482

caddc 9484

cmul 9486

cpnf 9614

cxr 9616

clt 9617

cn 10525

cz 10853

cuz 11071 ..^cfzo 11781

cseq 12063

covol 21602

cvol 21603

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-8 1764 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1961 ax-ext 2438 ax-rep 4551 ax-sep 4561 ax-nul 4569 ax-pow 4618 ax-pr 4679 ax-un 6567 ax-inf2 8047 ax-cnex 9537 ax-resscn 9538 ax-1cn 9539 ax-icn 9540 ax-addcl 9541 ax-addrcl 9542 ax-mulcl 9543 ax-mulrcl 9544 ax-mulcom 9545 ax-addass 9546 ax-mulass 9547 ax-distr 9548 ax-i2m1 9549 ax-1ne0 9550 ax-1rid 9551 ax-rnegex 9552 ax-rrecex 9553 ax-cnre 9554 ax-pre-lttri 9555 ax-pre-lttrn 9556 ax-pre-ltadd 9557 ax-pre-mulgt0 9558 ax-pre-sup 9559

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 969 df-3an 970 df-tru 1377 df-fal 1380 df-ex 1592 df-nf 1595 df-sb 1707 df-eu 2272 df-mo 2273 df-clab 2446 df-cleq 2452 df-clel 2455 df-nfc 2610 df-ne 2657 df-nel 2658 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3108 df-sbc 3325 df-csb 3429 df-dif 3472 df-un 3474 df-in 3476 df-ss 3483 df-pss 3485 df-nul 3779 df-if 3933 df-pw 4005 df-sn 4021 df-pr 4023 df-tp 4025 df-op 4027 df-uni 4239 df-int 4276 df-iun 4320 df-disj 4411 df-br 4441 df-opab 4499 df-mpt 4500 df-tr 4534 df-eprel 4784 df-id 4788 df-po 4793 df-so 4794 df-fr 4831 df-se 4832 df-we 4833 df-ord 4874 df-on 4875 df-lim 4876 df-suc 4877 df-xp 4998 df-rel 4999 df-cnv 5000 df-co 5001 df-dm 5002 df-rn 5003 df-res 5004 df-ima 5005 df-iota 5542 df-fun 5581 df-fn 5582 df-f 5583 df-f1 5584 df-fo 5585 df-f1o 5586 df-fv 5587 df-isom 5588 df-riota 6236 df-ov 6278 df-oprab 6279 df-mpt2 6280 df-of 6515 df-om 6672 df-1st 6774 df-2nd 6775 df-recs 7032 df-rdg 7066 df-1o 7120 df-2o 7121 df-oadd 7124 df-er 7301 df-map 7412 df-en 7507 df-dom 7508 df-sdom 7509 df-fin 7510 df-fi 7860 df-sup 7890 df-oi 7924 df-card 8309 df-cda 8537 df-pnf 9619 df-mnf 9620 df-xr 9621 df-ltxr 9622 df-le 9623 df-sub 9796 df-neg 9797 df-div 10196 df-nn 10526 df-2 10583 df-3 10584 df-n0 10785 df-z 10854 df-uz 11072 df-q 11172 df-rp 11210 df-xneg 11307 df-xadd 11308 df-xmul 11309 df-ioo 11522 df-ico 11524 df-icc 11525 df-fz 11662 df-fzo 11782 df-fl 11886 df-seq 12064 df-exp 12123 df-hash 12361 df-cj 12882 df-re 12883 df-im 12884 df-sqr 13018 df-abs 13019 df-clim 13260 df-sum 13458 df-rest 14667 df-topgen 14688 df-psmet 18175 df-xmet 18176 df-met 18177 df-bl 18178 df-mopn 18179 df-top 19159 df-bases 19161 df-topon 19162 df-cmp 19646 df-ovol 21604 df-vol 21605

This theorem is referenced by: (None)

W3C validator