voliunnfl - Mathbox for Brendan Leahy

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

Theorem voliunnfl 31996

Description: voliun 22519 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 4209	. . . . . . . . 9
2		uni0 4228	. . . . . . . . 9
3	1, 2	syl6eq 2503	. . . . . . . 8
4	3	fveq2d 5874	. . . . . . 7
5		0mbl 22505	. . . . . . . . 9
6		mblvol 22496	. . . . . . . . 9
7	5, 6	ax-mp 5	. . . . . . . 8
8		ovol0 22458	. . . . . . . 8
9	7, 8	eqtri 2475	. . . . . . 7
10	4, 9	syl6req 2504	. . . . . 6
11	10	a1d 26	. . . . 5 $/\$ $/\$
12		reldom 7580	. . . . . . . . . . 11
13	12	brrelexi 4878	. . . . . . . . . 10
14		0sdomg 7706	. . . . . . . . . 10
15	13, 14	syl 17	. . . . . . . . 9
16	15	biimparc 490	. . . . . . . 8 $/\$
17		fodomr 7728	. . . . . . . 8 $/\$
18	16, 17	sylancom 674	. . . . . . 7 $/\$
19		unissb 4232	. . . . . . . . . . . . 13
20	19	anbi1i 702	. . . . . . . . . . . 12 $/\$ $/\$
21		r19.26 2919	. . . . . . . . . . . 12 $/\$ $/\$
22	20, 21	bitr4i 256	. . . . . . . . . . 11 $/\$ $/\$
23		ovolctb2 22457	. . . . . . . . . . . . . 14 $/\$
24	23	ex 436	. . . . . . . . . . . . 13
25	24	imdistani 697	. . . . . . . . . . . 12 $/\$ $/\$
26	25	ralimi 2783	. . . . . . . . . . 11 $/\$ $/\$
27	22, 26	sylbi 199	. . . . . . . . . 10 $/\$ $/\$
28	27	ancoms 455	. . . . . . . . 9 $/\$ $/\$
29		foima 5803	. . . . . . . . . . . 12
30	29	raleqdv 2995	. . . . . . . . . . 11 $/\$ $/\$
31		fofn 5800	. . . . . . . . . . . 12
32		ssid 3453	. . . . . . . . . . . 12
33		sseq1 3455	. . . . . . . . . . . . . 14
34		fveq2 5870	. . . . . . . . . . . . . . 15
35	34	eqeq1d 2455	. . . . . . . . . . . . . 14
36	33, 35	anbi12d 718	. . . . . . . . . . . . 13 $/\$ $/\$
37	36	ralima 6150	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
38	31, 32, 37	sylancl 669	. . . . . . . . . . 11 $/\$ $/\$
39	30, 38	bitr3d 259	. . . . . . . . . 10 $/\$ $/\$
40		difss 3562	. . . . . . . . . . . . . . . . . 18 $\$ ..^
41		ovolssnul 22452	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $/\$ $/\$ $\$ ..^
42	40, 41	mp3an1 1353	. . . . . . . . . . . . . . . . 17 $/\$ $\$ ..^
43		ssdifss 3566	. . . . . . . . . . . . . . . . . 18 $\$ ..^
44		nulmbl 22501	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
45		mblvol 22496	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ ..^ $\$ ..^ $\$ ..^
46	45	eqeq1d 2455	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ ..^ $\$ ..^ $\$ ..^
47	46	biimpar 488	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
48		0re 9648	. . . . . . . . . . . . . . . . . . . . . . 23
49	47, 48	syl6eqel 2539	. . . . . . . . . . . . . . . . . . . . . 22 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
50	49	expcom 437	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^ $\$ ..^
51	50	ancld 556	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
52	51	adantl 468	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
53	44, 52	mpd 15	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
54	43, 53	sylan 474	. . . . . . . . . . . . . . . . 17 $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
55	42, 54	syldan 473	. . . . . . . . . . . . . . . 16 $/\$ $\$ ..^ $/\$ $\$ ..^
56	55	ralimi 2783	. . . . . . . . . . . . . . 15 $/\$ $\$ ..^ $/\$ $\$ ..^
57		fveq2 5870	. . . . . . . . . . . . . . . . . . . . 21
58		oveq2 6303	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
59	58	iuneq1d 4306	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
60	57, 59	difeq12d 3554	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
61		eqid 2453	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
62		fvex 5880	. . . . . . . . . . . . . . . . . . . . 21
63		difexg 4554	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^
64	62, 63	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^
65	60, 61, 64	fvmpt 5953	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
66	65	eleq1d 2515	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
67	65	fveq2d 5874	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
68	67	eleq1d 2515	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
69	66, 68	anbi12d 718	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
70	69	ralbiia 2820	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
71		fveq2 5870	. . . . . . . . . . . . . . . . . . . 20
72		oveq2 6303	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
73	72	iuneq1d 4306	. . . . . . . . . . . . . . . . . . . 20 ..^ ..^
74	71, 73	difeq12d 3554	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
75	74	eleq1d 2515	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
76	74	fveq2d 5874	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
77	76	eleq1d 2515	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
78	75, 77	anbi12d 718	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
79	78	cbvralv 3021	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
80	70, 79	bitri 253	. . . . . . . . . . . . . . 15 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
81	56, 80	sylibr 216	. . . . . . . . . . . . . 14 $/\$ $\$ ..^ $/\$ $\$ ..^
82		fveq2 5870	. . . . . . . . . . . . . . . 16
83	82	iundisj2 22514	. . . . . . . . . . . . . . 15 Disj $\$ ..^
84		disjeq2 4380	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^ Disj $\$ ..^ Disj $\$ ..^
85	84, 65	mprg 2753	. . . . . . . . . . . . . . 15 Disj $\$ ..^ Disj $\$ ..^
86	83, 85	mpbir 213	. . . . . . . . . . . . . 14 Disj $\$ ..^
87		nnex 10622	. . . . . . . . . . . . . . . . 17
88	87	mptex 6141	. . . . . . . . . . . . . . . 16 $\$ ..^
89		fveq1 5869	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
90	89	eleq1d 2515	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
91	89	fveq2d 5874	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
92	91	eleq1d 2515	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
93	90, 92	anbi12d 718	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^ $/\$ $\$ ..^
94	93	ralbidv 2829	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $/\$ $\$ ..^ $/\$ $\$ ..^
95	89	adantr 467	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^
96	95	disjeq2dv 4381	. . . . . . . . . . . . . . . . . 18 $\$ ..^ Disj Disj $\$ ..^
97	94, 96	anbi12d 718	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $/\$ Disj $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^
98	89	iuneq2d 4308	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
99	98	fveq2d 5874	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
100		voliunnfl.1	. . . . . . . . . . . . . . . . . . . . . 22
101		voliunnfl.2	. . . . . . . . . . . . . . . . . . . . . . 23
102		seqeq3 12225	. . . . . . . . . . . . . . . . . . . . . . 23
103	101, 102	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
104	100, 103	eqtri 2475	. . . . . . . . . . . . . . . . . . . . 21
105	104	rneqi 5064	. . . . . . . . . . . . . . . . . . . 20
106	105	supeq1i 7966	. . . . . . . . . . . . . . . . . . 19
107	91	mpteq2dv 4493	. . . . . . . . . . . . . . . . . . . . . 22 $\$ ..^ $\$ ..^
108	107	seqeq3d 12228	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
109	108	rneqd 5065	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
110	109	supeq1d 7965	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
111	106, 110	syl5eq 2499	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
112	99, 111	eqeq12d 2468	. . . . . . . . . . . . . . . . 17 $\$ ..^ $\$ ..^ $\$ ..^
113	97, 112	imbi12d 322	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $/\$ Disj $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
114		voliunnfl.3	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Disj
115	88, 113, 114	vtocl 3102	. . . . . . . . . . . . . . 15 $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
116	65	iuneq2i 4300	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^
117	116	fveq2i 5873	. . . . . . . . . . . . . . 15 $\$ ..^ $\$ ..^
118	67	mpteq2ia 4488	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
119		seqeq3 12225	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^ $\$ ..^ $\$ ..^
120	118, 119	ax-mp 5	. . . . . . . . . . . . . . . . 17 $\$ ..^ $\$ ..^
121	120	rneqi 5064	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^
122	121	supeq1i 7966	. . . . . . . . . . . . . . 15 $\$ ..^ $\$ ..^
123	115, 117, 122	3eqtr3g 2510	. . . . . . . . . . . . . 14 $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
124	81, 86, 123	sylancl 669	. . . . . . . . . . . . 13 $/\$ $\$ ..^ $\$ ..^
125	124	adantl 468	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^ $\$ ..^
126	82	iundisj 22513	. . . . . . . . . . . . . . . 16 $\$ ..^
127		fofun 5799	. . . . . . . . . . . . . . . . 17
128		funiunfv 6158	. . . . . . . . . . . . . . . . 17
129	127, 128	syl 17	. . . . . . . . . . . . . . . 16
130	126, 129	syl5eqr 2501	. . . . . . . . . . . . . . 15 $\$ ..^
131	29	unieqd 4211	. . . . . . . . . . . . . . 15
132	130, 131	eqtrd 2487	. . . . . . . . . . . . . 14 $\$ ..^
133	132	fveq2d 5874	. . . . . . . . . . . . 13 $\$ ..^
134	133	adantr 467	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^
135	57	sseq1d 3461	. . . . . . . . . . . . . . . . . . . . 21
136	57	fveq2d 5874	. . . . . . . . . . . . . . . . . . . . . 22
137	136	eqeq1d 2455	. . . . . . . . . . . . . . . . . . . . 21
138	135, 137	anbi12d 718	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
139	138	rspccva 3151	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
140		ssdifss 3566	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^
141	140	adantr 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ ..^
142		difss 3562	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^
143		ovolssnul 22452	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^ $/\$ $/\$ $\$ ..^
144	142, 143	mp3an1 1353	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ ..^
145	141, 144	jca 535	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ ..^ $/\$ $\$ ..^
146		nulmbl 22501	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
147		mblvol 22496	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^ $\$ ..^
148	145, 146, 147	3syl 18	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ ..^ $\$ ..^
149	148, 144	eqtrd 2487	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ ..^
150	139, 149	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ ..^
151	150	mpteq2dva 4492	. . . . . . . . . . . . . . . . 17 $/\$ $\$ ..^
152	151	seqeq3d 12228	. . . . . . . . . . . . . . . 16 $/\$ $\$ ..^
153	152	rneqd 5065	. . . . . . . . . . . . . . 15 $/\$ $\$ ..^
154	153	supeq1d 7965	. . . . . . . . . . . . . 14 $/\$ $\$ ..^
155		0cn 9640	. . . . . . . . . . . . . . . . . . . . . 22
156		ser1const 12276	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
157	155, 156	mpan 677	. . . . . . . . . . . . . . . . . . . . 21
158		nncn 10624	. . . . . . . . . . . . . . . . . . . . . 22
159	158	mul01d 9837	. . . . . . . . . . . . . . . . . . . . 21
160	157, 159	eqtrd 2487	. . . . . . . . . . . . . . . . . . . 20
161	160	mpteq2ia 4488	. . . . . . . . . . . . . . . . . . 19
162		fconstmpt 4881	. . . . . . . . . . . . . . . . . . . . 21
163		seqeq3 12225	. . . . . . . . . . . . . . . . . . . . 21
164	162, 163	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
165		1z 10974	. . . . . . . . . . . . . . . . . . . . . 22
166		seqfn 12232	. . . . . . . . . . . . . . . . . . . . . 22
167	165, 166	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
168		nnuz 11201	. . . . . . . . . . . . . . . . . . . . . . 23
169	168	fneq2i 5676	. . . . . . . . . . . . . . . . . . . . . 22
170		dffn5 5915	. . . . . . . . . . . . . . . . . . . . . 22
171	169, 170	bitr3i 255	. . . . . . . . . . . . . . . . . . . . 21
172	167, 171	mpbi 212	. . . . . . . . . . . . . . . . . . . 20
173	164, 172	eqtr3i 2477	. . . . . . . . . . . . . . . . . . 19
174		fconstmpt 4881	. . . . . . . . . . . . . . . . . . 19
175	161, 173, 174	3eqtr4i 2485	. . . . . . . . . . . . . . . . . 18
176	175	rneqi 5064	. . . . . . . . . . . . . . . . 17
177		1nn 10627	. . . . . . . . . . . . . . . . . 18
178		ne0i 3739	. . . . . . . . . . . . . . . . . 18
179		rnxp 5270	. . . . . . . . . . . . . . . . . 18
180	177, 178, 179	mp2b 10	. . . . . . . . . . . . . . . . 17
181	176, 180	eqtri 2475	. . . . . . . . . . . . . . . 16
182	181	supeq1i 7966	. . . . . . . . . . . . . . 15
183		xrltso 11447	. . . . . . . . . . . . . . . 16
184		0xr 9692	. . . . . . . . . . . . . . . 16
185		supsn 7993	. . . . . . . . . . . . . . . 16 $/\$
186	183, 184, 185	mp2an 679	. . . . . . . . . . . . . . 15
187	182, 186	eqtri 2475	. . . . . . . . . . . . . 14
188	154, 187	syl6eq 2503	. . . . . . . . . . . . 13 $/\$ $\$ ..^
189	188	adantl 468	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^
190	125, 134, 189	3eqtr3rd 2496	. . . . . . . . . . 11 $/\$ $/\$
191	190	ex 436	. . . . . . . . . 10 $/\$
192	39, 191	sylbid 219	. . . . . . . . 9 $/\$
193	28, 192	syl5 33	. . . . . . . 8 $/\$
194	193	exlimiv 1778	. . . . . . 7 $/\$
195	18, 194	syl 17	. . . . . 6 $/\$ $/\$
196	195	expimpd 608	. . . . 5 $/\$ $/\$
197	11, 196	pm2.61ine 2709	. . . 4 $/\$ $/\$
198		renepnf 9693	. . . . . . 7
199	48, 198	mp1i 13	. . . . . 6
200		fveq2 5870	. . . . . . 7
201		rembl 22506	. . . . . . . . 9
202		mblvol 22496	. . . . . . . . 9
203	201, 202	ax-mp 5	. . . . . . . 8
204		ovolre 22491	. . . . . . . 8
205	203, 204	eqtri 2475	. . . . . . 7
206	200, 205	syl6eq 2503	. . . . . 6
207	199, 206	neeqtrrd 2700	. . . . 5
208	207	necon2i 2660	. . . 4
209	197, 208	syl 17	. . 3 $/\$ $/\$
210	209	expr 620	. 2 $/\$
211		eqimss 3486	. . 3
212	211	necon3bi 2652	. 2
213	210, 212	pm2.61d1 163	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $/\$ wa 371

