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 29668

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 5920	. . . . . . . . 9
3	2	cnveqd 5178	. . . . . . . 8
4	3	imaeq1d 5336	. . . . . . 7
5	4	ad2antrr 725	. . . . . 6 $/\$ $/\$
6		exmid 415	. . . . . . . . . . 11 ↾_t $\/$ ↾_t
7	6	biantrur 506	. . . . . . . . . 10 ↾_t $\/$ ↾_t $/\$
8		andir 866	. . . . . . . . . 10 ↾_t $\/$ ↾_t $/\$ ↾_t $/\$ $\/$ ↾_t $/\$
9	7, 8	bitri 249	. . . . . . . . 9 ↾_t $/\$ $\/$ ↾_t $/\$
10		retopbas 21030	. . . . . . . . . . . . . . . . . 18
11		bastg 19262	. . . . . . . . . . . . . . . . . 18
12	10, 11	ax-mp 5	. . . . . . . . . . . . . . . . 17
13	12	sseli 3500	. . . . . . . . . . . . . . . 16
14	13	ad2antlr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
15		cnpimaex 19551	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ $/\$ ↾_t $/\$
16	15	3com12 1200	. . . . . . . . . . . . . . . 16 $/\$ ↾_t $/\$ ↾_t $/\$
17	16	3expa 1196	. . . . . . . . . . . . . . 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 5731	. . . . . . . . . . . . . . . . . . 19
22	21	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
23		restsspw 14687	. . . . . . . . . . . . . . . . . . . 20 ↾_t
24	23	sseli 3500	. . . . . . . . . . . . . . . . . . 19 ↾_t
25	24	elpwid 4020	. . . . . . . . . . . . . . . . . 18 ↾_t
26		simpl 457	. . . . . . . . . . . . . . . . . 18 $/\$
27		fnfvima 6138	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
28	22, 25, 26, 27	syl3an 1270	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ↾_t $/\$ $/\$
29	28	3expb 1197	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ↾_t $/\$ $/\$
30	20, 29	sseldd 3505	. . . . . . . . . . . . . . 15 $/\$ $/\$ ↾_t $/\$ $/\$
31	30	rexlimdvaa 2956	. . . . . . . . . . . . . 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 3016	. . . . . . . . . . 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 3104	. . . . . . 7 $/\$ $/\$ ↾_t ↾_t $/\$ $/\$ $\/$ ↾_t $/\$
40		eqid 2467	. . . . . . . 8
41	40	mptpreima 5500	. . . . . . 7
42		unrab 3769	. . . . . . 7 ↾_t ↾_t $/\$ $/\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ $\/$ ↾_t $/\$
43	39, 41, 42	3eqtr4g 2533	. . . . . 6 $/\$ $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
44	5, 43	eqtrd 2508	. . . . 5 $/\$ $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
45	44	3adantl3 1154	. . . 4 $/\$ $/\$ $\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
46		incom 3691	. . . . . . . . 9 ↾_t $/\$ ↾_t ↾_t ↾_t $/\$
47		dfin4 3738	. . . . . . . . 9 ↾_t $/\$ ↾_t ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
48		inrab 3770	. . . . . . . . . . . 12 ↾_t $/\$ ↾_t $/\$ $/\$
49	48	a1i 11	. . . . . . . . . . 11 ↾_t ↾_t $/\$ ↾_t $/\$ $/\$
50	49	iuneq2i 4344	. . . . . . . . . 10 ↾_t ↾_t $/\$ ↾_t ↾_t $/\$ $/\$
51		iunin2 4389	. . . . . . . . . 10 ↾_t ↾_t $/\$ ↾_t ↾_t $/\$
52		iunrab 4372	. . . . . . . . . 10 ↾_t ↾_t $/\$ $/\$ ↾_t ↾_t $/\$ $/\$
53	50, 51, 52	3eqtr3i 2504	. . . . . . . . 9 ↾_t ↾_t $/\$ ↾_t ↾_t $/\$ $/\$
54	46, 47, 53	3eqtr3i 2504	. . . . . . . 8 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$
55		eqeq2 2482	. . . . . . . . . . . . 13 $/\$ $/\$
56		eqeq2 2482	. . . . . . . . . . . . 13 $/\$ $/\$
57		simprrl 763	. . . . . . . . . . . . . . . 16 ↾_t $/\$ $/\$ $/\$ $/\$
58	25	adantr 465	. . . . . . . . . . . . . . . . . 18 ↾_t $/\$
59	58	sselda 3504	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ $/\$
60		pm3.22 449	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
61	60	adantll 713	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ $/\$ $/\$
62	59, 61	jca 532	. . . . . . . . . . . . . . . 16 ↾_t $/\$ $/\$ $/\$ $/\$
63	57, 62	impbida 830	. . . . . . . . . . . . . . 15 ↾_t $/\$ $/\$ $/\$
64	63	abbidv 2603	. . . . . . . . . . . . . 14 ↾_t $/\$ $/\$ $/\$
65		df-rab 2823	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
66		cvjust 2461	. . . . . . . . . . . . . 14
67	64, 65, 66	3eqtr4g 2533	. . . . . . . . . . . . 13 ↾_t $/\$ $/\$
68		simpr 461	. . . . . . . . . . . . . . . . 17 $/\$
69	68	con3i 135	. . . . . . . . . . . . . . . 16 $/\$
70	69	ralrimivw 2879	. . . . . . . . . . . . . . 15 $/\$
71		rabeq0 3807	. . . . . . . . . . . . . . 15 $/\$ $/\$
72	70, 71	sylibr 212	. . . . . . . . . . . . . 14 $/\$
73	72	adantl 466	. . . . . . . . . . . . 13 ↾_t $/\$ $/\$
74	55, 56, 67, 73	ifbothda 3974	. . . . . . . . . . . 12 ↾_t $/\$
75	74	iuneq2i 4344	. . . . . . . . . . 11 ↾_t $/\$ ↾_t
76		retop 21031	. . . . . . . . . . . . . 14
77		resttop 19455	. . . . . . . . . . . . . 14 $/\$ ↾_t
78	76, 77	mpan 670	. . . . . . . . . . . . 13 ↾_t
79		0opn 19208	. . . . . . . . . . . . . . . 16 ↾_t ↾_t
80	78, 79	syl 16	. . . . . . . . . . . . . . 15 ↾_t
81		ifcl 3981	. . . . . . . . . . . . . . . 16 ↾_t $/\$ ↾_t ↾_t
82	81	ancoms 453	. . . . . . . . . . . . . . 15 ↾_t $/\$ ↾_t ↾_t
83	80, 82	sylan 471	. . . . . . . . . . . . . 14 $/\$ ↾_t ↾_t
84	83	ralrimiva 2878	. . . . . . . . . . . . 13 ↾_t ↾_t
85		iunopn 19202	. . . . . . . . . . . . 13 ↾_t $/\$ ↾_t ↾_t ↾_t ↾_t
86	78, 84, 85	syl2anc 661	. . . . . . . . . . . 12 ↾_t ↾_t
87		eqid 2467	. . . . . . . . . . . . 13 ↾_t ↾_t
88	87	subopnmbl 21776	. . . . . . . . . . . 12 $/\$ ↾_t ↾_t ↾_t
89	86, 88	mpdan 668	. . . . . . . . . . 11 ↾_t
90	75, 89	syl5eqel 2559	. . . . . . . . . 10 ↾_t $/\$
91	90	adantr 465	. . . . . . . . 9 $/\$ $\$ ↾_t ↾_t $/\$
92		difss 3631	. . . . . . . . . . . . 13 ↾_t $/\$ $\$ ↾_t ↾_t $/\$
93		ssrab2 3585	. . . . . . . . . . . . . . 15 $/\$
94	93	rgenw 2825	. . . . . . . . . . . . . 14 ↾_t $/\$
95		iunss 4366	. . . . . . . . . . . . . 14 ↾_t $/\$ ↾_t $/\$
96	94, 95	mpbir 209	. . . . . . . . . . . . 13 ↾_t $/\$
97	92, 96	sstri 3513	. . . . . . . . . . . 12 ↾_t $/\$ $\$ ↾_t
98		mblss 21705	. . . . . . . . . . . 12
99	97, 98	syl5ss 3515	. . . . . . . . . . 11 ↾_t $/\$ $\$ ↾_t
100	99	adantr 465	. . . . . . . . . 10 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
101		ssdif 3639	. . . . . . . . . . . . . 14 ↾_t $/\$ ↾_t $/\$ $\$ ↾_t $\$ ↾_t
102	96, 101	ax-mp 5	. . . . . . . . . . . . 13 ↾_t $/\$ $\$ ↾_t $\$ ↾_t
103		ovex 6309	. . . . . . . . . . . . . . . . . . . . 21
104	103	rabex 4598	. . . . . . . . . . . . . . . . . . . 20 ↾_t $/\$
105		eqid 2467	. . . . . . . . . . . . . . . . . . . 20 ↾_t $/\$ ↾_t $/\$
106	104, 105	fnmpti 5709	. . . . . . . . . . . . . . . . . . 19 ↾_t $/\$
107		retopon 21033	. . . . . . . . . . . . . . . . . . . . . 22 TopOn
108		resttopon 19456	. . . . . . . . . . . . . . . . . . . . . 22 TopOn $/\$ ↾_t TopOn
109	107, 98, 108	sylancr 663	. . . . . . . . . . . . . . . . . . . . 21 ↾_t TopOn
110		cnpfval 19529	. . . . . . . . . . . . . . . . . . . . 21 ↾_t TopOn $/\$ TopOn ↾_t ↾_t $/\$
111	109, 107, 110	sylancl 662	. . . . . . . . . . . . . . . . . . . 20 ↾_t ↾_t $/\$
112	111	fneq1d 5671	. . . . . . . . . . . . . . . . . . 19 ↾_t ↾_t $/\$
113	106, 112	mpbiri 233	. . . . . . . . . . . . . . . . . 18 ↾_t
114		elpreima 6001	. . . . . . . . . . . . . . . . . 18 ↾_t ↾_t $/\$ ↾_t
115	113, 114	syl 16	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ ↾_t
116		rele 5131	. . . . . . . . . . . . . . . . . . . 20
117		elrelimasn 5361	. . . . . . . . . . . . . . . . . . . 20 ↾_t ↾_t
118	116, 117	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ↾_t ↾_t
119		fvex 5876	. . . . . . . . . . . . . . . . . . . 20 ↾_t
120	119	epelc 4793	. . . . . . . . . . . . . . . . . . 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 2603	. . . . . . . . . . . . . . 15 $/\$ ↾_t ↾_t
125		df-rab 2823	. . . . . . . . . . . . . . 15 ↾_t $/\$ ↾_t
126		imaco 5512	. . . . . . . . . . . . . . . 16 ↾_t ↾_t
127		abid2 2607	. . . . . . . . . . . . . . . 16 ↾_t ↾_t
128	126, 127	eqtr4i 2499	. . . . . . . . . . . . . . 15 ↾_t ↾_t
129	124, 125, 128	3eqtr4g 2533	. . . . . . . . . . . . . 14 ↾_t ↾_t
130	129	difeq2d 3622	. . . . . . . . . . . . 13 $\$ ↾_t $\$ ↾_t
131	102, 130	syl5sseq 3552	. . . . . . . . . . . 12 ↾_t $/\$ $\$ ↾_t $\$ ↾_t
132		difss 3631	. . . . . . . . . . . . 13 $\$ ↾_t
133	132, 98	syl5ss 3515	. . . . . . . . . . . 12 $\$ ↾_t
134	131, 133	jca 532	. . . . . . . . . . 11 ↾_t $/\$ $\$ ↾_t $\$ ↾_t $/\$ $\$ ↾_t
135		ovolssnul 21661	. . . . . . . . . . . 12 ↾_t $/\$ $\$ ↾_t $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
136	135	3expa 1196	. . . . . . . . . . 11 ↾_t $/\$ $\$ ↾_t $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
137	134, 136	sylan 471	. . . . . . . . . 10 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
138		nulmbl 21709	. . . . . . . . . 10 ↾_t $/\$ $\$ ↾_t $/\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
139	100, 137, 138	syl2anc 661	. . . . . . . . 9 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
140		difmbl 21716	. . . . . . . . 9 ↾_t $/\$ $/\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
141	91, 139, 140	syl2anc 661	. . . . . . . 8 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
142	54, 141	syl5eqelr 2560	. . . . . . 7 $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$
143		ssrab2 3585	. . . . . . . . . 10 ↾_t $/\$
144	143, 98	syl5ss 3515	. . . . . . . . 9 ↾_t $/\$
145	144	adantr 465	. . . . . . . 8 $/\$ $\$ ↾_t ↾_t $/\$
146	126	eleq2i 2545	. . . . . . . . . . . . . . . 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 3581	. . . . . . . . . . 11 ↾_t $/\$ ↾_t
155		dfdif2 3485	. . . . . . . . . . 11 $\$ ↾_t ↾_t
156	154, 155	syl6sseqr 3551	. . . . . . . . . 10 ↾_t $/\$ $\$ ↾_t
157	156, 133	jca 532	. . . . . . . . 9 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
158		ovolssnul 21661	. . . . . . . . . 10 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$
159	158	3expa 1196	. . . . . . . . 9 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$
160	157, 159	sylan 471	. . . . . . . 8 $/\$ $\$ ↾_t ↾_t $/\$
161		nulmbl 21709	. . . . . . . 8 ↾_t $/\$ $/\$ ↾_t $/\$ ↾_t $/\$
162	145, 160, 161	syl2anc 661	. . . . . . 7 $/\$ $\$ ↾_t ↾_t $/\$
163		unmbl 21711	. . . . . . 7 ↾_t ↾_t $/\$ $/\$ $/\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
164	142, 162, 163	syl2anc 661	. . . . . 6 $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
165	164	3adant1 1014	. . . . 5 $/\$ $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
166	165	adantr 465	. . . 4 $/\$ $/\$ $\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
167	45, 166	eqeltrd 2555	. . 3 $/\$ $/\$ $\$ ↾_t $/\$
168	167	ralrimiva 2878	. 2 $/\$ $/\$ $\$ ↾_t
169		ismbf 21800	. . 3 MblFn
170	169	3ad2ant1 1017	. 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 973

