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 30033

Description: voliun 21837 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 4242	. . . . . . . . 9
2		uni0 4261	. . . . . . . . 9
3	1, 2	syl6eq 2500	. . . . . . . 8
4	3	fveq2d 5860	. . . . . . 7
5		0mbl 21823	. . . . . . . . 9
6		mblvol 21814	. . . . . . . . 9
7	5, 6	ax-mp 5	. . . . . . . 8
8		ovol0 21777	. . . . . . . 8
9	7, 8	eqtri 2472	. . . . . . 7
10	4, 9	syl6req 2501	. . . . . 6
11	10	a1d 25	. . . . 5 $/\$ $/\$
12		reldom 7524	. . . . . . . . . . 11
13	12	brrelexi 5030	. . . . . . . . . 10
14		0sdomg 7648	. . . . . . . . . 10
15	13, 14	syl 16	. . . . . . . . 9
16	15	biimparc 487	. . . . . . . 8 $/\$
17		fodomr 7670	. . . . . . . 8 $/\$
18	16, 17	sylancom 667	. . . . . . 7 $/\$
19		unissb 4266	. . . . . . . . . . . . 13
20	19	anbi1i 695	. . . . . . . . . . . 12 $/\$ $/\$
21		r19.26 2970	. . . . . . . . . . . 12 $/\$ $/\$
22	20, 21	bitr4i 252	. . . . . . . . . . 11 $/\$ $/\$
23		ovolctb2 21776	. . . . . . . . . . . . . 14 $/\$
24	23	ex 434	. . . . . . . . . . . . 13
25	24	imdistani 690	. . . . . . . . . . . 12 $/\$ $/\$
26	25	ralimi 2836	. . . . . . . . . . 11 $/\$ $/\$
27	22, 26	sylbi 195	. . . . . . . . . 10 $/\$ $/\$
28	27	ancoms 453	. . . . . . . . 9 $/\$ $/\$
29		foima 5790	. . . . . . . . . . . 12
30	29	raleqdv 3046	. . . . . . . . . . 11 $/\$ $/\$
31		fofn 5787	. . . . . . . . . . . 12
32		ssid 3508	. . . . . . . . . . . 12
33		sseq1 3510	. . . . . . . . . . . . . 14
34		fveq2 5856	. . . . . . . . . . . . . . 15
35	34	eqeq1d 2445	. . . . . . . . . . . . . 14
36	33, 35	anbi12d 710	. . . . . . . . . . . . 13 $/\$ $/\$
37	36	ralima 6137	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
38	31, 32, 37	sylancl 662	. . . . . . . . . . 11 $/\$ $/\$
39	30, 38	bitr3d 255	. . . . . . . . . 10 $/\$ $/\$
40		difss 3616	. . . . . . . . . . . . . . . . . 18 $\$ ..^
41		ovolssnul 21771	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $/\$ $/\$ $\$ ..^
42	40, 41	mp3an1 1312	. . . . . . . . . . . . . . . . 17 $/\$ $\$ ..^
43		ssdifss 3620	. . . . . . . . . . . . . . . . . 18 $\$ ..^
44		nulmbl 21819	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
45		mblvol 21814	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ ..^ $\$ ..^ $\$ ..^
46	45	eqeq1d 2445	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ ..^ $\$ ..^ $\$ ..^
47	46	biimpar 485	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
48		0re 9599	. . . . . . . . . . . . . . . . . . . . . . 23
49	47, 48	syl6eqel 2539	. . . . . . . . . . . . . . . . . . . . . 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 2836	. . . . . . . . . . . . . . 15 $/\$ $\$ ..^ $/\$ $\$ ..^
57		fveq2 5856	. . . . . . . . . . . . . . . . . . . . 21
58		oveq2 6289	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
59	58	iuneq1d 4340	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
60	57, 59	difeq12d 3608	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
61		eqid 2443	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
62		fvex 5866	. . . . . . . . . . . . . . . . . . . . 21
63		difexg 4585	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^
64	62, 63	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^
65	60, 61, 64	fvmpt 5941	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
66	65	eleq1d 2512	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
67	65	fveq2d 5860	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
68	67	eleq1d 2512	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
69	66, 68	anbi12d 710	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
70	69	ralbiia 2873	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
71		fveq2 5856	. . . . . . . . . . . . . . . . . . . 20
72		oveq2 6289	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
73	72	iuneq1d 4340	. . . . . . . . . . . . . . . . . . . 20 ..^ ..^
74	71, 73	difeq12d 3608	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
75	74	eleq1d 2512	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
76	74	fveq2d 5860	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
77	76	eleq1d 2512	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
78	75, 77	anbi12d 710	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
79	78	cbvralv 3070	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
80	70, 79	bitri 249	. . . . . . . . . . . . . . 15 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
81	56, 80	sylibr 212	. . . . . . . . . . . . . 14 $/\$ $\$ ..^ $/\$ $\$ ..^
82		fveq2 5856	. . . . . . . . . . . . . . . 16
83	82	iundisj2 21832	. . . . . . . . . . . . . . 15 Disj $\$ ..^
84		disjeq2 4411	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^ Disj $\$ ..^ Disj $\$ ..^
85	84, 65	mprg 2806	. . . . . . . . . . . . . . 15 Disj $\$ ..^ Disj $\$ ..^
86	83, 85	mpbir 209	. . . . . . . . . . . . . 14 Disj $\$ ..^
87		nnex 10548	. . . . . . . . . . . . . . . . 17
88	87	mptex 6128	. . . . . . . . . . . . . . . 16 $\$ ..^
89		fveq1 5855	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
90	89	eleq1d 2512	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
91	89	fveq2d 5860	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
92	91	eleq1d 2512	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
93	90, 92	anbi12d 710	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^ $/\$ $\$ ..^
94	93	ralbidv 2882	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $/\$ $\$ ..^ $/\$ $\$ ..^
95	89	adantr 465	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^
96	95	disjeq2dv 4412	. . . . . . . . . . . . . . . . . 18 $\$ ..^ Disj Disj $\$ ..^
97	94, 96	anbi12d 710	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $/\$ Disj $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^
98	89	iuneq2d 4342	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
99	98	fveq2d 5860	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
100		voliunnfl.1	. . . . . . . . . . . . . . . . . . . . . 22
101		voliunnfl.2	. . . . . . . . . . . . . . . . . . . . . . 23
102		seqeq3 12091	. . . . . . . . . . . . . . . . . . . . . . 23
103	101, 102	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
104	100, 103	eqtri 2472	. . . . . . . . . . . . . . . . . . . . 21
105	104	rneqi 5219	. . . . . . . . . . . . . . . . . . . 20
106	105	supeq1i 7909	. . . . . . . . . . . . . . . . . . 19
107	91	mpteq2dv 4524	. . . . . . . . . . . . . . . . . . . . . 22 $\$ ..^ $\$ ..^
108	107	seqeq3d 12094	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
109	108	rneqd 5220	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
110	109	supeq1d 7908	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
111	106, 110	syl5eq 2496	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
112	99, 111	eqeq12d 2465	. . . . . . . . . . . . . . . . 17 $\$ ..^ $\$ ..^ $\$ ..^
113	97, 112	imbi12d 320	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $/\$ Disj $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
114		voliunnfl.3	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Disj
115	88, 113, 114	vtocl 3147	. . . . . . . . . . . . . . 15 $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
116	65	iuneq2i 4334	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^
117	116	fveq2i 5859	. . . . . . . . . . . . . . 15 $\$ ..^ $\$ ..^
118	67	mpteq2ia 4519	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
119		seqeq3 12091	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^ $\$ ..^ $\$ ..^
120	118, 119	ax-mp 5	. . . . . . . . . . . . . . . . 17 $\$ ..^ $\$ ..^
121	120	rneqi 5219	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^
122	121	supeq1i 7909	. . . . . . . . . . . . . . 15 $\$ ..^ $\$ ..^
123	115, 117, 122	3eqtr3g 2507	. . . . . . . . . . . . . 14 $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
124	81, 86, 123	sylancl 662	. . . . . . . . . . . . 13 $/\$ $\$ ..^ $\$ ..^
125	124	adantl 466	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^ $\$ ..^
126	82	iundisj 21831	. . . . . . . . . . . . . . . 16 $\$ ..^
127		fofun 5786	. . . . . . . . . . . . . . . . 17
128		funiunfv 6145	. . . . . . . . . . . . . . . . 17
129	127, 128	syl 16	. . . . . . . . . . . . . . . 16
130	126, 129	syl5eqr 2498	. . . . . . . . . . . . . . 15 $\$ ..^
131	29	unieqd 4244	. . . . . . . . . . . . . . 15
132	130, 131	eqtrd 2484	. . . . . . . . . . . . . 14 $\$ ..^
133	132	fveq2d 5860	. . . . . . . . . . . . 13 $\$ ..^
134	133	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^
135	57	sseq1d 3516	. . . . . . . . . . . . . . . . . . . . 21
136	57	fveq2d 5860	. . . . . . . . . . . . . . . . . . . . . 22
137	136	eqeq1d 2445	. . . . . . . . . . . . . . . . . . . . 21
138	135, 137	anbi12d 710	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
139	138	rspccva 3195	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
140		ssdifss 3620	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^
141	140	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ ..^
142		difss 3616	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^
143		ovolssnul 21771	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^ $/\$ $/\$ $\$ ..^
144	142, 143	mp3an1 1312	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ ..^
145	141, 144	jca 532	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ ..^ $/\$ $\$ ..^
146		nulmbl 21819	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
147		mblvol 21814	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^ $\$ ..^
148	145, 146, 147	3syl 20	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ ..^ $\$ ..^
149	148, 144	eqtrd 2484	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ ..^
150	139, 149	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ ..^
151	150	mpteq2dva 4523	. . . . . . . . . . . . . . . . 17 $/\$ $\$ ..^
152	151	seqeq3d 12094	. . . . . . . . . . . . . . . 16 $/\$ $\$ ..^
153	152	rneqd 5220	. . . . . . . . . . . . . . 15 $/\$ $\$ ..^
154	153	supeq1d 7908	. . . . . . . . . . . . . 14 $/\$ $\$ ..^
155		0cn 9591	. . . . . . . . . . . . . . . . . . . . . 22
156		ser1const 12142	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
157	155, 156	mpan 670	. . . . . . . . . . . . . . . . . . . . 21
158		nncn 10550	. . . . . . . . . . . . . . . . . . . . . 22
159	158	mul01d 9782	. . . . . . . . . . . . . . . . . . . . 21
160	157, 159	eqtrd 2484	. . . . . . . . . . . . . . . . . . . 20
161	160	mpteq2ia 4519	. . . . . . . . . . . . . . . . . . 19
162		fconstmpt 5033	. . . . . . . . . . . . . . . . . . . . 21
163		seqeq3 12091	. . . . . . . . . . . . . . . . . . . . 21
164	162, 163	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
165		1z 10900	. . . . . . . . . . . . . . . . . . . . . 22
166		seqfn 12098	. . . . . . . . . . . . . . . . . . . . . 22
167	165, 166	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
168		nnuz 11125	. . . . . . . . . . . . . . . . . . . . . . 23
169	168	fneq2i 5666	. . . . . . . . . . . . . . . . . . . . . 22
170		dffn5 5903	. . . . . . . . . . . . . . . . . . . . . 22
171	169, 170	bitr3i 251	. . . . . . . . . . . . . . . . . . . . 21
172	167, 171	mpbi 208	. . . . . . . . . . . . . . . . . . . 20
173	164, 172	eqtr3i 2474	. . . . . . . . . . . . . . . . . . 19
174		fconstmpt 5033	. . . . . . . . . . . . . . . . . . 19
175	161, 173, 174	3eqtr4i 2482	. . . . . . . . . . . . . . . . . 18
176	175	rneqi 5219	. . . . . . . . . . . . . . . . 17
177		1nn 10553	. . . . . . . . . . . . . . . . . 18
178		ne0i 3776	. . . . . . . . . . . . . . . . . 18
179		rnxp 5427	. . . . . . . . . . . . . . . . . 18
180	177, 178, 179	mp2b 10	. . . . . . . . . . . . . . . . 17
181	176, 180	eqtri 2472	. . . . . . . . . . . . . . . 16
182	181	supeq1i 7909	. . . . . . . . . . . . . . 15
183		xrltso 11356	. . . . . . . . . . . . . . . 16
184		0xr 9643	. . . . . . . . . . . . . . . 16
185		supsn 7933	. . . . . . . . . . . . . . . 16 $/\$
186	183, 184, 185	mp2an 672	. . . . . . . . . . . . . . 15
187	182, 186	eqtri 2472	. . . . . . . . . . . . . 14
188	154, 187	syl6eq 2500	. . . . . . . . . . . . 13 $/\$ $\$ ..^
189	188	adantl 466	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^
190	125, 134, 189	3eqtr3rd 2493	. . . . . . . . . . 11 $/\$ $/\$
191	190	ex 434	. . . . . . . . . 10 $/\$
192	39, 191	sylbid 215	. . . . . . . . 9 $/\$
193	28, 192	syl5 32	. . . . . . . 8 $/\$
194	193	exlimiv 1709	. . . . . . 7 $/\$
195	18, 194	syl 16	. . . . . 6 $/\$ $/\$
196	195	expimpd 603	. . . . 5 $/\$ $/\$
197	11, 196	pm2.61ine 2756	. . . 4 $/\$ $/\$
198		renepnf 9644	. . . . . . 7
199	48, 198	mp1i 12	. . . . . 6
200		fveq2 5856	. . . . . . 7
201		rembl 21824	. . . . . . . . 9
202		mblvol 21814	. . . . . . . . 9
203	201, 202	ax-mp 5	. . . . . . . 8
204		ovolre 21809	. . . . . . . 8
205	203, 204	eqtri 2472	. . . . . . 7
206	200, 205	syl6eq 2500	. . . . . 6
207	199, 206	neeqtrrd 2743	. . . . 5
208	207	necon2i 2686	. . . 4
209	197, 208	syl 16	. . 3 $/\$ $/\$
210	209	expr 615	. 2 $/\$
211		eqimss 3541	. . 3
212	211	necon3bi 2672	. 2
213	210, 212	pm2.61d1 159	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369

