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 30223

Description: voliun 22049 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 4171	. . . . . . . . 9
2		uni0 4190	. . . . . . . . 9
3	1, 2	syl6eq 2439	. . . . . . . 8
4	3	fveq2d 5778	. . . . . . 7
5		0mbl 22035	. . . . . . . . 9
6		mblvol 22026	. . . . . . . . 9
7	5, 6	ax-mp 5	. . . . . . . 8
8		ovol0 21989	. . . . . . . 8
9	7, 8	eqtri 2411	. . . . . . 7
10	4, 9	syl6req 2440	. . . . . 6
11	10	a1d 25	. . . . 5 $/\$ $/\$
12		reldom 7441	. . . . . . . . . . 11
13	12	brrelexi 4954	. . . . . . . . . 10
14		0sdomg 7565	. . . . . . . . . 10
15	13, 14	syl 16	. . . . . . . . 9
16	15	biimparc 485	. . . . . . . 8 $/\$
17		fodomr 7587	. . . . . . . 8 $/\$
18	16, 17	sylancom 665	. . . . . . 7 $/\$
19		unissb 4194	. . . . . . . . . . . . 13
20	19	anbi1i 693	. . . . . . . . . . . 12 $/\$ $/\$
21		r19.26 2909	. . . . . . . . . . . 12 $/\$ $/\$
22	20, 21	bitr4i 252	. . . . . . . . . . 11 $/\$ $/\$
23		ovolctb2 21988	. . . . . . . . . . . . . 14 $/\$
24	23	ex 432	. . . . . . . . . . . . 13
25	24	imdistani 688	. . . . . . . . . . . 12 $/\$ $/\$
26	25	ralimi 2775	. . . . . . . . . . 11 $/\$ $/\$
27	22, 26	sylbi 195	. . . . . . . . . 10 $/\$ $/\$
28	27	ancoms 451	. . . . . . . . 9 $/\$ $/\$
29		foima 5708	. . . . . . . . . . . 12
30	29	raleqdv 2985	. . . . . . . . . . 11 $/\$ $/\$
31		fofn 5705	. . . . . . . . . . . 12
32		ssid 3436	. . . . . . . . . . . 12
33		sseq1 3438	. . . . . . . . . . . . . 14
34		fveq2 5774	. . . . . . . . . . . . . . 15
35	34	eqeq1d 2384	. . . . . . . . . . . . . 14
36	33, 35	anbi12d 708	. . . . . . . . . . . . 13 $/\$ $/\$
37	36	ralima 6053	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
38	31, 32, 37	sylancl 660	. . . . . . . . . . 11 $/\$ $/\$
39	30, 38	bitr3d 255	. . . . . . . . . 10 $/\$ $/\$
40		difss 3545	. . . . . . . . . . . . . . . . . 18 $\$ ..^
41		ovolssnul 21983	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $/\$ $/\$ $\$ ..^
42	40, 41	mp3an1 1309	. . . . . . . . . . . . . . . . 17 $/\$ $\$ ..^
43		ssdifss 3549	. . . . . . . . . . . . . . . . . 18 $\$ ..^
44		nulmbl 22031	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
45		mblvol 22026	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ ..^ $\$ ..^ $\$ ..^
46	45	eqeq1d 2384	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ ..^ $\$ ..^ $\$ ..^
47	46	biimpar 483	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
48		0re 9507	. . . . . . . . . . . . . . . . . . . . . . 23
49	47, 48	syl6eqel 2478	. . . . . . . . . . . . . . . . . . . . . 22 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
50	49	expcom 433	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^ $\$ ..^
51	50	ancld 551	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
52	51	adantl 464	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
53	44, 52	mpd 15	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
54	43, 53	sylan 469	. . . . . . . . . . . . . . . . 17 $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
55	42, 54	syldan 468	. . . . . . . . . . . . . . . 16 $/\$ $\$ ..^ $/\$ $\$ ..^
56	55	ralimi 2775	. . . . . . . . . . . . . . 15 $/\$ $\$ ..^ $/\$ $\$ ..^
57		fveq2 5774	. . . . . . . . . . . . . . . . . . . . 21
58		oveq2 6204	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
59	58	iuneq1d 4268	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
60	57, 59	difeq12d 3537	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
61		eqid 2382	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
62		fvex 5784	. . . . . . . . . . . . . . . . . . . . 21
63		difexg 4513	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^
64	62, 63	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^
65	60, 61, 64	fvmpt 5857	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
66	65	eleq1d 2451	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
67	65	fveq2d 5778	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
68	67	eleq1d 2451	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
69	66, 68	anbi12d 708	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
70	69	ralbiia 2812	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
71		fveq2 5774	. . . . . . . . . . . . . . . . . . . 20
72		oveq2 6204	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
73	72	iuneq1d 4268	. . . . . . . . . . . . . . . . . . . 20 ..^ ..^
74	71, 73	difeq12d 3537	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
75	74	eleq1d 2451	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
76	74	fveq2d 5778	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
77	76	eleq1d 2451	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
78	75, 77	anbi12d 708	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
79	78	cbvralv 3009	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
80	70, 79	bitri 249	. . . . . . . . . . . . . . 15 $\$ ..^ $/\$ $\$ ..^ $\$ ..^ $/\$ $\$ ..^
81	56, 80	sylibr 212	. . . . . . . . . . . . . 14 $/\$ $\$ ..^ $/\$ $\$ ..^
82		fveq2 5774	. . . . . . . . . . . . . . . 16
83	82	iundisj2 22044	. . . . . . . . . . . . . . 15 Disj $\$ ..^
84		disjeq2 4342	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^ Disj $\$ ..^ Disj $\$ ..^
85	84, 65	mprg 2745	. . . . . . . . . . . . . . 15 Disj $\$ ..^ Disj $\$ ..^
86	83, 85	mpbir 209	. . . . . . . . . . . . . 14 Disj $\$ ..^
87		nnex 10458	. . . . . . . . . . . . . . . . 17
88	87	mptex 6044	. . . . . . . . . . . . . . . 16 $\$ ..^
89		fveq1 5773	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
90	89	eleq1d 2451	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
91	89	fveq2d 5778	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
92	91	eleq1d 2451	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
93	90, 92	anbi12d 708	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^ $/\$ $\$ ..^
94	93	ralbidv 2821	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $/\$ $\$ ..^ $/\$ $\$ ..^
95	89	adantr 463	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $/\$ $\$ ..^
96	95	disjeq2dv 4343	. . . . . . . . . . . . . . . . . 18 $\$ ..^ Disj Disj $\$ ..^
97	94, 96	anbi12d 708	. . . . . . . . . . . . . . . . 17 $\$ ..^ $/\$ $/\$ Disj $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^
98	89	iuneq2d 4270	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
99	98	fveq2d 5778	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
100		voliunnfl.1	. . . . . . . . . . . . . . . . . . . . . 22
101		voliunnfl.2	. . . . . . . . . . . . . . . . . . . . . . 23
102		seqeq3 12015	. . . . . . . . . . . . . . . . . . . . . . 23
103	101, 102	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
104	100, 103	eqtri 2411	. . . . . . . . . . . . . . . . . . . . 21
105	104	rneqi 5142	. . . . . . . . . . . . . . . . . . . 20
106	105	supeq1i 7821	. . . . . . . . . . . . . . . . . . 19
107	91	mpteq2dv 4454	. . . . . . . . . . . . . . . . . . . . . 22 $\$ ..^ $\$ ..^
108	107	seqeq3d 12018	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^
109	108	rneqd 5143	. . . . . . . . . . . . . . . . . . . 20 $\$ ..^ $\$ ..^
110	109	supeq1d 7820	. . . . . . . . . . . . . . . . . . 19 $\$ ..^ $\$ ..^
111	106, 110	syl5eq 2435	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
112	99, 111	eqeq12d 2404	. . . . . . . . . . . . . . . . 17 $\$ ..^ $\$ ..^ $\$ ..^
113	97, 112	imbi12d 318	. . . . . . . . . . . . . . . 16 $\$ ..^ $/\$ $/\$ Disj $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
114		voliunnfl.3	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Disj
115	88, 113, 114	vtocl 3086	. . . . . . . . . . . . . . 15 $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
116	65	iuneq2i 4262	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^
117	116	fveq2i 5777	. . . . . . . . . . . . . . 15 $\$ ..^ $\$ ..^
118	67	mpteq2ia 4449	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^
119		seqeq3 12015	. . . . . . . . . . . . . . . . . 18 $\$ ..^ $\$ ..^ $\$ ..^ $\$ ..^
120	118, 119	ax-mp 5	. . . . . . . . . . . . . . . . 17 $\$ ..^ $\$ ..^
121	120	rneqi 5142	. . . . . . . . . . . . . . . 16 $\$ ..^ $\$ ..^
122	121	supeq1i 7821	. . . . . . . . . . . . . . 15 $\$ ..^ $\$ ..^
123	115, 117, 122	3eqtr3g 2446	. . . . . . . . . . . . . 14 $\$ ..^ $/\$ $\$ ..^ $/\$ Disj $\$ ..^ $\$ ..^ $\$ ..^
124	81, 86, 123	sylancl 660	. . . . . . . . . . . . 13 $/\$ $\$ ..^ $\$ ..^
125	124	adantl 464	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^ $\$ ..^
126	82	iundisj 22043	. . . . . . . . . . . . . . . 16 $\$ ..^
127		fofun 5704	. . . . . . . . . . . . . . . . 17
128		funiunfv 6061	. . . . . . . . . . . . . . . . 17
129	127, 128	syl 16	. . . . . . . . . . . . . . . 16
130	126, 129	syl5eqr 2437	. . . . . . . . . . . . . . 15 $\$ ..^
131	29	unieqd 4173	. . . . . . . . . . . . . . 15
132	130, 131	eqtrd 2423	. . . . . . . . . . . . . 14 $\$ ..^
133	132	fveq2d 5778	. . . . . . . . . . . . 13 $\$ ..^
134	133	adantr 463	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^
135	57	sseq1d 3444	. . . . . . . . . . . . . . . . . . . . 21
136	57	fveq2d 5778	. . . . . . . . . . . . . . . . . . . . . 22
137	136	eqeq1d 2384	. . . . . . . . . . . . . . . . . . . . 21
138	135, 137	anbi12d 708	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
139	138	rspccva 3134	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
140		ssdifss 3549	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^
141	140	adantr 463	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ ..^
142		difss 3545	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^
143		ovolssnul 21983	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ ..^ $/\$ $/\$ $\$ ..^
144	142, 143	mp3an1 1309	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ ..^
145	141, 144	jca 530	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ ..^ $/\$ $\$ ..^
146		nulmbl 22031	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $/\$ $\$ ..^ $\$ ..^
147		mblvol 22026	. . . . . . . . . . . . . . . . . . . . 21 $\$ ..^ $\$ ..^ $\$ ..^
148	145, 146, 147	3syl 20	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ ..^ $\$ ..^
149	148, 144	eqtrd 2423	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ ..^
150	139, 149	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ ..^
151	150	mpteq2dva 4453	. . . . . . . . . . . . . . . . 17 $/\$ $\$ ..^
152	151	seqeq3d 12018	. . . . . . . . . . . . . . . 16 $/\$ $\$ ..^
153	152	rneqd 5143	. . . . . . . . . . . . . . 15 $/\$ $\$ ..^
154	153	supeq1d 7820	. . . . . . . . . . . . . 14 $/\$ $\$ ..^
155		0cn 9499	. . . . . . . . . . . . . . . . . . . . . 22
156		ser1const 12066	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
157	155, 156	mpan 668	. . . . . . . . . . . . . . . . . . . . 21
158		nncn 10460	. . . . . . . . . . . . . . . . . . . . . 22
159	158	mul01d 9690	. . . . . . . . . . . . . . . . . . . . 21
160	157, 159	eqtrd 2423	. . . . . . . . . . . . . . . . . . . 20
161	160	mpteq2ia 4449	. . . . . . . . . . . . . . . . . . 19
162		fconstmpt 4957	. . . . . . . . . . . . . . . . . . . . 21
163		seqeq3 12015	. . . . . . . . . . . . . . . . . . . . 21
164	162, 163	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
165		1z 10811	. . . . . . . . . . . . . . . . . . . . . 22
166		seqfn 12022	. . . . . . . . . . . . . . . . . . . . . 22
167	165, 166	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
168		nnuz 11036	. . . . . . . . . . . . . . . . . . . . . . 23
169	168	fneq2i 5584	. . . . . . . . . . . . . . . . . . . . . 22
170		dffn5 5819	. . . . . . . . . . . . . . . . . . . . . 22
171	169, 170	bitr3i 251	. . . . . . . . . . . . . . . . . . . . 21
172	167, 171	mpbi 208	. . . . . . . . . . . . . . . . . . . 20
173	164, 172	eqtr3i 2413	. . . . . . . . . . . . . . . . . . 19
174		fconstmpt 4957	. . . . . . . . . . . . . . . . . . 19
175	161, 173, 174	3eqtr4i 2421	. . . . . . . . . . . . . . . . . 18
176	175	rneqi 5142	. . . . . . . . . . . . . . . . 17
177		1nn 10463	. . . . . . . . . . . . . . . . . 18
178		ne0i 3717	. . . . . . . . . . . . . . . . . 18
179		rnxp 5347	. . . . . . . . . . . . . . . . . 18
180	177, 178, 179	mp2b 10	. . . . . . . . . . . . . . . . 17
181	176, 180	eqtri 2411	. . . . . . . . . . . . . . . 16
182	181	supeq1i 7821	. . . . . . . . . . . . . . 15
183		xrltso 11268	. . . . . . . . . . . . . . . 16
184		0xr 9551	. . . . . . . . . . . . . . . 16
185		supsn 7845	. . . . . . . . . . . . . . . 16 $/\$
186	183, 184, 185	mp2an 670	. . . . . . . . . . . . . . 15
187	182, 186	eqtri 2411	. . . . . . . . . . . . . 14
188	154, 187	syl6eq 2439	. . . . . . . . . . . . 13 $/\$ $\$ ..^
189	188	adantl 464	. . . . . . . . . . . 12 $/\$ $/\$ $\$ ..^
190	125, 134, 189	3eqtr3rd 2432	. . . . . . . . . . 11 $/\$ $/\$
191	190	ex 432	. . . . . . . . . 10 $/\$
192	39, 191	sylbid 215	. . . . . . . . 9 $/\$
193	28, 192	syl5 32	. . . . . . . 8 $/\$
194	193	exlimiv 1730	. . . . . . 7 $/\$
195	18, 194	syl 16	. . . . . 6 $/\$ $/\$
196	195	expimpd 601	. . . . 5 $/\$ $/\$
197	11, 196	pm2.61ine 2695	. . . 4 $/\$ $/\$
198		renepnf 9552	. . . . . . 7
199	48, 198	mp1i 12	. . . . . 6
200		fveq2 5774	. . . . . . 7
201		rembl 22036	. . . . . . . . 9
202		mblvol 22026	. . . . . . . . 9
203	201, 202	ax-mp 5	. . . . . . . 8
204		ovolre 22021	. . . . . . . 8
205	203, 204	eqtri 2411	. . . . . . 7
206	200, 205	syl6eq 2439	. . . . . 6
207	199, 206	neeqtrrd 2682	. . . . 5
208	207	necon2i 2625	. . . 4
209	197, 208	syl 16	. . 3 $/\$ $/\$
210	209	expr 613	. 2 $/\$
211		eqimss 3469	. . 3
212	211	necon3bi 2611	. 2
213	210, 212	pm2.61d1 159	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 367

