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 28378

Description: voliun 21004 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 4092	. . . . . . . . 9
2		uni0 4111	. . . . . . . . 9
3	1, 2	syl6eq 2485	. . . . . . . 8
4	3	fveq2d 5688	. . . . . . 7
5		0mbl 20990	. . . . . . . . 9
6		mblvol 20982	. . . . . . . . 9
7	5, 6	ax-mp 5	. . . . . . . 8
8		ovol0 20945	. . . . . . . 8
9	7, 8	eqtri 2457	. . . . . . 7
10	4, 9	syl6req 2486	. . . . . 6
11	10	a1d 25	. . . . 5 $/\$ $/\$
12		reldom 7308	. . . . . . . . . . 11
13	12	brrelexi 4871	. . . . . . . . . 10
14		0sdomg 7432	. . . . . . . . . 10
15	13, 14	syl 16	. . . . . . . . 9
16	15	biimparc 487	. . . . . . . 8 $/\$
17		fodomr 7454	. . . . . . . 8 $/\$
18	16, 17	sylancom 667	. . . . . . 7 $/\$
19		unissb 4116	. . . . . . . . . . . . 13
20	19	anbi1i 695	. . . . . . . . . . . 12 $/\$ $/\$
21		r19.26 2843	. . . . . . . . . . . 12 $/\$ $/\$
22	20, 21	bitr4i 252	. . . . . . . . . . 11 $/\$ $/\$
23		ovolctb2 20944	. . . . . . . . . . . . . 14 $/\$
24	23	ex 434	. . . . . . . . . . . . 13
25	24	imdistani 690	. . . . . . . . . . . 12 $/\$ $/\$
26	25	ralimi 2785	. . . . . . . . . . 11 $/\$ $/\$
27	22, 26	sylbi 195	. . . . . . . . . 10 $/\$ $/\$
28	27	ancoms 453	. . . . . . . . 9 $/\$ $/\$
29		foima 5618	. . . . . . . . . . . 12
30	29	raleqdv 2917	. . . . . . . . . . 11 $/\$ $/\$
31		fofn 5615	. . . . . . . . . . . 12
32		ssid 3368	. . . . . . . . . . . 12
33		sseq1 3370	. . . . . . . . . . . . . 14
34		fveq2 5684	. . . . . . . . . . . . . . 15
35	34	eqeq1d 2445	. . . . . . . . . . . . . 14
36	33, 35	anbi12d 710	. . . . . . . . . . . . 13 $/\$ $/\$
37	36	ralima 5950	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
38	31, 32, 37	sylancl 662	. . . . . . . . . . 11 $/\$ $/\$
39	30, 38	bitr3d 255	. . . . . . . . . 10 $/\$ $/\$
40		difss 3476	. . . . . . . . . . . . . . . . . 18 $\$ ..^
41		ovolssnul 20939	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $/\$ $/\$ $\$ ..^
42	40, 41	mp3an1 1301	. . . . . . . . . . . . . . . . 17 $/\$ $\$ ..^
43		ssdifss 3480	. . . . . . . . . . . . . . . . . 18 $\$ ..^
44		nulmbl 20986	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
45		mblvol 20982	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ ..^ $\$ ..^ $\$ ..^
46	45	eqeq1d 2445	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ ..^ $\$ ..^ $\$ ..^
47	46	biimpar 485	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
48		0re 9378	. . . . . . . . . . . . . . . . . . . . . . 23
49	47, 48	syl6eqel 2525	. . . . . . . . . . . . . . . . . . . . . 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 2785	. . . . . . . . . . . . . . 15 $/\$ $\$ ..^ $/\$ $\$ ..^
57		fveq2 5684	. . . . . . . . . . . . . . . . . . . . 21
58		oveq2 6094	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
59	58	iuneq1d 4188	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
60	57, 59	difeq12d 3468	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
61		eqid 2437	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
62		fvex 5694	. . . . . . . . . . . . . . . . . . . . 21
63		difexg 4433	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^
64	62, 63	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^
65	60, 61, 64	fvmpt 5767	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
66	65	eleq1d 2503	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
67	65	fveq2d 5688	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
68	67	eleq1d 2503	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
69	66, 68	anbi12d 710	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
70	69	ralbiia 2741	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
71		fveq2 5684	. . . . . . . . . . . . . . . . . . . 20
72		oveq2 6094	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
73	72	iuneq1d 4188	. . . . . . . . . . . . . . . . . . . 20 ..^ ..^
74	71, 73	difeq12d 3468	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
75	74	eleq1d 2503	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
76	74	fveq2d 5688	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
77	76	eleq1d 2503	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
78	75, 77	anbi12d 710	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
79	78	cbvralv 2941	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
80	70, 79	bitri 249	. . . . . . . . . . . . . . 15 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
81	56, 80	sylibr 212	. . . . . . . . . . . . . 14 $/\$ $\$ ..^ $/\$ $\$ ..^
82		fveq2 5684	. . . . . . . . . . . . . . . 16
83	82	iundisj2 20999	. . . . . . . . . . . . . . 15 Disj $\$ ..^
84		disjeq2 4259	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^ Disj $\$ ..^ Disj $\$ ..^
85	84, 65	mprg 2779	. . . . . . . . . . . . . . 15 Disj $\$ ..^ Disj $\$ ..^
86	83, 85	mpbir 209	. . . . . . . . . . . . . 14 Disj $\$ ..^
87		nnex 10320	. . . . . . . . . . . . . . . . 17
88	87	mptex 5941	. . . . . . . . . . . . . . . 16 $\$ ..^
89		fveq1 5683	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
90	89	eleq1d 2503	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
91	89	fveq2d 5688	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
92	91	eleq1d 2503	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
93	90, 92	anbi12d 710	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^ $/\$ $\$ ..^
94	93	ralbidv 2729	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $/\$ $\$ ..^ $/\$ $\$ ..^
95	89	adantr 465	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^
96	95	disjeq2dv 4260	. . . . . . . . . . . . . . . . . 18 $\$ ..^ Disj Disj $\$ ..^
97	94, 96	anbi12d 710	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $/\$ Disj $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^
98	89	iuneq2d 4190	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
99	98	fveq2d 5688	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
100		voliunnfl.1	. . . . . . . . . . . . . . . . . . . . . 22
101		voliunnfl.2	. . . . . . . . . . . . . . . . . . . . . . 23
102		seqeq3 11803	. . . . . . . . . . . . . . . . . . . . . . 23
103	101, 102	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
104	100, 103	eqtri 2457	. . . . . . . . . . . . . . . . . . . . 21
105	104	rneqi 5058	. . . . . . . . . . . . . . . . . . . 20
106	105	supeq1i 7689	. . . . . . . . . . . . . . . . . . 19
107	91	mpteq2dv 4372	. . . . . . . . . . . . . . . . . . . . . 22 $\$ ..^ $\$ ..^
108	107	seqeq3d 11806	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
109	108	rneqd 5059	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
110	109	supeq1d 7688	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
111	106, 110	syl5eq 2481	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
112	99, 111	eqeq12d 2451	. . . . . . . . . . . . . . . . 17 $\$ ..^ $\$ ..^ $\$ ..^
113	97, 112	imbi12d 320	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $/\$ Disj $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
114		voliunnfl.3	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Disj
115	88, 113, 114	vtocl 3017	. . . . . . . . . . . . . . 15 $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
116	65	iuneq2i 4182	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^
117	116	fveq2i 5687	. . . . . . . . . . . . . . 15 $\$ ..^ $\$ ..^
118	67	mpteq2ia 4367	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
119		seqeq3 11803	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^ $\$ ..^ $\$ ..^
120	118, 119	ax-mp 5	. . . . . . . . . . . . . . . . 17 $\$ ..^ $\$ ..^
121	120	rneqi 5058	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^
122	121	supeq1i 7689	. . . . . . . . . . . . . . 15 $\$ ..^ $\$ ..^
123	115, 117, 122	3eqtr3g 2492	. . . . . . . . . . . . . 14 $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
124	81, 86, 123	sylancl 662	. . . . . . . . . . . . 13 $/\$ $\$ ..^ $\$ ..^
125	124	adantl 466	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^ $\$ ..^
126	82	iundisj 20998	. . . . . . . . . . . . . . . 16 $\$ ..^
127		fofun 5614	. . . . . . . . . . . . . . . . 17
128		funiunfv 5958	. . . . . . . . . . . . . . . . 17
129	127, 128	syl 16	. . . . . . . . . . . . . . . 16
130	126, 129	syl5eqr 2483	. . . . . . . . . . . . . . 15 $\$ ..^
131	29	unieqd 4094	. . . . . . . . . . . . . . 15
132	130, 131	eqtrd 2469	. . . . . . . . . . . . . 14 $\$ ..^
133	132	fveq2d 5688	. . . . . . . . . . . . 13 $\$ ..^
134	133	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^
135	57	sseq1d 3376	. . . . . . . . . . . . . . . . . . . . 21
136	57	fveq2d 5688	. . . . . . . . . . . . . . . . . . . . . 22
137	136	eqeq1d 2445	. . . . . . . . . . . . . . . . . . . . 21
138	135, 137	anbi12d 710	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
139	138	rspccva 3065	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
140		ssdifss 3480	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^
141	140	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ ..^
142		difss 3476	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^
143		ovolssnul 20939	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^ $/\$ $/\$ $\$ ..^
144	142, 143	mp3an1 1301	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ ..^
145	141, 144	jca 532	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ ..^ $/\$ $\$ ..^
146		nulmbl 20986	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
147		mblvol 20982	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^ $\$ ..^
148	145, 146, 147	3syl 20	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ ..^ $\$ ..^
149	148, 144	eqtrd 2469	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ ..^
150	139, 149	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ ..^
151	150	mpteq2dva 4371	. . . . . . . . . . . . . . . . 17 $/\$ $\$ ..^
152	151	seqeq3d 11806	. . . . . . . . . . . . . . . 16 $/\$ $\$ ..^
153	152	rneqd 5059	. . . . . . . . . . . . . . 15 $/\$ $\$ ..^
154	153	supeq1d 7688	. . . . . . . . . . . . . 14 $/\$ $\$ ..^
155		0cn 9370	. . . . . . . . . . . . . . . . . . . . . 22
156		ser1const 11854	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
157	155, 156	mpan 670	. . . . . . . . . . . . . . . . . . . . 21
158		nncn 10322	. . . . . . . . . . . . . . . . . . . . . 22
159	158	mul01d 9560	. . . . . . . . . . . . . . . . . . . . 21
160	157, 159	eqtrd 2469	. . . . . . . . . . . . . . . . . . . 20
161	160	mpteq2ia 4367	. . . . . . . . . . . . . . . . . . 19
162		fconstmpt 4874	. . . . . . . . . . . . . . . . . . . . 21
163		seqeq3 11803	. . . . . . . . . . . . . . . . . . . . 21
164	162, 163	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
165		1z 10668	. . . . . . . . . . . . . . . . . . . . . 22
166		seqfn 11810	. . . . . . . . . . . . . . . . . . . . . 22
167	165, 166	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
168		nnuz 10888	. . . . . . . . . . . . . . . . . . . . . . 23
169	168	fneq2i 5499	. . . . . . . . . . . . . . . . . . . . . 22
170		dffn5 5730	. . . . . . . . . . . . . . . . . . . . . 22
171	169, 170	bitr3i 251	. . . . . . . . . . . . . . . . . . . . 21
172	167, 171	mpbi 208	. . . . . . . . . . . . . . . . . . . 20
173	164, 172	eqtr3i 2459	. . . . . . . . . . . . . . . . . . 19
174		fconstmpt 4874	. . . . . . . . . . . . . . . . . . 19
175	161, 173, 174	3eqtr4i 2467	. . . . . . . . . . . . . . . . . 18
176	175	rneqi 5058	. . . . . . . . . . . . . . . . 17
177		1nn 10325	. . . . . . . . . . . . . . . . . 18
178		ne0i 3636	. . . . . . . . . . . . . . . . . 18
179		rnxp 5261	. . . . . . . . . . . . . . . . . 18
180	177, 178, 179	mp2b 10	. . . . . . . . . . . . . . . . 17
181	176, 180	eqtri 2457	. . . . . . . . . . . . . . . 16
182	181	supeq1i 7689	. . . . . . . . . . . . . . 15
183		xrltso 11110	. . . . . . . . . . . . . . . 16
184		0xr 9422	. . . . . . . . . . . . . . . 16
185		supsn 7711	. . . . . . . . . . . . . . . 16 $/\$
186	183, 184, 185	mp2an 672	. . . . . . . . . . . . . . 15
187	182, 186	eqtri 2457	. . . . . . . . . . . . . 14
188	154, 187	syl6eq 2485	. . . . . . . . . . . . 13 $/\$ $\$ ..^
189	188	adantl 466	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^
190	125, 134, 189	3eqtr3rd 2478	. . . . . . . . . . 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 2681	. . . 4 $/\$ $/\$
198		renepnf 9423	. . . . . . 7
199	48, 198	mp1i 12	. . . . . 6
200		fveq2 5684	. . . . . . 7
201		rembl 20991	. . . . . . . . 9
202		mblvol 20982	. . . . . . . . 9
203	201, 202	ax-mp 5	. . . . . . . 8
204		ovolre 20977	. . . . . . . 8
205	203, 204	eqtri 2457	. . . . . . 7
206	200, 205	syl6eq 2485	. . . . . 6
207	199, 206	neeqtrrd 2626	. . . . 5
208	207	necon2i 2652	. . . 4
209	197, 208	syl 16	. . 3 $/\$ $/\$
210	209	expr 615	. 2 $/\$
211		eqimss 3401	. . 3
212	211	necon3bi 2646	. 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 2600