wceq 1383

wex 1599

wcel 1804

wne 2638

wral 2793

cvv 3095 $\$ cdif 3458

wss 3461

c0 3770

csn 4014

cuni 4234

ciun 4315 Disj wdisj 4407 class class class wbr 4437

cmpt 4495

wor 4789

cxp 4987

cdm 4989

crn 4990

cima 4992

wfun 5572

wfn 5573

wfo 5576

cfv 5578 (class class class)co 6281

cdom 7516

csdm 7517

csup 7902

cc 9493

cr 9494

cc0 9495

c1 9496

caddc 9498

cmul 9500

cpnf 9628

cxr 9630

clt 9631

cn 10542

cz 10870

cuz 11090 ..^cfzo 11803

cseq 12086

covol 21747

cvol 21748

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-8 1806 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-rep 4548 ax-sep 4558 ax-nul 4566 ax-pow 4615 ax-pr 4676 ax-un 6577 ax-inf2 8061 ax-cnex 9551 ax-resscn 9552 ax-1cn 9553 ax-icn 9554 ax-addcl 9555 ax-addrcl 9556 ax-mulcl 9557 ax-mulrcl 9558 ax-mulcom 9559 ax-addass 9560 ax-mulass 9561 ax-distr 9562 ax-i2m1 9563 ax-1ne0 9564 ax-1rid 9565 ax-rnegex 9566 ax-rrecex 9567 ax-cnre 9568 ax-pre-lttri 9569 ax-pre-lttrn 9570 ax-pre-ltadd 9571 ax-pre-mulgt0 9572 ax-pre-sup 9573

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 975 df-3an 976 df-tru 1386 df-fal 1389 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-nel 2641 df-ral 2798 df-rex 2799 df-reu 2800 df-rmo 2801 df-rab 2802 df-v 3097 df-sbc 3314 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3771 df-if 3927 df-pw 3999 df-sn 4015 df-pr 4017 df-tp 4019 df-op 4021 df-uni 4235 df-int 4272 df-iun 4317 df-disj 4408 df-br 4438 df-opab 4496 df-mpt 4497 df-tr 4531 df-eprel 4781 df-id 4785 df-po 4790 df-so 4791 df-fr 4828 df-se 4829 df-we 4830 df-ord 4871 df-on 4872 df-lim 4873 df-suc 4874 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-res 5001 df-ima 5002 df-iota 5541 df-fun 5580 df-fn 5581 df-f 5582 df-f1 5583 df-fo 5584 df-f1o 5585 df-fv 5586 df-isom 5587 df-riota 6242 df-ov 6284 df-oprab 6285 df-mpt2 6286 df-of 6525 df-om 6686 df-1st 6785 df-2nd 6786 df-recs 7044 df-rdg 7078 df-1o 7132 df-2o 7133 df-oadd 7136 df-er 7313 df-map 7424 df-en 7519 df-dom 7520 df-sdom 7521 df-fin 7522 df-fi 7873 df-sup 7903 df-oi 7938 df-card 8323 df-cda 8551 df-pnf 9633 df-mnf 9634 df-xr 9635 df-ltxr 9636 df-le 9637 df-sub 9812 df-neg 9813 df-div 10213 df-nn 10543 df-2 10600 df-3 10601 df-n0 10802 df-z 10871 df-uz 11091 df-q 11192 df-rp 11230 df-xneg 11327 df-xadd 11328 df-xmul 11329 df-ioo 11542 df-ico 11544 df-icc 11545 df-fz 11682 df-fzo 11804 df-fl 11908 df-seq 12087 df-exp 12146 df-hash 12385 df-cj 12911 df-re 12912 df-im 12913 df-sqrt 13047 df-abs 13048 df-clim 13290 df-sum 13488 df-rest 14697 df-topgen 14718 df-psmet 18285 df-xmet 18286 df-met 18287 df-bl 18288 df-mopn 18289 df-top 19272 df-bases 19274 df-topon 19275 df-cmp 19760 df-ovol 21749 df-vol 21750

This theorem is referenced by: (None)

W3C validator