wceq 1446

wex 1665

wcel 1889

wne 2624

wral 2739

cvv 3047 $\$ cdif 3403

wss 3406

c0 3733

csn 3970

cuni 4201

ciun 4281 Disj wdisj 4376 class class class wbr 4405

cmpt 4464

wor 4757

cxp 4835

cdm 4837

crn 4838

cima 4840

wfun 5579

wfn 5580

wfo 5583

cfv 5585 (class class class)co 6295

cdom 7572

csdm 7573

csup 7959

cc 9542

cr 9543

cc0 9544

c1 9545

caddc 9547

cmul 9549

cpnf 9677

cxr 9679

clt 9680

cn 10616

cz 10944

cuz 11166 ..^cfzo 11922

cseq 12220

covol 22425

cvol 22427

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-rep 4518 ax-sep 4528 ax-nul 4537 ax-pow 4584 ax-pr 4642 ax-un 6588 ax-inf2 8151 ax-cnex 9600 ax-resscn 9601 ax-1cn 9602 ax-icn 9603 ax-addcl 9604 ax-addrcl 9605 ax-mulcl 9606 ax-mulrcl 9607 ax-mulcom 9608 ax-addass 9609 ax-mulass 9610 ax-distr 9611 ax-i2m1 9612 ax-1ne0 9613 ax-1rid 9614 ax-rnegex 9615 ax-rrecex 9616 ax-cnre 9617 ax-pre-lttri 9618 ax-pre-lttrn 9619 ax-pre-ltadd 9620 ax-pre-mulgt0 9621 ax-pre-sup 9622

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 987 df-3an 988 df-tru 1449 df-fal 1452 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-nel 2627 df-ral 2744 df-rex 2745 df-reu 2746 df-rmo 2747 df-rab 2748 df-v 3049 df-sbc 3270 df-csb 3366 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-pss 3422 df-nul 3734 df-if 3884 df-pw 3955 df-sn 3971 df-pr 3973 df-tp 3975 df-op 3977 df-uni 4202 df-int 4238 df-iun 4283 df-disj 4377 df-br 4406 df-opab 4465 df-mpt 4466 df-tr 4501 df-eprel 4748 df-id 4752 df-po 4758 df-so 4759 df-fr 4796 df-se 4797 df-we 4798 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-pred 5383 df-ord 5429 df-on 5430 df-lim 5431 df-suc 5432 df-iota 5549 df-fun 5587 df-fn 5588 df-f 5589 df-f1 5590 df-fo 5591 df-f1o 5592 df-fv 5593 df-isom 5594 df-riota 6257 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-of 6536 df-om 6698 df-1st 6798 df-2nd 6799 df-wrecs 7033 df-recs 7095 df-rdg 7133 df-1o 7187 df-2o 7188 df-oadd 7191 df-er 7368 df-map 7479 df-en 7575 df-dom 7576 df-sdom 7577 df-fin 7578 df-fi 7930 df-sup 7961 df-inf 7962 df-oi 8030 df-card 8378 df-cda 8603 df-pnf 9682 df-mnf 9683 df-xr 9684 df-ltxr 9685 df-le 9686 df-sub 9867 df-neg 9868 df-div 10277 df-nn 10617 df-2 10675 df-3 10676 df-n0 10877 df-z 10945 df-uz 11167 df-q 11272 df-rp 11310 df-xneg 11416 df-xadd 11417 df-xmul 11418 df-ioo 11646 df-ico 11648 df-icc 11649 df-fz 11792 df-fzo 11923 df-fl 12035 df-seq 12221 df-exp 12280 df-hash 12523 df-cj 13174 df-re 13175 df-im 13176 df-sqrt 13310 df-abs 13311 df-clim 13564 df-sum 13765 df-rest 15333 df-topgen 15354 df-psmet 18974 df-xmet 18975 df-met 18976 df-bl 18977 df-mopn 18978 df-top 19933 df-bases 19934 df-topon 19935 df-cmp 20414 df-ovol 22428 df-vol 22430

This theorem is referenced by: (None)

W3C validator