cnambfre - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cnambfre		Structured version Unicode version

Theorem cnambfre 28445

Description: A real-valued, a.e. continuous function is measurable. (Contributed by Brendan Leahy, 4-Apr-2018.)

**Assertion**
Ref	Expression
cnambfre	$/\$ $/\$ $\$ ↾_t MblFn

Proof of Theorem cnambfre Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		id 22	. . . . . . . . . 10
2	1	feqmptd 5749	. . . . . . . . 9
3	2	cnveqd 5020	. . . . . . . 8
4	3	imaeq1d 5173	. . . . . . 7
5	4	ad2antrr 725	. . . . . 6 $/\$ $/\$
6		exmid 415	. . . . . . . . . . 11 ↾_t $\/$ ↾_t
7	6	biantrur 506	. . . . . . . . . 10 ↾_t $\/$ ↾_t $/\$
8		andir 863	. . . . . . . . . 10 ↾_t $\/$ ↾_t $/\$ ↾_t $/\$ $\/$ ↾_t $/\$
9	7, 8	bitri 249	. . . . . . . . 9 ↾_t $/\$ $\/$ ↾_t $/\$
10		retopbas 20344	. . . . . . . . . . . . . . . . . 18
11		bastg 18576	. . . . . . . . . . . . . . . . . 18
12	10, 11	ax-mp 5	. . . . . . . . . . . . . . . . 17
13	12	sseli 3357	. . . . . . . . . . . . . . . 16
14	13	ad2antlr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
15		cnpimaex 18865	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ $/\$ ↾_t $/\$
16	15	3com12 1191	. . . . . . . . . . . . . . . 16 $/\$ ↾_t $/\$ ↾_t $/\$
17	16	3expa 1187	. . . . . . . . . . . . . . 15 $/\$ ↾_t $/\$ ↾_t $/\$
18	14, 17	sylanl1 650	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ↾_t $/\$ ↾_t $/\$
19	18	ex 434	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ↾_t ↾_t $/\$
20		simprrr 764	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ↾_t $/\$ $/\$
21		ffn 5564	. . . . . . . . . . . . . . . . . . 19
22	21	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
23		restsspw 14375	. . . . . . . . . . . . . . . . . . . 20 ↾_t
24	23	sseli 3357	. . . . . . . . . . . . . . . . . . 19 ↾_t
25	24	elpwid 3875	. . . . . . . . . . . . . . . . . 18 ↾_t
26		simpl 457	. . . . . . . . . . . . . . . . . 18 $/\$
27		fnfvima 5960	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
28	22, 25, 26, 27	syl3an 1260	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ↾_t $/\$ $/\$
29	28	3expb 1188	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ↾_t $/\$ $/\$
30	20, 29	sseldd 3362	. . . . . . . . . . . . . . 15 $/\$ $/\$ ↾_t $/\$ $/\$
31	30	rexlimdvaa 2847	. . . . . . . . . . . . . 14 $/\$ ↾_t $/\$
32	31	ad3antrrr 729	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ↾_t ↾_t $/\$
33	19, 32	impbid 191	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ ↾_t ↾_t $/\$
34	33	pm5.32da 641	. . . . . . . . . . 11 $/\$ $/\$ $/\$ ↾_t $/\$ ↾_t $/\$ ↾_t $/\$
35		r19.42v 2880	. . . . . . . . . . 11 ↾_t ↾_t $/\$ $/\$ ↾_t $/\$ ↾_t $/\$
36	34, 35	syl6bbr 263	. . . . . . . . . 10 $/\$ $/\$ $/\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$
37	36	orbi1d 702	. . . . . . . . 9 $/\$ $/\$ $/\$ ↾_t $/\$ $\/$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ $\/$ ↾_t $/\$
38	9, 37	syl5bb 257	. . . . . . . 8 $/\$ $/\$ $/\$ ↾_t ↾_t $/\$ $/\$ $\/$ ↾_t $/\$
39	38	rabbidva 2968	. . . . . . 7 $/\$ $/\$ ↾_t ↾_t $/\$ $/\$ $\/$ ↾_t $/\$
40		eqid 2443	. . . . . . . 8
41	40	mptpreima 5336	. . . . . . 7
42		unrab 3626	. . . . . . 7 ↾_t ↾_t $/\$ $/\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ $\/$ ↾_t $/\$
43	39, 41, 42	3eqtr4g 2500	. . . . . 6 $/\$ $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
44	5, 43	eqtrd 2475	. . . . 5 $/\$ $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
45	44	3adantl3 1146	. . . 4 $/\$ $/\$ $\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
46		incom 3548	. . . . . . . . 9 ↾_t $/\$ ↾_t ↾_t ↾_t $/\$
47		dfin4 3595	. . . . . . . . 9 ↾_t $/\$ ↾_t ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
48		inrab 3627	. . . . . . . . . . . 12 ↾_t $/\$ ↾_t $/\$ $/\$
49	48	a1i 11	. . . . . . . . . . 11 ↾_t ↾_t $/\$ ↾_t $/\$ $/\$
50	49	iuneq2i 4194	. . . . . . . . . 10 ↾_t ↾_t $/\$ ↾_t ↾_t $/\$ $/\$
51		iunin2 4239	. . . . . . . . . 10 ↾_t ↾_t $/\$ ↾_t ↾_t $/\$
52		iunrab 4222	. . . . . . . . . 10 ↾_t ↾_t $/\$ $/\$ ↾_t ↾_t $/\$ $/\$
53	50, 51, 52	3eqtr3i 2471	. . . . . . . . 9 ↾_t ↾_t $/\$ ↾_t ↾_t $/\$ $/\$
54	46, 47, 53	3eqtr3i 2471	. . . . . . . 8 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$
55		eqeq2 2452	. . . . . . . . . . . . 13 $/\$ $/\$
56		eqeq2 2452	. . . . . . . . . . . . 13 $/\$ $/\$
57		simprrl 763	. . . . . . . . . . . . . . . 16 ↾_t $/\$ $/\$ $/\$ $/\$
58	25	adantr 465	. . . . . . . . . . . . . . . . . 18 ↾_t $/\$
59	58	sselda 3361	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ $/\$
60		pm3.22 449	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
61	60	adantll 713	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ $/\$ $/\$
62	59, 61	jca 532	. . . . . . . . . . . . . . . 16 ↾_t $/\$ $/\$ $/\$ $/\$
63	57, 62	impbida 828	. . . . . . . . . . . . . . 15 ↾_t $/\$ $/\$ $/\$
64	63	abbidv 2562	. . . . . . . . . . . . . 14 ↾_t $/\$ $/\$ $/\$
65		df-rab 2729	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
66		cvjust 2438	. . . . . . . . . . . . . 14
67	64, 65, 66	3eqtr4g 2500	. . . . . . . . . . . . 13 ↾_t $/\$ $/\$
68		simpr 461	. . . . . . . . . . . . . . . . 17 $/\$
69	68	con3i 135	. . . . . . . . . . . . . . . 16 $/\$
70	69	ralrimivw 2805	. . . . . . . . . . . . . . 15 $/\$
71		rabeq0 3664	. . . . . . . . . . . . . . 15 $/\$ $/\$
72	70, 71	sylibr 212	. . . . . . . . . . . . . 14 $/\$
73	72	adantl 466	. . . . . . . . . . . . 13 ↾_t $/\$ $/\$
74	55, 56, 67, 73	ifbothda 3829	. . . . . . . . . . . 12 ↾_t $/\$
75	74	iuneq2i 4194	. . . . . . . . . . 11 ↾_t $/\$ ↾_t
76		retop 20345	. . . . . . . . . . . . . 14
77		resttop 18769	. . . . . . . . . . . . . 14 $/\$ ↾_t
78	76, 77	mpan 670	. . . . . . . . . . . . 13 ↾_t
79		0opn 18522	. . . . . . . . . . . . . . . 16 ↾_t ↾_t
80	78, 79	syl 16	. . . . . . . . . . . . . . 15 ↾_t
81		ifcl 3836	. . . . . . . . . . . . . . . 16 ↾_t $/\$ ↾_t ↾_t
82	81	ancoms 453	. . . . . . . . . . . . . . 15 ↾_t $/\$ ↾_t ↾_t
83	80, 82	sylan 471	. . . . . . . . . . . . . 14 $/\$ ↾_t ↾_t
84	83	ralrimiva 2804	. . . . . . . . . . . . 13 ↾_t ↾_t
85		iunopn 18516	. . . . . . . . . . . . 13 ↾_t $/\$ ↾_t ↾_t ↾_t ↾_t
86	78, 84, 85	syl2anc 661	. . . . . . . . . . . 12 ↾_t ↾_t
87		eqid 2443	. . . . . . . . . . . . 13 ↾_t ↾_t
88	87	subopnmbl 21089	. . . . . . . . . . . 12 $/\$ ↾_t ↾_t ↾_t
89	86, 88	mpdan 668	. . . . . . . . . . 11 ↾_t
90	75, 89	syl5eqel 2527	. . . . . . . . . 10 ↾_t $/\$
91	90	adantr 465	. . . . . . . . 9 $/\$ $\$ ↾_t ↾_t $/\$
92		difss 3488	. . . . . . . . . . . . 13 ↾_t $/\$ $\$ ↾_t ↾_t $/\$
93		ssrab2 3442	. . . . . . . . . . . . . . 15 $/\$
94	93	rgenw 2788	. . . . . . . . . . . . . 14 ↾_t $/\$
95		iunss 4216	. . . . . . . . . . . . . 14 ↾_t $/\$ ↾_t $/\$
96	94, 95	mpbir 209	. . . . . . . . . . . . 13 ↾_t $/\$
97	92, 96	sstri 3370	. . . . . . . . . . . 12 ↾_t $/\$ $\$ ↾_t
98		mblss 21019	. . . . . . . . . . . 12
99	97, 98	syl5ss 3372	. . . . . . . . . . 11 ↾_t $/\$ $\$ ↾_t
100	99	adantr 465	. . . . . . . . . 10 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
101		ssdif 3496	. . . . . . . . . . . . . 14 ↾_t $/\$ ↾_t $/\$ $\$ ↾_t $\$ ↾_t
102	96, 101	ax-mp 5	. . . . . . . . . . . . 13 ↾_t $/\$ $\$ ↾_t $\$ ↾_t
103		ovex 6121	. . . . . . . . . . . . . . . . . . . . 21
104	103	rabex 4448	. . . . . . . . . . . . . . . . . . . 20 ↾_t $/\$
105		eqid 2443	. . . . . . . . . . . . . . . . . . . 20 ↾_t $/\$ ↾_t $/\$
106	104, 105	fnmpti 5544	. . . . . . . . . . . . . . . . . . 19 ↾_t $/\$
107		retopon 20347	. . . . . . . . . . . . . . . . . . . . . 22 TopOn
108		resttopon 18770	. . . . . . . . . . . . . . . . . . . . . 22 TopOn $/\$ ↾_t TopOn
109	107, 98, 108	sylancr 663	. . . . . . . . . . . . . . . . . . . . 21 ↾_t TopOn
110		cnpfval 18843	. . . . . . . . . . . . . . . . . . . . 21 ↾_t TopOn $/\$ TopOn ↾_t ↾_t $/\$
111	109, 107, 110	sylancl 662	. . . . . . . . . . . . . . . . . . . 20 ↾_t ↾_t $/\$
112	111	fneq1d 5506	. . . . . . . . . . . . . . . . . . 19 ↾_t ↾_t $/\$
113	106, 112	mpbiri 233	. . . . . . . . . . . . . . . . . 18 ↾_t
114		elpreima 5828	. . . . . . . . . . . . . . . . . 18 ↾_t ↾_t $/\$ ↾_t
115	113, 114	syl 16	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ ↾_t
116		rele 4973	. . . . . . . . . . . . . . . . . . . 20
117		elrelimasn 5198	. . . . . . . . . . . . . . . . . . . 20 ↾_t ↾_t
118	116, 117	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ↾_t ↾_t
119		fvex 5706	. . . . . . . . . . . . . . . . . . . 20 ↾_t
120	119	epelc 4639	. . . . . . . . . . . . . . . . . . 19 ↾_t ↾_t
121	118, 120	bitr2i 250	. . . . . . . . . . . . . . . . . 18 ↾_t ↾_t
122	121	anbi2i 694	. . . . . . . . . . . . . . . . 17 $/\$ ↾_t $/\$ ↾_t
123	115, 122	syl6rbbr 264	. . . . . . . . . . . . . . . 16 $/\$ ↾_t ↾_t
124	123	abbidv 2562	. . . . . . . . . . . . . . 15 $/\$ ↾_t ↾_t
125		df-rab 2729	. . . . . . . . . . . . . . 15 ↾_t $/\$ ↾_t
126		imaco 5348	. . . . . . . . . . . . . . . 16 ↾_t ↾_t
127		abid2 2565	. . . . . . . . . . . . . . . 16 ↾_t ↾_t
128	126, 127	eqtr4i 2466	. . . . . . . . . . . . . . 15 ↾_t ↾_t
129	124, 125, 128	3eqtr4g 2500	. . . . . . . . . . . . . 14 ↾_t ↾_t
130	129	difeq2d 3479	. . . . . . . . . . . . 13 $\$ ↾_t $\$ ↾_t
131	102, 130	syl5sseq 3409	. . . . . . . . . . . 12 ↾_t $/\$ $\$ ↾_t $\$ ↾_t
132		difss 3488	. . . . . . . . . . . . 13 $\$ ↾_t
133	132, 98	syl5ss 3372	. . . . . . . . . . . 12 $\$ ↾_t
134	131, 133	jca 532	. . . . . . . . . . 11 ↾_t $/\$ $\$ ↾_t $\$ ↾_t $/\$ $\$ ↾_t
135		ovolssnul 20975	. . . . . . . . . . . 12 ↾_t $/\$ $\$ ↾_t $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
136	135	3expa 1187	. . . . . . . . . . 11 ↾_t $/\$ $\$ ↾_t $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
137	134, 136	sylan 471	. . . . . . . . . 10 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
138		nulmbl 21022	. . . . . . . . . 10 ↾_t $/\$ $\$ ↾_t $/\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
139	100, 137, 138	syl2anc 661	. . . . . . . . 9 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
140		difmbl 21029	. . . . . . . . 9 ↾_t $/\$ $/\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
141	91, 139, 140	syl2anc 661	. . . . . . . 8 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
142	54, 141	syl5eqelr 2528	. . . . . . 7 $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$
143		ssrab2 3442	. . . . . . . . . 10 ↾_t $/\$
144	143, 98	syl5ss 3372	. . . . . . . . 9 ↾_t $/\$
145	144	adantr 465	. . . . . . . 8 $/\$ $\$ ↾_t ↾_t $/\$
146	126	eleq2i 2507	. . . . . . . . . . . . . . . 16 ↾_t ↾_t
147		ibar 504	. . . . . . . . . . . . . . . . . 18 ↾_t $/\$ ↾_t
148	121, 147	syl5rbb 258	. . . . . . . . . . . . . . . . 17 $/\$ ↾_t ↾_t
149	115, 148	sylan9bb 699	. . . . . . . . . . . . . . . 16 $/\$ ↾_t ↾_t
150	146, 149	syl5rbb 258	. . . . . . . . . . . . . . 15 $/\$ ↾_t ↾_t
151	150	notbid 294	. . . . . . . . . . . . . 14 $/\$ ↾_t ↾_t
152	151	biimpd 207	. . . . . . . . . . . . 13 $/\$ ↾_t ↾_t
153	152	adantrd 468	. . . . . . . . . . . 12 $/\$ ↾_t $/\$ ↾_t
154	153	ss2rabdv 3438	. . . . . . . . . . 11 ↾_t $/\$ ↾_t
155		dfdif2 3342	. . . . . . . . . . 11 $\$ ↾_t ↾_t
156	154, 155	syl6sseqr 3408	. . . . . . . . . 10 ↾_t $/\$ $\$ ↾_t
157	156, 133	jca 532	. . . . . . . . 9 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
158		ovolssnul 20975	. . . . . . . . . 10 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$
159	158	3expa 1187	. . . . . . . . 9 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$
160	157, 159	sylan 471	. . . . . . . 8 $/\$ $\$ ↾_t ↾_t $/\$
161		nulmbl 21022	. . . . . . . 8 ↾_t $/\$ $/\$ ↾_t $/\$ ↾_t $/\$
162	145, 160, 161	syl2anc 661	. . . . . . 7 $/\$ $\$ ↾_t ↾_t $/\$
163		unmbl 21024	. . . . . . 7 ↾_t ↾_t $/\$ $/\$ $/\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
164	142, 162, 163	syl2anc 661	. . . . . 6 $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
165	164	3adant1 1006	. . . . 5 $/\$ $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
166	165	adantr 465	. . . 4 $/\$ $/\$ $\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
167	45, 166	eqeltrd 2517	. . 3 $/\$ $/\$ $\$ ↾_t $/\$
168	167	ralrimiva 2804	. 2 $/\$ $/\$ $\$ ↾_t
169		ismbf 21113	. . 3 MblFn
170	169	3ad2ant1 1009	. 2 $/\$ $/\$ $\$ ↾_t MblFn
171	168, 170	mpbird 232	1 $/\$ $/\$ $\$ ↾_t MblFn

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369 $/\$ w3a 965