wceq 1399

wex 1620

wcel 1826

wne 2577

wral 2732

cvv 3034 $\$ cdif 3386

wss 3389

c0 3711

csn 3944

cuni 4163

ciun 4243 Disj wdisj 4338 class class class wbr 4367

cmpt 4425

wor 4713

cxp 4911

cdm 4913

crn 4914

cima 4916

wfun 5490

wfn 5491

wfo 5494

cfv 5496 (class class class)co 6196

cdom 7433

csdm 7434

csup 7815

cc 9401

cr 9402

cc0 9403

c1 9404

caddc 9406

cmul 9408

cpnf 9536

cxr 9538

clt 9539

cn 10452

cz 10781

cuz 11001 ..^cfzo 11717

cseq 12010

covol 21959

cvol 21960

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-rep 4478 ax-sep 4488 ax-nul 4496 ax-pow 4543 ax-pr 4601 ax-un 6491 ax-inf2 7972 ax-cnex 9459 ax-resscn 9460 ax-1cn 9461 ax-icn 9462 ax-addcl 9463 ax-addrcl 9464 ax-mulcl 9465 ax-mulrcl 9466 ax-mulcom 9467 ax-addass 9468 ax-mulass 9469 ax-distr 9470 ax-i2m1 9471 ax-1ne0 9472 ax-1rid 9473 ax-rnegex 9474 ax-rrecex 9475 ax-cnre 9476 ax-pre-lttri 9477 ax-pre-lttrn 9478 ax-pre-ltadd 9479 ax-pre-mulgt0 9480 ax-pre-sup 9481

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1402 df-fal 1405 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-nel 2580 df-ral 2737 df-rex 2738 df-reu 2739 df-rmo 2740 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-pss 3405 df-nul 3712 df-if 3858 df-pw 3929 df-sn 3945 df-pr 3947 df-tp 3949 df-op 3951 df-uni 4164 df-int 4200 df-iun 4245 df-disj 4339 df-br 4368 df-opab 4426 df-mpt 4427 df-tr 4461 df-eprel 4705 df-id 4709 df-po 4714 df-so 4715 df-fr 4752 df-se 4753 df-we 4754 df-ord 4795 df-on 4796 df-lim 4797 df-suc 4798 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-f1 5501 df-fo 5502 df-f1o 5503 df-fv 5504 df-isom 5505 df-riota 6158 df-ov 6199 df-oprab 6200 df-mpt2 6201 df-of 6439 df-om 6600 df-1st 6699 df-2nd 6700 df-recs 6960 df-rdg 6994 df-1o 7048 df-2o 7049 df-oadd 7052 df-er 7229 df-map 7340 df-en 7436 df-dom 7437 df-sdom 7438 df-fin 7439 df-fi 7786 df-sup 7816 df-oi 7850 df-card 8233 df-cda 8461 df-pnf 9541 df-mnf 9542 df-xr 9543 df-ltxr 9544 df-le 9545 df-sub 9720 df-neg 9721 df-div 10124 df-nn 10453 df-2 10511 df-3 10512 df-n0 10713 df-z 10782 df-uz 11002 df-q 11102 df-rp 11140 df-xneg 11239 df-xadd 11240 df-xmul 11241 df-ioo 11454 df-ico 11456 df-icc 11457 df-fz 11594 df-fzo 11718 df-fl 11828 df-seq 12011 df-exp 12070 df-hash 12308 df-cj 12934 df-re 12935 df-im 12936 df-sqrt 13070 df-abs 13071 df-clim 13313 df-sum 13511 df-rest 14830 df-topgen 14851 df-psmet 18524 df-xmet 18525 df-met 18526 df-bl 18527 df-mopn 18528 df-top 19484 df-bases 19486 df-topon 19487 df-cmp 19973 df-ovol 21961 df-vol 21962

This theorem is referenced by: (None)

W3C validator