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 32048

Description: voliun 22586 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 4198	. . . . . . . . 9
2		uni0 4217	. . . . . . . . 9
3	1, 2	syl6eq 2521	. . . . . . . 8
4	3	fveq2d 5883	. . . . . . 7
5		0mbl 22571	. . . . . . . . 9
6		mblvol 22562	. . . . . . . . 9
7	5, 6	ax-mp 5	. . . . . . . 8
8		ovol0 22524	. . . . . . . 8
9	7, 8	eqtri 2493	. . . . . . 7
10	4, 9	syl6req 2522	. . . . . 6
11	10	a1d 25	. . . . 5 $/\$ $/\$
12		reldom 7593	. . . . . . . . . . 11
13	12	brrelexi 4880	. . . . . . . . . 10
14		0sdomg 7719	. . . . . . . . . 10
15	13, 14	syl 17	. . . . . . . . 9
16	15	biimparc 495	. . . . . . . 8 $/\$
17		fodomr 7741	. . . . . . . 8 $/\$
18	16, 17	sylancom 680	. . . . . . 7 $/\$
19		unissb 4221	. . . . . . . . . . . . 13
20	19	anbi1i 709	. . . . . . . . . . . 12 $/\$ $/\$
21		r19.26 2904	. . . . . . . . . . . 12 $/\$ $/\$
22	20, 21	bitr4i 260	. . . . . . . . . . 11 $/\$ $/\$
23		ovolctb2 22523	. . . . . . . . . . . . . 14 $/\$
24	23	ex 441	. . . . . . . . . . . . 13
25	24	imdistani 704	. . . . . . . . . . . 12 $/\$ $/\$
26	25	ralimi 2796	. . . . . . . . . . 11 $/\$ $/\$
27	22, 26	sylbi 200	. . . . . . . . . 10 $/\$ $/\$
28	27	ancoms 460	. . . . . . . . 9 $/\$ $/\$
29		foima 5811	. . . . . . . . . . . 12
30	29	raleqdv 2979	. . . . . . . . . . 11 $/\$ $/\$
31		fofn 5808	. . . . . . . . . . . 12
32		ssid 3437	. . . . . . . . . . . 12
33		sseq1 3439	. . . . . . . . . . . . . 14
34		fveq2 5879	. . . . . . . . . . . . . . 15
35	34	eqeq1d 2473	. . . . . . . . . . . . . 14
36	33, 35	anbi12d 725	. . . . . . . . . . . . 13 $/\$ $/\$
37	36	ralima 6163	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
38	31, 32, 37	sylancl 675	. . . . . . . . . . 11 $/\$ $/\$
39	30, 38	bitr3d 263	. . . . . . . . . 10 $/\$ $/\$
40		difss 3549	. . . . . . . . . . . . . . . . . 18 $\$ ..^
41		ovolssnul 22518	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $/\$ $/\$ $\$ ..^
42	40, 41	mp3an1 1377	. . . . . . . . . . . . . . . . 17 $/\$ $\$ ..^
43		ssdifss 3553	. . . . . . . . . . . . . . . . . 18 $\$ ..^
44		nulmbl 22567	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
45		mblvol 22562	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ ..^ $\$ ..^ $\$ ..^
46	45	eqeq1d 2473	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ ..^ $\$ ..^ $\$ ..^
47	46	biimpar 493	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
48		0re 9661	. . . . . . . . . . . . . . . . . . . . . . 23
49	47, 48	syl6eqel 2557	. . . . . . . . . . . . . . . . . . . . . 22 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
50	49	expcom 442	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^ $\$ ..^
51	50	ancld 562	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
52	51	adantl 473	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
53	44, 52	mpd 15	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
54	43, 53	sylan 479	. . . . . . . . . . . . . . . . 17 $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
55	42, 54	syldan 478	. . . . . . . . . . . . . . . 16 $/\$ $\$ ..^ $/\$ $\$ ..^
56	55	ralimi 2796	. . . . . . . . . . . . . . 15 $/\$ $\$ ..^ $/\$ $\$ ..^
57		fveq2 5879	. . . . . . . . . . . . . . . . . . . . 21
58		oveq2 6316	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
59	58	iuneq1d 4294	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
60	57, 59	difeq12d 3541	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
61		eqid 2471	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
62		fvex 5889	. . . . . . . . . . . . . . . . . . . . 21
63		difexg 4545	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^
64	62, 63	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^
65	60, 61, 64	fvmpt 5963	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
66	65	eleq1d 2533	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
67	65	fveq2d 5883	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
68	67	eleq1d 2533	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
69	66, 68	anbi12d 725	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
70	69	ralbiia 2822	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
71		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20
72		oveq2 6316	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
73	72	iuneq1d 4294	. . . . . . . . . . . . . . . . . . . 20 ..^ ..^
74	71, 73	difeq12d 3541	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
75	74	eleq1d 2533	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
76	74	fveq2d 5883	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
77	76	eleq1d 2533	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
78	75, 77	anbi12d 725	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
79	78	cbvralv 3005	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
80	70, 79	bitri 257	. . . . . . . . . . . . . . 15 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
81	56, 80	sylibr 217	. . . . . . . . . . . . . 14 $/\$ $\$ ..^ $/\$ $\$ ..^
82		fveq2 5879	. . . . . . . . . . . . . . . 16
83	82	iundisj2 22581	. . . . . . . . . . . . . . 15 Disj $\$ ..^
84		disjeq2 4370	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^ Disj $\$ ..^ Disj $\$ ..^
85	84, 65	mprg 2770	. . . . . . . . . . . . . . 15 Disj $\$ ..^ Disj $\$ ..^
86	83, 85	mpbir 214	. . . . . . . . . . . . . 14 Disj $\$ ..^
87		nnex 10637	. . . . . . . . . . . . . . . . 17
88	87	mptex 6152	. . . . . . . . . . . . . . . 16 $\$ ..^
89		fveq1 5878	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
90	89	eleq1d 2533	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
91	89	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
92	91	eleq1d 2533	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
93	90, 92	anbi12d 725	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^ $/\$ $\$ ..^
94	93	ralbidv 2829	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $/\$ $\$ ..^ $/\$ $\$ ..^
95	89	adantr 472	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^
96	95	disjeq2dv 4371	. . . . . . . . . . . . . . . . . 18 $\$ ..^ Disj Disj $\$ ..^
97	94, 96	anbi12d 725	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $/\$ Disj $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^
98	89	iuneq2d 4296	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
99	98	fveq2d 5883	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
100		voliunnfl.1	. . . . . . . . . . . . . . . . . . . . . 22
101		voliunnfl.2	. . . . . . . . . . . . . . . . . . . . . . 23
102		seqeq3 12256	. . . . . . . . . . . . . . . . . . . . . . 23
103	101, 102	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
104	100, 103	eqtri 2493	. . . . . . . . . . . . . . . . . . . . 21
105	104	rneqi 5067	. . . . . . . . . . . . . . . . . . . 20
106	105	supeq1i 7979	. . . . . . . . . . . . . . . . . . 19
107	91	mpteq2dv 4483	. . . . . . . . . . . . . . . . . . . . . 22 $\$ ..^ $\$ ..^
108	107	seqeq3d 12259	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
109	108	rneqd 5068	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
110	109	supeq1d 7978	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
111	106, 110	syl5eq 2517	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
112	99, 111	eqeq12d 2486	. . . . . . . . . . . . . . . . 17 $\$ ..^ $\$ ..^ $\$ ..^
113	97, 112	imbi12d 327	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $/\$ Disj $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
114		voliunnfl.3	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Disj
115	88, 113, 114	vtocl 3086	. . . . . . . . . . . . . . 15 $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
116	65	iuneq2i 4288	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^
117	116	fveq2i 5882	. . . . . . . . . . . . . . 15 $\$ ..^ $\$ ..^
118	67	mpteq2ia 4478	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
119		seqeq3 12256	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^ $\$ ..^ $\$ ..^
120	118, 119	ax-mp 5	. . . . . . . . . . . . . . . . 17 $\$ ..^ $\$ ..^
121	120	rneqi 5067	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^
122	121	supeq1i 7979	. . . . . . . . . . . . . . 15 $\$ ..^ $\$ ..^
123	115, 117, 122	3eqtr3g 2528	. . . . . . . . . . . . . 14 $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
124	81, 86, 123	sylancl 675	. . . . . . . . . . . . 13 $/\$ $\$ ..^ $\$ ..^
125	124	adantl 473	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^ $\$ ..^
126	82	iundisj 22580	. . . . . . . . . . . . . . . 16 $\$ ..^
127		fofun 5807	. . . . . . . . . . . . . . . . 17
128		funiunfv 6171	. . . . . . . . . . . . . . . . 17
129	127, 128	syl 17	. . . . . . . . . . . . . . . 16
130	126, 129	syl5eqr 2519	. . . . . . . . . . . . . . 15 $\$ ..^
131	29	unieqd 4200	. . . . . . . . . . . . . . 15
132	130, 131	eqtrd 2505	. . . . . . . . . . . . . 14 $\$ ..^
133	132	fveq2d 5883	. . . . . . . . . . . . 13 $\$ ..^
134	133	adantr 472	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^
135	57	sseq1d 3445	. . . . . . . . . . . . . . . . . . . . 21
136	57	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . 22
137	136	eqeq1d 2473	. . . . . . . . . . . . . . . . . . . . 21
138	135, 137	anbi12d 725	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
139	138	rspccva 3135	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
140		ssdifss 3553	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^
141	140	adantr 472	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ ..^
142		difss 3549	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^
143		ovolssnul 22518	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^ $/\$ $/\$ $\$ ..^
144	142, 143	mp3an1 1377	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ ..^
145	141, 144	jca 541	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ ..^ $/\$ $\$ ..^
146		nulmbl 22567	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
147		mblvol 22562	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^ $\$ ..^
148	145, 146, 147	3syl 18	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ ..^ $\$ ..^
149	148, 144	eqtrd 2505	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ ..^
150	139, 149	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ ..^
151	150	mpteq2dva 4482	. . . . . . . . . . . . . . . . 17 $/\$ $\$ ..^
152	151	seqeq3d 12259	. . . . . . . . . . . . . . . 16 $/\$ $\$ ..^
153	152	rneqd 5068	. . . . . . . . . . . . . . 15 $/\$ $\$ ..^
154	153	supeq1d 7978	. . . . . . . . . . . . . 14 $/\$ $\$ ..^
155		0cn 9653	. . . . . . . . . . . . . . . . . . . . . 22
156		ser1const 12307	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
157	155, 156	mpan 684	. . . . . . . . . . . . . . . . . . . . 21
158		nncn 10639	. . . . . . . . . . . . . . . . . . . . . 22
159	158	mul01d 9850	. . . . . . . . . . . . . . . . . . . . 21
160	157, 159	eqtrd 2505	. . . . . . . . . . . . . . . . . . . 20
161	160	mpteq2ia 4478	. . . . . . . . . . . . . . . . . . 19
162		fconstmpt 4883	. . . . . . . . . . . . . . . . . . . . 21
163		seqeq3 12256	. . . . . . . . . . . . . . . . . . . . 21
164	162, 163	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
165		1z 10991	. . . . . . . . . . . . . . . . . . . . . 22
166		seqfn 12263	. . . . . . . . . . . . . . . . . . . . . 22
167	165, 166	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
168		nnuz 11218	. . . . . . . . . . . . . . . . . . . . . . 23
169	168	fneq2i 5681	. . . . . . . . . . . . . . . . . . . . . 22
170		dffn5 5924	. . . . . . . . . . . . . . . . . . . . . 22
171	169, 170	bitr3i 259	. . . . . . . . . . . . . . . . . . . . 21
172	167, 171	mpbi 213	. . . . . . . . . . . . . . . . . . . 20
173	164, 172	eqtr3i 2495	. . . . . . . . . . . . . . . . . . 19
174		fconstmpt 4883	. . . . . . . . . . . . . . . . . . 19
175	161, 173, 174	3eqtr4i 2503	. . . . . . . . . . . . . . . . . 18
176	175	rneqi 5067	. . . . . . . . . . . . . . . . 17
177		1nn 10642	. . . . . . . . . . . . . . . . . 18
178		ne0i 3728	. . . . . . . . . . . . . . . . . 18
179		rnxp 5273	. . . . . . . . . . . . . . . . . 18
180	177, 178, 179	mp2b 10	. . . . . . . . . . . . . . . . 17
181	176, 180	eqtri 2493	. . . . . . . . . . . . . . . 16
182	181	supeq1i 7979	. . . . . . . . . . . . . . 15
183		xrltso 11463	. . . . . . . . . . . . . . . 16
184		0xr 9705	. . . . . . . . . . . . . . . 16
185		supsn 8006	. . . . . . . . . . . . . . . 16 $/\$
186	183, 184, 185	mp2an 686	. . . . . . . . . . . . . . 15
187	182, 186	eqtri 2493	. . . . . . . . . . . . . 14
188	154, 187	syl6eq 2521	. . . . . . . . . . . . 13 $/\$ $\$ ..^
189	188	adantl 473	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^
190	125, 134, 189	3eqtr3rd 2514	. . . . . . . . . . 11 $/\$ $/\$
191	190	ex 441	. . . . . . . . . 10 $/\$
192	39, 191	sylbid 223	. . . . . . . . 9 $/\$
193	28, 192	syl5 32	. . . . . . . 8 $/\$
194	193	exlimiv 1784	. . . . . . 7 $/\$
195	18, 194	syl 17	. . . . . 6 $/\$ $/\$
196	195	expimpd 614	. . . . 5 $/\$ $/\$
197	11, 196	pm2.61ine 2726	. . . 4 $/\$ $/\$
198		renepnf 9706	. . . . . . 7
199	48, 198	mp1i 13	. . . . . 6
200		fveq2 5879	. . . . . . 7
201		rembl 22572	. . . . . . . . 9
202		mblvol 22562	. . . . . . . . 9
203	201, 202	ax-mp 5	. . . . . . . 8
204		ovolre 22557	. . . . . . . 8
205	203, 204	eqtri 2493	. . . . . . 7
206	200, 205	syl6eq 2521	. . . . . 6
207	199, 206	neeqtrrd 2717	. . . . 5
208	207	necon2i 2677	. . . 4
209	197, 208	syl 17	. . 3 $/\$ $/\$
210	209	expr 626	. 2 $/\$
211		eqimss 3470	. . 3
212	211	necon3bi 2669	. 2
213	210, 212	pm2.61d1 164	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $/\$ wa 376

