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 31942

Description: voliun 22499 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 4225	. . . . . . . . 9
2		uni0 4244	. . . . . . . . 9
3	1, 2	syl6eq 2480	. . . . . . . 8
4	3	fveq2d 5883	. . . . . . 7
5		0mbl 22485	. . . . . . . . 9
6		mblvol 22476	. . . . . . . . 9
7	5, 6	ax-mp 5	. . . . . . . 8
8		ovol0 22438	. . . . . . . 8
9	7, 8	eqtri 2452	. . . . . . 7
10	4, 9	syl6req 2481	. . . . . 6
11	10	a1d 27	. . . . 5 $/\$ $/\$
12		reldom 7581	. . . . . . . . . . 11
13	12	brrelexi 4892	. . . . . . . . . 10
14		0sdomg 7705	. . . . . . . . . 10
15	13, 14	syl 17	. . . . . . . . 9
16	15	biimparc 490	. . . . . . . 8 $/\$
17		fodomr 7727	. . . . . . . 8 $/\$
18	16, 17	sylancom 672	. . . . . . 7 $/\$
19		unissb 4248	. . . . . . . . . . . . 13
20	19	anbi1i 700	. . . . . . . . . . . 12 $/\$ $/\$
21		r19.26 2956	. . . . . . . . . . . 12 $/\$ $/\$
22	20, 21	bitr4i 256	. . . . . . . . . . 11 $/\$ $/\$
23		ovolctb2 22437	. . . . . . . . . . . . . 14 $/\$
24	23	ex 436	. . . . . . . . . . . . 13
25	24	imdistani 695	. . . . . . . . . . . 12 $/\$ $/\$
26	25	ralimi 2819	. . . . . . . . . . 11 $/\$ $/\$
27	22, 26	sylbi 199	. . . . . . . . . 10 $/\$ $/\$
28	27	ancoms 455	. . . . . . . . 9 $/\$ $/\$
29		foima 5813	. . . . . . . . . . . 12
30	29	raleqdv 3032	. . . . . . . . . . 11 $/\$ $/\$
31		fofn 5810	. . . . . . . . . . . 12
32		ssid 3484	. . . . . . . . . . . 12
33		sseq1 3486	. . . . . . . . . . . . . 14
34		fveq2 5879	. . . . . . . . . . . . . . 15
35	34	eqeq1d 2425	. . . . . . . . . . . . . 14
36	33, 35	anbi12d 716	. . . . . . . . . . . . 13 $/\$ $/\$
37	36	ralima 6158	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
38	31, 32, 37	sylancl 667	. . . . . . . . . . 11 $/\$ $/\$
39	30, 38	bitr3d 259	. . . . . . . . . 10 $/\$ $/\$
40		difss 3593	. . . . . . . . . . . . . . . . . 18 $\$ ..^
41		ovolssnul 22432	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $/\$ $/\$ $\$ ..^
42	40, 41	mp3an1 1348	. . . . . . . . . . . . . . . . 17 $/\$ $\$ ..^
43		ssdifss 3597	. . . . . . . . . . . . . . . . . 18 $\$ ..^
44		nulmbl 22481	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
45		mblvol 22476	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ ..^ $\$ ..^ $\$ ..^
46	45	eqeq1d 2425	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ ..^ $\$ ..^ $\$ ..^
47	46	biimpar 488	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
48		0re 9645	. . . . . . . . . . . . . . . . . . . . . . 23
49	47, 48	syl6eqel 2519	. . . . . . . . . . . . . . . . . . . . . 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 2819	. . . . . . . . . . . . . . 15 $/\$ $\$ ..^ $/\$ $\$ ..^
57		fveq2 5879	. . . . . . . . . . . . . . . . . . . . 21
58		oveq2 6311	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
59	58	iuneq1d 4322	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
60	57, 59	difeq12d 3585	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
61		eqid 2423	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
62		fvex 5889	. . . . . . . . . . . . . . . . . . . . 21
63		difexg 4570	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^
64	62, 63	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^
65	60, 61, 64	fvmpt 5962	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
66	65	eleq1d 2492	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
67	65	fveq2d 5883	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
68	67	eleq1d 2492	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
69	66, 68	anbi12d 716	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
70	69	ralbiia 2856	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
71		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20
72		oveq2 6311	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
73	72	iuneq1d 4322	. . . . . . . . . . . . . . . . . . . 20 ..^ ..^
74	71, 73	difeq12d 3585	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
75	74	eleq1d 2492	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
76	74	fveq2d 5883	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
77	76	eleq1d 2492	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
78	75, 77	anbi12d 716	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
79	78	cbvralv 3056	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
80	70, 79	bitri 253	. . . . . . . . . . . . . . 15 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
81	56, 80	sylibr 216	. . . . . . . . . . . . . 14 $/\$ $\$ ..^ $/\$ $\$ ..^
82		fveq2 5879	. . . . . . . . . . . . . . . 16
83	82	iundisj2 22494	. . . . . . . . . . . . . . 15 Disj $\$ ..^
84		disjeq2 4396	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^ Disj $\$ ..^ Disj $\$ ..^
85	84, 65	mprg 2789	. . . . . . . . . . . . . . 15 Disj $\$ ..^ Disj $\$ ..^
86	83, 85	mpbir 213	. . . . . . . . . . . . . 14 Disj $\$ ..^
87		nnex 10617	. . . . . . . . . . . . . . . . 17
88	87	mptex 6149	. . . . . . . . . . . . . . . 16 $\$ ..^
89		fveq1 5878	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
90	89	eleq1d 2492	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
91	89	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
92	91	eleq1d 2492	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
93	90, 92	anbi12d 716	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^ $/\$ $\$ ..^
94	93	ralbidv 2865	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $/\$ $\$ ..^ $/\$ $\$ ..^
95	89	adantr 467	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^
96	95	disjeq2dv 4397	. . . . . . . . . . . . . . . . . 18 $\$ ..^ Disj Disj $\$ ..^
97	94, 96	anbi12d 716	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $/\$ Disj $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^
98	89	iuneq2d 4324	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
99	98	fveq2d 5883	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
100		voliunnfl.1	. . . . . . . . . . . . . . . . . . . . . 22
101		voliunnfl.2	. . . . . . . . . . . . . . . . . . . . . . 23
102		seqeq3 12219	. . . . . . . . . . . . . . . . . . . . . . 23
103	101, 102	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
104	100, 103	eqtri 2452	. . . . . . . . . . . . . . . . . . . . 21
105	104	rneqi 5078	. . . . . . . . . . . . . . . . . . . 20
106	105	supeq1i 7965	. . . . . . . . . . . . . . . . . . 19
107	91	mpteq2dv 4509	. . . . . . . . . . . . . . . . . . . . . 22 $\$ ..^ $\$ ..^
108	107	seqeq3d 12222	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
109	108	rneqd 5079	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
110	109	supeq1d 7964	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
111	106, 110	syl5eq 2476	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
112	99, 111	eqeq12d 2445	. . . . . . . . . . . . . . . . 17 $\$ ..^ $\$ ..^ $\$ ..^
113	97, 112	imbi12d 322	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $/\$ Disj $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
114		voliunnfl.3	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Disj
115	88, 113, 114	vtocl 3134	. . . . . . . . . . . . . . 15 $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
116	65	iuneq2i 4316	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^
117	116	fveq2i 5882	. . . . . . . . . . . . . . 15 $\$ ..^ $\$ ..^
118	67	mpteq2ia 4504	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
119		seqeq3 12219	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^ $\$ ..^ $\$ ..^
120	118, 119	ax-mp 5	. . . . . . . . . . . . . . . . 17 $\$ ..^ $\$ ..^
121	120	rneqi 5078	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^
122	121	supeq1i 7965	. . . . . . . . . . . . . . 15 $\$ ..^ $\$ ..^
123	115, 117, 122	3eqtr3g 2487	. . . . . . . . . . . . . 14 $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
124	81, 86, 123	sylancl 667	. . . . . . . . . . . . 13 $/\$ $\$ ..^ $\$ ..^
125	124	adantl 468	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^ $\$ ..^
126	82	iundisj 22493	. . . . . . . . . . . . . . . 16 $\$ ..^
127		fofun 5809	. . . . . . . . . . . . . . . . 17
128		funiunfv 6166	. . . . . . . . . . . . . . . . 17
129	127, 128	syl 17	. . . . . . . . . . . . . . . 16
130	126, 129	syl5eqr 2478	. . . . . . . . . . . . . . 15 $\$ ..^
131	29	unieqd 4227	. . . . . . . . . . . . . . 15
132	130, 131	eqtrd 2464	. . . . . . . . . . . . . 14 $\$ ..^
133	132	fveq2d 5883	. . . . . . . . . . . . 13 $\$ ..^
134	133	adantr 467	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^
135	57	sseq1d 3492	. . . . . . . . . . . . . . . . . . . . 21
136	57	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . 22
137	136	eqeq1d 2425	. . . . . . . . . . . . . . . . . . . . 21
138	135, 137	anbi12d 716	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
139	138	rspccva 3182	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
140		ssdifss 3597	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^
141	140	adantr 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ ..^
142		difss 3593	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^
143		ovolssnul 22432	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^ $/\$ $/\$ $\$ ..^
144	142, 143	mp3an1 1348	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ ..^
145	141, 144	jca 535	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ ..^ $/\$ $\$ ..^
146		nulmbl 22481	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
147		mblvol 22476	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^ $\$ ..^
148	145, 146, 147	3syl 18	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ ..^ $\$ ..^
149	148, 144	eqtrd 2464	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ ..^
150	139, 149	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ ..^
151	150	mpteq2dva 4508	. . . . . . . . . . . . . . . . 17 $/\$ $\$ ..^
152	151	seqeq3d 12222	. . . . . . . . . . . . . . . 16 $/\$ $\$ ..^
153	152	rneqd 5079	. . . . . . . . . . . . . . 15 $/\$ $\$ ..^
154	153	supeq1d 7964	. . . . . . . . . . . . . 14 $/\$ $\$ ..^
155		0cn 9637	. . . . . . . . . . . . . . . . . . . . . 22
156		ser1const 12270	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
157	155, 156	mpan 675	. . . . . . . . . . . . . . . . . . . . 21
158		nncn 10619	. . . . . . . . . . . . . . . . . . . . . 22
159	158	mul01d 9834	. . . . . . . . . . . . . . . . . . . . 21
160	157, 159	eqtrd 2464	. . . . . . . . . . . . . . . . . . . 20
161	160	mpteq2ia 4504	. . . . . . . . . . . . . . . . . . 19
162		fconstmpt 4895	. . . . . . . . . . . . . . . . . . . . 21
163		seqeq3 12219	. . . . . . . . . . . . . . . . . . . . 21
164	162, 163	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
165		1z 10969	. . . . . . . . . . . . . . . . . . . . . 22
166		seqfn 12226	. . . . . . . . . . . . . . . . . . . . . 22
167	165, 166	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
168		nnuz 11196	. . . . . . . . . . . . . . . . . . . . . . 23
169	168	fneq2i 5687	. . . . . . . . . . . . . . . . . . . . . 22
170		dffn5 5924	. . . . . . . . . . . . . . . . . . . . . 22
171	169, 170	bitr3i 255	. . . . . . . . . . . . . . . . . . . . 21
172	167, 171	mpbi 212	. . . . . . . . . . . . . . . . . . . 20
173	164, 172	eqtr3i 2454	. . . . . . . . . . . . . . . . . . 19
174		fconstmpt 4895	. . . . . . . . . . . . . . . . . . 19
175	161, 173, 174	3eqtr4i 2462	. . . . . . . . . . . . . . . . . 18
176	175	rneqi 5078	. . . . . . . . . . . . . . . . 17
177		1nn 10622	. . . . . . . . . . . . . . . . . 18
178		ne0i 3768	. . . . . . . . . . . . . . . . . 18
179		rnxp 5284	. . . . . . . . . . . . . . . . . 18
180	177, 178, 179	mp2b 10	. . . . . . . . . . . . . . . . 17
181	176, 180	eqtri 2452	. . . . . . . . . . . . . . . 16
182	181	supeq1i 7965	. . . . . . . . . . . . . . 15
183		xrltso 11442	. . . . . . . . . . . . . . . 16
184		0xr 9689	. . . . . . . . . . . . . . . 16
185		supsn 7992	. . . . . . . . . . . . . . . 16 $/\$
186	183, 184, 185	mp2an 677	. . . . . . . . . . . . . . 15
187	182, 186	eqtri 2452	. . . . . . . . . . . . . 14
188	154, 187	syl6eq 2480	. . . . . . . . . . . . 13 $/\$ $\$ ..^
189	188	adantl 468	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^
190	125, 134, 189	3eqtr3rd 2473	. . . . . . . . . . 11 $/\$ $/\$
191	190	ex 436	. . . . . . . . . 10 $/\$
192	39, 191	sylbid 219	. . . . . . . . 9 $/\$
193	28, 192	syl5 34	. . . . . . . 8 $/\$
194	193	exlimiv 1767	. . . . . . 7 $/\$
195	18, 194	syl 17	. . . . . 6 $/\$ $/\$
196	195	expimpd 607	. . . . 5 $/\$ $/\$
197	11, 196	pm2.61ine 2738	. . . 4 $/\$ $/\$
198		renepnf 9690	. . . . . . 7
199	48, 198	mp1i 13	. . . . . 6
200		fveq2 5879	. . . . . . 7
201		rembl 22486	. . . . . . . . 9
202		mblvol 22476	. . . . . . . . 9
203	201, 202	ax-mp 5	. . . . . . . 8
204		ovolre 22471	. . . . . . . 8
205	203, 204	eqtri 2452	. . . . . . 7
206	200, 205	syl6eq 2480	. . . . . 6
207	199, 206	neeqtrrd 2725	. . . . 5
208	207	necon2i 2668	. . . 4
209	197, 208	syl 17	. . 3 $/\$ $/\$
210	209	expr 619	. 2 $/\$
211		eqimss 3517	. . 3
212	211	necon3bi 2654	. 2
213	210, 212	pm2.61d1 163	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $/\$ wa 371

