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 28438

Description: voliun 21038 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 4102	. . . . . . . . 9
2		uni0 4121	. . . . . . . . 9
3	1, 2	syl6eq 2491	. . . . . . . 8
4	3	fveq2d 5698	. . . . . . 7
5		0mbl 21024	. . . . . . . . 9
6		mblvol 21016	. . . . . . . . 9
7	5, 6	ax-mp 5	. . . . . . . 8
8		ovol0 20979	. . . . . . . 8
9	7, 8	eqtri 2463	. . . . . . 7
10	4, 9	syl6req 2492	. . . . . 6
11	10	a1d 25	. . . . 5 $/\$ $/\$
12		reldom 7319	. . . . . . . . . . 11
13	12	brrelexi 4882	. . . . . . . . . 10
14		0sdomg 7443	. . . . . . . . . 10
15	13, 14	syl 16	. . . . . . . . 9
16	15	biimparc 487	. . . . . . . 8 $/\$
17		fodomr 7465	. . . . . . . 8 $/\$
18	16, 17	sylancom 667	. . . . . . 7 $/\$
19		unissb 4126	. . . . . . . . . . . . 13
20	19	anbi1i 695	. . . . . . . . . . . 12 $/\$ $/\$
21		r19.26 2852	. . . . . . . . . . . 12 $/\$ $/\$
22	20, 21	bitr4i 252	. . . . . . . . . . 11 $/\$ $/\$
23		ovolctb2 20978	. . . . . . . . . . . . . 14 $/\$
24	23	ex 434	. . . . . . . . . . . . 13
25	24	imdistani 690	. . . . . . . . . . . 12 $/\$ $/\$
26	25	ralimi 2794	. . . . . . . . . . 11 $/\$ $/\$
27	22, 26	sylbi 195	. . . . . . . . . 10 $/\$ $/\$
28	27	ancoms 453	. . . . . . . . 9 $/\$ $/\$
29		foima 5628	. . . . . . . . . . . 12
30	29	raleqdv 2926	. . . . . . . . . . 11 $/\$ $/\$
31		fofn 5625	. . . . . . . . . . . 12
32		ssid 3378	. . . . . . . . . . . 12
33		sseq1 3380	. . . . . . . . . . . . . 14
34		fveq2 5694	. . . . . . . . . . . . . . 15
35	34	eqeq1d 2451	. . . . . . . . . . . . . 14
36	33, 35	anbi12d 710	. . . . . . . . . . . . 13 $/\$ $/\$
37	36	ralima 5960	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
38	31, 32, 37	sylancl 662	. . . . . . . . . . 11 $/\$ $/\$
39	30, 38	bitr3d 255	. . . . . . . . . 10 $/\$ $/\$
40		difss 3486	. . . . . . . . . . . . . . . . . 18 $\$ ..^
41		ovolssnul 20973	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $/\$ $/\$ $\$ ..^
42	40, 41	mp3an1 1301	. . . . . . . . . . . . . . . . 17 $/\$ $\$ ..^
43		ssdifss 3490	. . . . . . . . . . . . . . . . . 18 $\$ ..^
44		nulmbl 21020	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
45		mblvol 21016	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ ..^ $\$ ..^ $\$ ..^
46	45	eqeq1d 2451	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ ..^ $\$ ..^ $\$ ..^
47	46	biimpar 485	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
48		0re 9389	. . . . . . . . . . . . . . . . . . . . . . 23
49	47, 48	syl6eqel 2531	. . . . . . . . . . . . . . . . . . . . . 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 2794	. . . . . . . . . . . . . . 15 $/\$ $\$ ..^ $/\$ $\$ ..^
57		fveq2 5694	. . . . . . . . . . . . . . . . . . . . 21
58		oveq2 6102	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
59	58	iuneq1d 4198	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
60	57, 59	difeq12d 3478	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
61		eqid 2443	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
62		fvex 5704	. . . . . . . . . . . . . . . . . . . . 21
63		difexg 4443	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^
64	62, 63	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^
65	60, 61, 64	fvmpt 5777	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
66	65	eleq1d 2509	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
67	65	fveq2d 5698	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
68	67	eleq1d 2509	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
69	66, 68	anbi12d 710	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
70	69	ralbiia 2750	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
71		fveq2 5694	. . . . . . . . . . . . . . . . . . . 20
72		oveq2 6102	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
73	72	iuneq1d 4198	. . . . . . . . . . . . . . . . . . . 20 ..^ ..^
74	71, 73	difeq12d 3478	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
75	74	eleq1d 2509	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
76	74	fveq2d 5698	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
77	76	eleq1d 2509	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
78	75, 77	anbi12d 710	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
79	78	cbvralv 2950	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
80	70, 79	bitri 249	. . . . . . . . . . . . . . 15 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
81	56, 80	sylibr 212	. . . . . . . . . . . . . 14 $/\$ $\$ ..^ $/\$ $\$ ..^
82		fveq2 5694	. . . . . . . . . . . . . . . 16
83	82	iundisj2 21033	. . . . . . . . . . . . . . 15 Disj $\$ ..^
84		disjeq2 4269	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^ Disj $\$ ..^ Disj $\$ ..^
85	84, 65	mprg 2788	. . . . . . . . . . . . . . 15 Disj $\$ ..^ Disj $\$ ..^
86	83, 85	mpbir 209	. . . . . . . . . . . . . 14 Disj $\$ ..^
87		nnex 10331	. . . . . . . . . . . . . . . . 17
88	87	mptex 5951	. . . . . . . . . . . . . . . 16 $\$ ..^
89		fveq1 5693	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
90	89	eleq1d 2509	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
91	89	fveq2d 5698	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
92	91	eleq1d 2509	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
93	90, 92	anbi12d 710	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^ $/\$ $\$ ..^
94	93	ralbidv 2738	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $/\$ $\$ ..^ $/\$ $\$ ..^
95	89	adantr 465	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^
96	95	disjeq2dv 4270	. . . . . . . . . . . . . . . . . 18 $\$ ..^ Disj Disj $\$ ..^
97	94, 96	anbi12d 710	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $/\$ Disj $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^
98	89	iuneq2d 4200	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
99	98	fveq2d 5698	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
100		voliunnfl.1	. . . . . . . . . . . . . . . . . . . . . 22
101		voliunnfl.2	. . . . . . . . . . . . . . . . . . . . . . 23
102		seqeq3 11814	. . . . . . . . . . . . . . . . . . . . . . 23
103	101, 102	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
104	100, 103	eqtri 2463	. . . . . . . . . . . . . . . . . . . . 21
105	104	rneqi 5069	. . . . . . . . . . . . . . . . . . . 20
106	105	supeq1i 7700	. . . . . . . . . . . . . . . . . . 19
107	91	mpteq2dv 4382	. . . . . . . . . . . . . . . . . . . . . 22 $\$ ..^ $\$ ..^
108	107	seqeq3d 11817	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
109	108	rneqd 5070	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
110	109	supeq1d 7699	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
111	106, 110	syl5eq 2487	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
112	99, 111	eqeq12d 2457	. . . . . . . . . . . . . . . . 17 $\$ ..^ $\$ ..^ $\$ ..^
113	97, 112	imbi12d 320	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $/\$ Disj $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
114		voliunnfl.3	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Disj
115	88, 113, 114	vtocl 3027	. . . . . . . . . . . . . . 15 $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
116	65	iuneq2i 4192	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^
117	116	fveq2i 5697	. . . . . . . . . . . . . . 15 $\$ ..^ $\$ ..^
118	67	mpteq2ia 4377	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
119		seqeq3 11814	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^ $\$ ..^ $\$ ..^
120	118, 119	ax-mp 5	. . . . . . . . . . . . . . . . 17 $\$ ..^ $\$ ..^
121	120	rneqi 5069	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^
122	121	supeq1i 7700	. . . . . . . . . . . . . . 15 $\$ ..^ $\$ ..^
123	115, 117, 122	3eqtr3g 2498	. . . . . . . . . . . . . 14 $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
124	81, 86, 123	sylancl 662	. . . . . . . . . . . . 13 $/\$ $\$ ..^ $\$ ..^
125	124	adantl 466	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^ $\$ ..^
126	82	iundisj 21032	. . . . . . . . . . . . . . . 16 $\$ ..^
127		fofun 5624	. . . . . . . . . . . . . . . . 17
128		funiunfv 5968	. . . . . . . . . . . . . . . . 17
129	127, 128	syl 16	. . . . . . . . . . . . . . . 16
130	126, 129	syl5eqr 2489	. . . . . . . . . . . . . . 15 $\$ ..^
131	29	unieqd 4104	. . . . . . . . . . . . . . 15
132	130, 131	eqtrd 2475	. . . . . . . . . . . . . 14 $\$ ..^
133	132	fveq2d 5698	. . . . . . . . . . . . 13 $\$ ..^
134	133	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^
135	57	sseq1d 3386	. . . . . . . . . . . . . . . . . . . . 21
136	57	fveq2d 5698	. . . . . . . . . . . . . . . . . . . . . 22
137	136	eqeq1d 2451	. . . . . . . . . . . . . . . . . . . . 21
138	135, 137	anbi12d 710	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
139	138	rspccva 3075	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
140		ssdifss 3490	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^
141	140	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ ..^
142		difss 3486	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^
143		ovolssnul 20973	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^ $/\$ $/\$ $\$ ..^
144	142, 143	mp3an1 1301	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ ..^
145	141, 144	jca 532	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ ..^ $/\$ $\$ ..^
146		nulmbl 21020	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
147		mblvol 21016	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^ $\$ ..^
148	145, 146, 147	3syl 20	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ ..^ $\$ ..^
149	148, 144	eqtrd 2475	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ ..^
150	139, 149	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ ..^
151	150	mpteq2dva 4381	. . . . . . . . . . . . . . . . 17 $/\$ $\$ ..^
152	151	seqeq3d 11817	. . . . . . . . . . . . . . . 16 $/\$ $\$ ..^
153	152	rneqd 5070	. . . . . . . . . . . . . . 15 $/\$ $\$ ..^
154	153	supeq1d 7699	. . . . . . . . . . . . . 14 $/\$ $\$ ..^
155		0cn 9381	. . . . . . . . . . . . . . . . . . . . . 22
156		ser1const 11865	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
157	155, 156	mpan 670	. . . . . . . . . . . . . . . . . . . . 21
158		nncn 10333	. . . . . . . . . . . . . . . . . . . . . 22
159	158	mul01d 9571	. . . . . . . . . . . . . . . . . . . . 21
160	157, 159	eqtrd 2475	. . . . . . . . . . . . . . . . . . . 20
161	160	mpteq2ia 4377	. . . . . . . . . . . . . . . . . . 19
162		fconstmpt 4885	. . . . . . . . . . . . . . . . . . . . 21
163		seqeq3 11814	. . . . . . . . . . . . . . . . . . . . 21
164	162, 163	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
165		1z 10679	. . . . . . . . . . . . . . . . . . . . . 22
166		seqfn 11821	. . . . . . . . . . . . . . . . . . . . . 22
167	165, 166	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
168		nnuz 10899	. . . . . . . . . . . . . . . . . . . . . . 23
169	168	fneq2i 5509	. . . . . . . . . . . . . . . . . . . . . 22
170		dffn5 5740	. . . . . . . . . . . . . . . . . . . . . 22
171	169, 170	bitr3i 251	. . . . . . . . . . . . . . . . . . . . 21
172	167, 171	mpbi 208	. . . . . . . . . . . . . . . . . . . 20
173	164, 172	eqtr3i 2465	. . . . . . . . . . . . . . . . . . 19
174		fconstmpt 4885	. . . . . . . . . . . . . . . . . . 19
175	161, 173, 174	3eqtr4i 2473	. . . . . . . . . . . . . . . . . 18
176	175	rneqi 5069	. . . . . . . . . . . . . . . . 17
177		1nn 10336	. . . . . . . . . . . . . . . . . 18
178		ne0i 3646	. . . . . . . . . . . . . . . . . 18
179		rnxp 5271	. . . . . . . . . . . . . . . . . 18
180	177, 178, 179	mp2b 10	. . . . . . . . . . . . . . . . 17
181	176, 180	eqtri 2463	. . . . . . . . . . . . . . . 16
182	181	supeq1i 7700	. . . . . . . . . . . . . . 15
183		xrltso 11121	. . . . . . . . . . . . . . . 16
184		0xr 9433	. . . . . . . . . . . . . . . 16
185		supsn 7722	. . . . . . . . . . . . . . . 16 $/\$
186	183, 184, 185	mp2an 672	. . . . . . . . . . . . . . 15
187	182, 186	eqtri 2463	. . . . . . . . . . . . . 14
188	154, 187	syl6eq 2491	. . . . . . . . . . . . 13 $/\$ $\$ ..^
189	188	adantl 466	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^
190	125, 134, 189	3eqtr3rd 2484	. . . . . . . . . . 11 $/\$ $/\$
191	190	ex 434	. . . . . . . . . 10 $/\$
192	39, 191	sylbid 215	. . . . . . . . 9 $/\$
193	28, 192	syl5 32	. . . . . . . 8 $/\$
194	193	exlimiv 1688	. . . . . . 7 $/\$
195	18, 194	syl 16	. . . . . 6 $/\$ $/\$
196	195	expimpd 603	. . . . 5 $/\$ $/\$
197	11, 196	pm2.61ine 2690	. . . 4 $/\$ $/\$
198		renepnf 9434	. . . . . . 7
199	48, 198	mp1i 12	. . . . . 6
200		fveq2 5694	. . . . . . 7
201		rembl 21025	. . . . . . . . 9
202		mblvol 21016	. . . . . . . . 9
203	201, 202	ax-mp 5	. . . . . . . 8
204		ovolre 21011	. . . . . . . 8
205	203, 204	eqtri 2463	. . . . . . 7
206	200, 205	syl6eq 2491	. . . . . 6
207	199, 206	neeqtrrd 2635	. . . . 5
208	207	necon2i 2661	. . . 4
209	197, 208	syl 16	. . 3 $/\$ $/\$
210	209	expr 615	. 2 $/\$
211		eqimss 3411	. . 3
212	211	necon3bi 2655	. 2
213	210, 212	pm2.61d1 159	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369