wceq 1452

wex 1671

wcel 1904

wne 2641

wral 2756

cvv 3031 $\$ cdif 3387

wss 3390

c0 3722

csn 3959

cuni 4190

ciun 4269 Disj wdisj 4366 class class class wbr 4395

cmpt 4454

wor 4759

cxp 4837

cdm 4839

crn 4840

cima 4842

wfun 5583

wfn 5584

wfo 5587

cfv 5589 (class class class)co 6308

cdom 7585

csdm 7586

csup 7972

cc 9555

cr 9556

cc0 9557

c1 9558

caddc 9560

cmul 9562

cpnf 9690

cxr 9692

clt 9693

cn 10631

cz 10961

cuz 11182 ..^cfzo 11942

cseq 12251

covol 22491

cvol 22493

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-disj 4367 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-of 6550 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-er 7381 df-map 7492 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-fi 7943 df-sup 7974 df-inf 7975 df-oi 8043 df-card 8391 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-n0 10894 df-z 10962 df-uz 11183 df-q 11288 df-rp 11326 df-xneg 11432 df-xadd 11433 df-xmul 11434 df-ioo 11664 df-ico 11666 df-icc 11667 df-fz 11811 df-fzo 11943 df-fl 12061 df-seq 12252 df-exp 12311 df-hash 12554 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-clim 13629 df-sum 13830 df-rest 15399 df-topgen 15420 df-psmet 19039 df-xmet 19040 df-met 19041 df-bl 19042 df-mopn 19043 df-top 19998 df-bases 19999 df-topon 20000 df-cmp 20479 df-ovol 22494 df-vol 22496

This theorem is referenced by: (None)

W3C validator