wceq 1379

wcel 1767

cab 2452

wral 2814

wrex 2815

crab 2818 $\$ cdif 3473

cun 3474

cin 3475

wss 3476

c0 3785

cif 3939

cpw 4010

csn 4027

ciun 4325 class class class wbr 4447

cmpt 4505

cep 4789

ccnv 4998

cdm 4999

crn 5000

cima 5002

ccom 5003

wrel 5004

wfn 5583

wf 5584

cfv 5588 (class class class)co 6284

cmap 7420

cr 9491

cc0 9492

cioo 11529 ↾_t crest 14676

ctg 14693

ctop 19189 TopOnctopon 19190

ctb 19193

ccnp 19520

covol 21637

cvol 21638 MblFncmbf 21786

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6576 ax-inf2 8058 ax-cnex 9548 ax-resscn 9549 ax-1cn 9550 ax-icn 9551 ax-addcl 9552 ax-addrcl 9553 ax-mulcl 9554 ax-mulrcl 9555 ax-mulcom 9556 ax-addass 9557 ax-mulass 9558 ax-distr 9559 ax-i2m1 9560 ax-1ne0 9561 ax-1rid 9562 ax-rnegex 9563 ax-rrecex 9564 ax-cnre 9565 ax-pre-lttri 9566 ax-pre-lttrn 9567 ax-pre-ltadd 9568 ax-pre-mulgt0 9569 ax-pre-sup 9570

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-disj 4418 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-isom 5597 df-riota 6245 df-ov 6287 df-oprab 6288 df-mpt2 6289 df-of 6524 df-om 6685 df-1st 6784 df-2nd 6785 df-recs 7042 df-rdg 7076 df-1o 7130 df-2o 7131 df-oadd 7134 df-omul 7135 df-er 7311 df-map 7422 df-pm 7423 df-en 7517 df-dom 7518 df-sdom 7519 df-fin 7520 df-fi 7871 df-sup 7901 df-oi 7935 df-card 8320 df-acn 8323 df-cda 8548 df-pnf 9630 df-mnf 9631 df-xr 9632 df-ltxr 9633 df-le 9634 df-sub 9807 df-neg 9808 df-div 10207 df-nn 10537 df-2 10594 df-3 10595 df-4 10596 df-n0 10796 df-z 10865 df-uz 11083 df-q 11183 df-rp 11221 df-xneg 11318 df-xadd 11319 df-xmul 11320 df-ioo 11533 df-ico 11535 df-icc 11536 df-fz 11673 df-fzo 11793 df-fl 11897 df-seq 12076 df-exp 12135 df-hash 12374 df-cj 12895 df-re 12896 df-im 12897 df-sqrt 13031 df-abs 13032 df-clim 13274 df-rlim 13275 df-sum 13472 df-rest 14678 df-topgen 14699 df-psmet 18210 df-xmet 18211 df-met 18212 df-bl 18213 df-mopn 18214 df-top 19194 df-bases 19196 df-topon 19197 df-cnp 19523 df-cmp 19681 df-ovol 21639 df-vol 21640 df-mbf 21791

This theorem is referenced by: (None)

W3C validator