wceq 1369

wcel 1756

cab 2429

wral 2720

wrex 2721

crab 2724 $\$ cdif 3330

cun 3331

cin 3332

wss 3333

c0 3642

cif 3796

cpw 3865

csn 3882

ciun 4176 class class class wbr 4297

cmpt 4355

cep 4635

ccnv 4844

cdm 4845

crn 4846

cima 4848

ccom 4849

wrel 4850

wfn 5418

wf 5419

cfv 5423 (class class class)co 6096

cmap 7219

cr 9286

cc0 9287

cioo 11305 ↾_t crest 14364

ctg 14381

ctop 18503 TopOnctopon 18504

ctb 18507

ccnp 18834

covol 20951

cvol 20952 MblFncmbf 21099

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 4408 ax-sep 4418 ax-nul 4426 ax-pow 4475 ax-pr 4536 ax-un 6377 ax-inf2 7852 ax-cnex 9343 ax-resscn 9344 ax-1cn 9345 ax-icn 9346 ax-addcl 9347 ax-addrcl 9348 ax-mulcl 9349 ax-mulrcl 9350 ax-mulcom 9351 ax-addass 9352 ax-mulass 9353 ax-distr 9354 ax-i2m1 9355 ax-1ne0 9356 ax-1rid 9357 ax-rnegex 9358 ax-rrecex 9359 ax-cnre 9360 ax-pre-lttri 9361 ax-pre-lttrn 9362 ax-pre-ltadd 9363 ax-pre-mulgt0 9364 ax-pre-sup 9365

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 2573 df-ne 2613 df-nel 2614 df-ral 2725 df-rex 2726 df-reu 2727 df-rmo 2728 df-rab 2729 df-v 2979 df-sbc 3192 df-csb 3294 df-dif 3336 df-un 3338 df-in 3340 df-ss 3347 df-pss 3349 df-nul 3643 df-if 3797 df-pw 3867 df-sn 3883 df-pr 3885 df-tp 3887 df-op 3889 df-uni 4097 df-int 4134 df-iun 4178 df-disj 4268 df-br 4298 df-opab 4356 df-mpt 4357 df-tr 4391 df-eprel 4637 df-id 4641 df-po 4646 df-so 4647 df-fr 4684 df-se 4685 df-we 4686 df-ord 4727 df-on 4728 df-lim 4729 df-suc 4730 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-iota 5386 df-fun 5425 df-fn 5426 df-f 5427 df-f1 5428 df-fo 5429 df-f1o 5430 df-fv 5431 df-isom 5432 df-riota 6057 df-ov 6099 df-oprab 6100 df-mpt2 6101 df-of 6325 df-om 6482 df-1st 6582 df-2nd 6583 df-recs 6837 df-rdg 6871 df-1o 6925 df-2o 6926 df-oadd 6929 df-omul 6930 df-er 7106 df-map 7221 df-pm 7222 df-en 7316 df-dom 7317 df-sdom 7318 df-fin 7319 df-fi 7666 df-sup 7696 df-oi 7729 df-card 8114 df-acn 8117 df-cda 8342 df-pnf 9425 df-mnf 9426 df-xr 9427 df-ltxr 9428 df-le 9429 df-sub 9602 df-neg 9603 df-div 9999 df-nn 10328 df-2 10385 df-3 10386 df-4 10387 df-n0 10585 df-z 10652 df-uz 10867 df-q 10959 df-rp 10997 df-xneg 11094 df-xadd 11095 df-xmul 11096 df-ioo 11309 df-ico 11311 df-icc 11312 df-fz 11443 df-fzo 11554 df-fl 11647 df-seq 11812 df-exp 11871 df-hash 12109 df-cj 12593 df-re 12594 df-im 12595 df-sqr 12729 df-abs 12730 df-clim 12971 df-rlim 12972 df-sum 13169 df-rest 14366 df-topgen 14387 df-psmet 17814 df-xmet 17815 df-met 17816 df-bl 17817 df-mopn 17818 df-top 18508 df-bases 18510 df-topon 18511 df-cnp 18837 df-cmp 18995 df-ovol 20953 df-vol 20954 df-mbf 21104

This theorem is referenced by: (None)

W3C validator