wral 2709

cvv 2966 $\$ cdif 3318

wss 3321

c0 3630

csn 3870

cuni 4084

ciun 4164 Disj wdisj 4255 class class class wbr 4285

cmpt 4343

wor 4632

cxp 4830

cdm 4832

crn 4833

cima 4835

wfun 5405

wfn 5406

wfo 5409

cfv 5411 (class class class)co 6086

cdom 7300

csdm 7301

csup 7682

cc 9272

cr 9273

cc0 9274

c1 9275

caddc 9277

cmul 9279

cpnf 9407

cxr 9409

clt 9410

cn 10314

cz 10638

cuz 10853 ..^cfzo 11540

cseq 11798

covol 20915

cvol 20916

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 2418 ax-rep 4396 ax-sep 4406 ax-nul 4414 ax-pow 4463 ax-pr 4524 ax-un 6367 ax-inf2 7839 ax-cnex 9330 ax-resscn 9331 ax-1cn 9332 ax-icn 9333 ax-addcl 9334 ax-addrcl 9335 ax-mulcl 9336 ax-mulrcl 9337 ax-mulcom 9338 ax-addass 9339 ax-mulass 9340 ax-distr 9341 ax-i2m1 9342 ax-1ne0 9343 ax-1rid 9344 ax-rnegex 9345 ax-rrecex 9346 ax-cnre 9347 ax-pre-lttri 9348 ax-pre-lttrn 9349 ax-pre-ltadd 9350 ax-pre-mulgt0 9351 ax-pre-sup 9352

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 2256 df-mo 2257 df-clab 2424 df-cleq 2430 df-clel 2433 df-nfc 2562 df-ne 2602 df-nel 2603 df-ral 2714 df-rex 2715 df-reu 2716 df-rmo 2717 df-rab 2718 df-v 2968 df-sbc 3180 df-csb 3282 df-dif 3324 df-un 3326 df-in 3328 df-ss 3335 df-pss 3337 df-nul 3631 df-if 3785 df-pw 3855 df-sn 3871 df-pr 3873 df-tp 3875 df-op 3877 df-uni 4085 df-int 4122 df-iun 4166 df-disj 4256 df-br 4286 df-opab 4344 df-mpt 4345 df-tr 4379 df-eprel 4624 df-id 4628 df-po 4633 df-so 4634 df-fr 4671 df-se 4672 df-we 4673 df-ord 4714 df-on 4715 df-lim 4716 df-suc 4717 df-xp 4838 df-rel 4839 df-cnv 4840 df-co 4841 df-dm 4842 df-rn 4843 df-res 4844 df-ima 4845 df-iota 5374 df-fun 5413 df-fn 5414 df-f 5415 df-f1 5416 df-fo 5417 df-f1o 5418 df-fv 5419 df-isom 5420 df-riota 6045 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-of 6315 df-om 6472 df-1st 6572 df-2nd 6573 df-recs 6824 df-rdg 6858 df-1o 6912 df-2o 6913 df-oadd 6916 df-er 7093 df-map 7208 df-en 7303 df-dom 7304 df-sdom 7305 df-fin 7306 df-fi 7653 df-sup 7683 df-oi 7716 df-card 8101 df-cda 8329 df-pnf 9412 df-mnf 9413 df-xr 9414 df-ltxr 9415 df-le 9416 df-sub 9589 df-neg 9590 df-div 9986 df-nn 10315 df-2 10372 df-3 10373 df-n0 10572 df-z 10639 df-uz 10854 df-q 10946 df-rp 10984 df-xneg 11081 df-xadd 11082 df-xmul 11083 df-ioo 11296 df-ico 11298 df-icc 11299 df-fz 11430 df-fzo 11541 df-fl 11634 df-seq 11799 df-exp 11858 df-hash 12096 df-cj 12580 df-re 12581 df-im 12582 df-sqr 12716 df-abs 12717 df-clim 12958 df-sum 13156 df-rest 14353 df-topgen 14374 df-psmet 17778 df-xmet 17779 df-met 17780 df-bl 17781 df-mopn 17782 df-top 18472 df-bases 18474 df-topon 18475 df-cmp 18959 df-ovol 20917 df-vol 20918

This theorem is referenced by: (None)

W3C validator