wceq 1438

wex 1660

wcel 1869

wne 2619

wral 2776

cvv 3082 $\$ cdif 3434

wss 3437

c0 3762

csn 3997

cuni 4217

ciun 4297 Disj wdisj 4392 class class class wbr 4421

cmpt 4480

wor 4771

cxp 4849

cdm 4851

crn 4852

cima 4854

wfun 5593

wfn 5594

wfo 5597

cfv 5599 (class class class)co 6303

cdom 7573

csdm 7574

csup 7958

cc 9539

cr 9540

cc0 9541

c1 9542

caddc 9544

cmul 9546

cpnf 9674

cxr 9676

clt 9677

cn 10611

cz 10939

cuz 11161 ..^cfzo 11917

cseq 12214

covol 22405

cvol 22407

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-rep 4534 ax-sep 4544 ax-nul 4553 ax-pow 4600 ax-pr 4658 ax-un 6595 ax-inf2 8150 ax-cnex 9597 ax-resscn 9598 ax-1cn 9599 ax-icn 9600 ax-addcl 9601 ax-addrcl 9602 ax-mulcl 9603 ax-mulrcl 9604 ax-mulcom 9605 ax-addass 9606 ax-mulass 9607 ax-distr 9608 ax-i2m1 9609 ax-1ne0 9610 ax-1rid 9611 ax-rnegex 9612 ax-rrecex 9613 ax-cnre 9614 ax-pre-lttri 9615 ax-pre-lttrn 9616 ax-pre-ltadd 9617 ax-pre-mulgt0 9618 ax-pre-sup 9619

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 984 df-3an 985 df-tru 1441 df-fal 1444 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-nel 2622 df-ral 2781 df-rex 2782 df-reu 2783 df-rmo 2784 df-rab 2785 df-v 3084 df-sbc 3301 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-pss 3453 df-nul 3763 df-if 3911 df-pw 3982 df-sn 3998 df-pr 4000 df-tp 4002 df-op 4004 df-uni 4218 df-int 4254 df-iun 4299 df-disj 4393 df-br 4422 df-opab 4481 df-mpt 4482 df-tr 4517 df-eprel 4762 df-id 4766 df-po 4772 df-so 4773 df-fr 4810 df-se 4811 df-we 4812 df-xp 4857 df-rel 4858 df-cnv 4859 df-co 4860 df-dm 4861 df-rn 4862 df-res 4863 df-ima 4864 df-pred 5397 df-ord 5443 df-on 5444 df-lim 5445 df-suc 5446 df-iota 5563 df-fun 5601 df-fn 5602 df-f 5603 df-f1 5604 df-fo 5605 df-f1o 5606 df-fv 5607 df-isom 5608 df-riota 6265 df-ov 6306 df-oprab 6307 df-mpt2 6308 df-of 6543 df-om 6705 df-1st 6805 df-2nd 6806 df-wrecs 7034 df-recs 7096 df-rdg 7134 df-1o 7188 df-2o 7189 df-oadd 7192 df-er 7369 df-map 7480 df-en 7576 df-dom 7577 df-sdom 7578 df-fin 7579 df-fi 7929 df-sup 7960 df-inf 7961 df-oi 8029 df-card 8376 df-cda 8600 df-pnf 9679 df-mnf 9680 df-xr 9681 df-ltxr 9682 df-le 9683 df-sub 9864 df-neg 9865 df-div 10272 df-nn 10612 df-2 10670 df-3 10671 df-n0 10872 df-z 10940 df-uz 11162 df-q 11267 df-rp 11305 df-xneg 11411 df-xadd 11412 df-xmul 11413 df-ioo 11641 df-ico 11643 df-icc 11644 df-fz 11787 df-fzo 11918 df-fl 12029 df-seq 12215 df-exp 12274 df-hash 12517 df-cj 13156 df-re 13157 df-im 13158 df-sqrt 13292 df-abs 13293 df-clim 13545 df-sum 13746 df-rest 15314 df-topgen 15335 df-psmet 18955 df-xmet 18956 df-met 18957 df-bl 18958 df-mopn 18959 df-top 19913 df-bases 19914 df-topon 19915 df-cmp 20394 df-ovol 22408 df-vol 22410

This theorem is referenced by: (None)

W3C validator