wceq 1369

wex 1586

wcel 1756

wne 2609

wral 2718

cvv 2975 $\$ cdif 3328

wss 3331

c0 3640

csn 3880

cuni 4094

ciun 4174 Disj wdisj 4265 class class class wbr 4295

cmpt 4353

wor 4643

cxp 4841

cdm 4843

crn 4844

cima 4846

wfun 5415

wfn 5416

wfo 5419

cfv 5421 (class class class)co 6094

cdom 7311

csdm 7312

csup 7693

cc 9283

cr 9284

cc0 9285

c1 9286

caddc 9288

cmul 9290

cpnf 9418

cxr 9420

clt 9421

cn 10325

cz 10649

cuz 10864 ..^cfzo 11551

cseq 11809

covol 20949

cvol 20950

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4406 ax-sep 4416 ax-nul 4424 ax-pow 4473 ax-pr 4534 ax-un 6375 ax-inf2 7850 ax-cnex 9341 ax-resscn 9342 ax-1cn 9343 ax-icn 9344 ax-addcl 9345 ax-addrcl 9346 ax-mulcl 9347 ax-mulrcl 9348 ax-mulcom 9349 ax-addass 9350 ax-mulass 9351 ax-distr 9352 ax-i2m1 9353 ax-1ne0 9354 ax-1rid 9355 ax-rnegex 9356 ax-rrecex 9357 ax-cnre 9358 ax-pre-lttri 9359 ax-pre-lttrn 9360 ax-pre-ltadd 9361 ax-pre-mulgt0 9362 ax-pre-sup 9363

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2571 df-ne 2611 df-nel 2612 df-ral 2723 df-rex 2724 df-reu 2725 df-rmo 2726 df-rab 2727 df-v 2977 df-sbc 3190 df-csb 3292 df-dif 3334 df-un 3336 df-in 3338 df-ss 3345 df-pss 3347 df-nul 3641 df-if 3795 df-pw 3865 df-sn 3881 df-pr 3883 df-tp 3885 df-op 3887 df-uni 4095 df-int 4132 df-iun 4176 df-disj 4266 df-br 4296 df-opab 4354 df-mpt 4355 df-tr 4389 df-eprel 4635 df-id 4639 df-po 4644 df-so 4645 df-fr 4682 df-se 4683 df-we 4684 df-ord 4725 df-on 4726 df-lim 4727 df-suc 4728 df-xp 4849 df-rel 4850 df-cnv 4851 df-co 4852 df-dm 4853 df-rn 4854 df-res 4855 df-ima 4856 df-iota 5384 df-fun 5423 df-fn 5424 df-f 5425 df-f1 5426 df-fo 5427 df-f1o 5428 df-fv 5429 df-isom 5430 df-riota 6055 df-ov 6097 df-oprab 6098 df-mpt2 6099 df-of 6323 df-om 6480 df-1st 6580 df-2nd 6581 df-recs 6835 df-rdg 6869 df-1o 6923 df-2o 6924 df-oadd 6927 df-er 7104 df-map 7219 df-en 7314 df-dom 7315 df-sdom 7316 df-fin 7317 df-fi 7664 df-sup 7694 df-oi 7727 df-card 8112 df-cda 8340 df-pnf 9423 df-mnf 9424 df-xr 9425 df-ltxr 9426 df-le 9427 df-sub 9600 df-neg 9601 df-div 9997 df-nn 10326 df-2 10383 df-3 10384 df-n0 10583 df-z 10650 df-uz 10865 df-q 10957 df-rp 10995 df-xneg 11092 df-xadd 11093 df-xmul 11094 df-ioo 11307 df-ico 11309 df-icc 11310 df-fz 11441 df-fzo 11552 df-fl 11645 df-seq 11810 df-exp 11869 df-hash 12107 df-cj 12591 df-re 12592 df-im 12593 df-sqr 12727 df-abs 12728 df-clim 12969 df-sum 13167 df-rest 14364 df-topgen 14385 df-psmet 17812 df-xmet 17813 df-met 17814 df-bl 17815 df-mopn 17816 df-top 18506 df-bases 18508 df-topon 18509 df-cmp 18993 df-ovol 20951 df-vol 20952

This theorem is referenced by: (None)

W3C validator