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 30038

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 5911	. . . . . . . . 9
3	2	cnveqd 5168	. . . . . . . 8
4	3	imaeq1d 5326	. . . . . . 7
5	4	ad2antrr 725	. . . . . 6 $/\$ $/\$
6		exmid 415	. . . . . . . . . . 11 ↾_t $\/$ ↾_t
7	6	biantrur 506	. . . . . . . . . 10 ↾_t $\/$ ↾_t $/\$
8		andir 868	. . . . . . . . . 10 ↾_t $\/$ ↾_t $/\$ ↾_t $/\$ $\/$ ↾_t $/\$
9	7, 8	bitri 249	. . . . . . . . 9 ↾_t $/\$ $\/$ ↾_t $/\$
10		retopbas 21244	. . . . . . . . . . . . . . . . . 18
11		bastg 19444	. . . . . . . . . . . . . . . . . 18
12	10, 11	ax-mp 5	. . . . . . . . . . . . . . . . 17
13	12	sseli 3485	. . . . . . . . . . . . . . . 16
14	13	ad2antlr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
15		cnpimaex 19734	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ $/\$ ↾_t $/\$
16	15	3com12 1201	. . . . . . . . . . . . . . . 16 $/\$ ↾_t $/\$ ↾_t $/\$
17	16	3expa 1197	. . . . . . . . . . . . . . 15 $/\$ ↾_t $/\$ ↾_t $/\$
18	14, 17	sylanl1 650	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ↾_t $/\$ ↾_t $/\$
19	18	ex 434	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ↾_t ↾_t $/\$
20		simprrr 766	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ↾_t $/\$ $/\$
21		ffn 5721	. . . . . . . . . . . . . . . . . . 19
22	21	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
23		restsspw 14810	. . . . . . . . . . . . . . . . . . . 20 ↾_t
24	23	sseli 3485	. . . . . . . . . . . . . . . . . . 19 ↾_t
25	24	elpwid 4007	. . . . . . . . . . . . . . . . . 18 ↾_t
26		simpl 457	. . . . . . . . . . . . . . . . . 18 $/\$
27		fnfvima 6135	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
28	22, 25, 26, 27	syl3an 1271	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ↾_t $/\$ $/\$
29	28	3expb 1198	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ↾_t $/\$ $/\$
30	20, 29	sseldd 3490	. . . . . . . . . . . . . . 15 $/\$ $/\$ ↾_t $/\$ $/\$
31	30	rexlimdvaa 2936	. . . . . . . . . . . . . 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 2998	. . . . . . . . . . 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 3086	. . . . . . 7 $/\$ $/\$ ↾_t ↾_t $/\$ $/\$ $\/$ ↾_t $/\$
40		eqid 2443	. . . . . . . 8
41	40	mptpreima 5490	. . . . . . 7
42		unrab 3754	. . . . . . 7 ↾_t ↾_t $/\$ $/\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ $\/$ ↾_t $/\$
43	39, 41, 42	3eqtr4g 2509	. . . . . 6 $/\$ $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
44	5, 43	eqtrd 2484	. . . . 5 $/\$ $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
45	44	3adantl3 1155	. . . 4 $/\$ $/\$ $\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
46		incom 3676	. . . . . . . . 9 ↾_t $/\$ ↾_t ↾_t ↾_t $/\$
47		dfin4 3723	. . . . . . . . 9 ↾_t $/\$ ↾_t ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
48		inrab 3755	. . . . . . . . . . . 12 ↾_t $/\$ ↾_t $/\$ $/\$
49	48	a1i 11	. . . . . . . . . . 11 ↾_t ↾_t $/\$ ↾_t $/\$ $/\$
50	49	iuneq2i 4334	. . . . . . . . . 10 ↾_t ↾_t $/\$ ↾_t ↾_t $/\$ $/\$
51		iunin2 4379	. . . . . . . . . 10 ↾_t ↾_t $/\$ ↾_t ↾_t $/\$
52		iunrab 4362	. . . . . . . . . 10 ↾_t ↾_t $/\$ $/\$ ↾_t ↾_t $/\$ $/\$
53	50, 51, 52	3eqtr3i 2480	. . . . . . . . 9 ↾_t ↾_t $/\$ ↾_t ↾_t $/\$ $/\$
54	46, 47, 53	3eqtr3i 2480	. . . . . . . 8 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$
55		eqeq2 2458	. . . . . . . . . . . . 13 $/\$ $/\$
56		eqeq2 2458	. . . . . . . . . . . . 13 $/\$ $/\$
57		simprrl 765	. . . . . . . . . . . . . . . 16 ↾_t $/\$ $/\$ $/\$ $/\$
58	25	adantr 465	. . . . . . . . . . . . . . . . . 18 ↾_t $/\$
59	58	sselda 3489	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ $/\$
60		pm3.22 449	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
61	60	adantll 713	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ $/\$ $/\$
62	59, 61	jca 532	. . . . . . . . . . . . . . . 16 ↾_t $/\$ $/\$ $/\$ $/\$
63	57, 62	impbida 832	. . . . . . . . . . . . . . 15 ↾_t $/\$ $/\$ $/\$
64	63	abbidv 2579	. . . . . . . . . . . . . 14 ↾_t $/\$ $/\$ $/\$
65		df-rab 2802	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
66		cvjust 2437	. . . . . . . . . . . . . 14
67	64, 65, 66	3eqtr4g 2509	. . . . . . . . . . . . 13 ↾_t $/\$ $/\$
68		simpr 461	. . . . . . . . . . . . . . . . 17 $/\$
69	68	con3i 135	. . . . . . . . . . . . . . . 16 $/\$
70	69	ralrimivw 2858	. . . . . . . . . . . . . . 15 $/\$
71		rabeq0 3793	. . . . . . . . . . . . . . 15 $/\$ $/\$
72	70, 71	sylibr 212	. . . . . . . . . . . . . 14 $/\$
73	72	adantl 466	. . . . . . . . . . . . 13 ↾_t $/\$ $/\$
74	55, 56, 67, 73	ifbothda 3961	. . . . . . . . . . . 12 ↾_t $/\$
75	74	iuneq2i 4334	. . . . . . . . . . 11 ↾_t $/\$ ↾_t
76		retop 21245	. . . . . . . . . . . . . 14
77		resttop 19638	. . . . . . . . . . . . . 14 $/\$ ↾_t
78	76, 77	mpan 670	. . . . . . . . . . . . 13 ↾_t
79		0opn 19390	. . . . . . . . . . . . . . . 16 ↾_t ↾_t
80	78, 79	syl 16	. . . . . . . . . . . . . . 15 ↾_t
81		ifcl 3968	. . . . . . . . . . . . . . . 16 ↾_t $/\$ ↾_t ↾_t
82	81	ancoms 453	. . . . . . . . . . . . . . 15 ↾_t $/\$ ↾_t ↾_t
83	80, 82	sylan 471	. . . . . . . . . . . . . 14 $/\$ ↾_t ↾_t
84	83	ralrimiva 2857	. . . . . . . . . . . . 13 ↾_t ↾_t
85		iunopn 19384	. . . . . . . . . . . . 13 ↾_t $/\$ ↾_t ↾_t ↾_t ↾_t
86	78, 84, 85	syl2anc 661	. . . . . . . . . . . 12 ↾_t ↾_t
87		eqid 2443	. . . . . . . . . . . . 13 ↾_t ↾_t
88	87	subopnmbl 21990	. . . . . . . . . . . 12 $/\$ ↾_t ↾_t ↾_t
89	86, 88	mpdan 668	. . . . . . . . . . 11 ↾_t
90	75, 89	syl5eqel 2535	. . . . . . . . . 10 ↾_t $/\$
91	90	adantr 465	. . . . . . . . 9 $/\$ $\$ ↾_t ↾_t $/\$
92		difss 3616	. . . . . . . . . . . . 13 ↾_t $/\$ $\$ ↾_t ↾_t $/\$
93		ssrab2 3570	. . . . . . . . . . . . . . 15 $/\$
94	93	rgenw 2804	. . . . . . . . . . . . . 14 ↾_t $/\$
95		iunss 4356	. . . . . . . . . . . . . 14 ↾_t $/\$ ↾_t $/\$
96	94, 95	mpbir 209	. . . . . . . . . . . . 13 ↾_t $/\$
97	92, 96	sstri 3498	. . . . . . . . . . . 12 ↾_t $/\$ $\$ ↾_t
98		mblss 21919	. . . . . . . . . . . 12
99	97, 98	syl5ss 3500	. . . . . . . . . . 11 ↾_t $/\$ $\$ ↾_t
100	99	adantr 465	. . . . . . . . . 10 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
101		ssdif 3624	. . . . . . . . . . . . . 14 ↾_t $/\$ ↾_t $/\$ $\$ ↾_t $\$ ↾_t
102	96, 101	ax-mp 5	. . . . . . . . . . . . 13 ↾_t $/\$ $\$ ↾_t $\$ ↾_t
103		ovex 6309	. . . . . . . . . . . . . . . . . . . . 21
104	103	rabex 4588	. . . . . . . . . . . . . . . . . . . 20 ↾_t $/\$
105		eqid 2443	. . . . . . . . . . . . . . . . . . . 20 ↾_t $/\$ ↾_t $/\$
106	104, 105	fnmpti 5699	. . . . . . . . . . . . . . . . . . 19 ↾_t $/\$
107		retopon 21247	. . . . . . . . . . . . . . . . . . . . . 22 TopOn
108		resttopon 19639	. . . . . . . . . . . . . . . . . . . . . 22 TopOn $/\$ ↾_t TopOn
109	107, 98, 108	sylancr 663	. . . . . . . . . . . . . . . . . . . . 21 ↾_t TopOn
110		cnpfval 19712	. . . . . . . . . . . . . . . . . . . . 21 ↾_t TopOn $/\$ TopOn ↾_t ↾_t $/\$
111	109, 107, 110	sylancl 662	. . . . . . . . . . . . . . . . . . . 20 ↾_t ↾_t $/\$
112	111	fneq1d 5661	. . . . . . . . . . . . . . . . . . 19 ↾_t ↾_t $/\$
113	106, 112	mpbiri 233	. . . . . . . . . . . . . . . . . 18 ↾_t
114		elpreima 5992	. . . . . . . . . . . . . . . . . 18 ↾_t ↾_t $/\$ ↾_t
115	113, 114	syl 16	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ ↾_t
116		rele 5121	. . . . . . . . . . . . . . . . . . . 20
117		elrelimasn 5351	. . . . . . . . . . . . . . . . . . . 20 ↾_t ↾_t
118	116, 117	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ↾_t ↾_t
119		fvex 5866	. . . . . . . . . . . . . . . . . . . 20 ↾_t
120	119	epelc 4783	. . . . . . . . . . . . . . . . . . 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 2579	. . . . . . . . . . . . . . 15 $/\$ ↾_t ↾_t
125		df-rab 2802	. . . . . . . . . . . . . . 15 ↾_t $/\$ ↾_t
126		imaco 5502	. . . . . . . . . . . . . . . 16 ↾_t ↾_t
127		abid2 2583	. . . . . . . . . . . . . . . 16 ↾_t ↾_t
128	126, 127	eqtr4i 2475	. . . . . . . . . . . . . . 15 ↾_t ↾_t
129	124, 125, 128	3eqtr4g 2509	. . . . . . . . . . . . . 14 ↾_t ↾_t
130	129	difeq2d 3607	. . . . . . . . . . . . 13 $\$ ↾_t $\$ ↾_t
131	102, 130	syl5sseq 3537	. . . . . . . . . . . 12 ↾_t $/\$ $\$ ↾_t $\$ ↾_t
132		difss 3616	. . . . . . . . . . . . 13 $\$ ↾_t
133	132, 98	syl5ss 3500	. . . . . . . . . . . 12 $\$ ↾_t
134	131, 133	jca 532	. . . . . . . . . . 11 ↾_t $/\$ $\$ ↾_t $\$ ↾_t $/\$ $\$ ↾_t
135		ovolssnul 21875	. . . . . . . . . . . 12 ↾_t $/\$ $\$ ↾_t $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
136	135	3expa 1197	. . . . . . . . . . 11 ↾_t $/\$ $\$ ↾_t $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
137	134, 136	sylan 471	. . . . . . . . . 10 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
138		nulmbl 21923	. . . . . . . . . 10 ↾_t $/\$ $\$ ↾_t $/\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
139	100, 137, 138	syl2anc 661	. . . . . . . . 9 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
140		difmbl 21930	. . . . . . . . 9 ↾_t $/\$ $/\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
141	91, 139, 140	syl2anc 661	. . . . . . . 8 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
142	54, 141	syl5eqelr 2536	. . . . . . 7 $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$
143		ssrab2 3570	. . . . . . . . . 10 ↾_t $/\$
144	143, 98	syl5ss 3500	. . . . . . . . 9 ↾_t $/\$
145	144	adantr 465	. . . . . . . 8 $/\$ $\$ ↾_t ↾_t $/\$
146	126	eleq2i 2521	. . . . . . . . . . . . . . . 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 3566	. . . . . . . . . . 11 ↾_t $/\$ ↾_t
155		dfdif2 3470	. . . . . . . . . . 11 $\$ ↾_t ↾_t
156	154, 155	syl6sseqr 3536	. . . . . . . . . 10 ↾_t $/\$ $\$ ↾_t
157	156, 133	jca 532	. . . . . . . . 9 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
158		ovolssnul 21875	. . . . . . . . . 10 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$
159	158	3expa 1197	. . . . . . . . 9 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$
160	157, 159	sylan 471	. . . . . . . 8 $/\$ $\$ ↾_t ↾_t $/\$
161		nulmbl 21923	. . . . . . . 8 ↾_t $/\$ $/\$ ↾_t $/\$ ↾_t $/\$
162	145, 160, 161	syl2anc 661	. . . . . . 7 $/\$ $\$ ↾_t ↾_t $/\$
163		unmbl 21925	. . . . . . 7 ↾_t ↾_t $/\$ $/\$ $/\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
164	142, 162, 163	syl2anc 661	. . . . . 6 $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
165	164	3adant1 1015	. . . . 5 $/\$ $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
166	165	adantr 465	. . . 4 $/\$ $/\$ $\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
167	45, 166	eqeltrd 2531	. . 3 $/\$ $/\$ $\$ ↾_t $/\$
168	167	ralrimiva 2857	. 2 $/\$ $/\$ $\$ ↾_t
169		ismbf 22014	. . 3 MblFn
170	169	3ad2ant1 1018	. 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 974

wceq 1383

wcel 1804

cab 2428

wral 2793

wrex 2794

crab 2797 $\$ cdif 3458

cun 3459

cin 3460

wss 3461

c0 3770

cif 3926

cpw 3997

csn 4014

ciun 4315 class class class wbr 4437

cmpt 4495

cep 4779

ccnv 4988

cdm 4989

crn 4990

cima 4992

ccom 4993

wrel 4994

wfn 5573

wf 5574

cfv 5578 (class class class)co 6281

cmap 7422

cr 9494

cc0 9495

cioo 11539 ↾_t crest 14799

ctg 14816

ctop 19371 TopOnctopon 19372

ctb 19375

ccnp 19703

covol 21851

cvol 21852 MblFncmbf 22000

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-8 1806 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-rep 4548 ax-sep 4558 ax-nul 4566 ax-pow 4615 ax-pr 4676 ax-un 6577 ax-inf2 8061 ax-cnex 9551 ax-resscn 9552 ax-1cn 9553 ax-icn 9554 ax-addcl 9555 ax-addrcl 9556 ax-mulcl 9557 ax-mulrcl 9558 ax-mulcom 9559 ax-addass 9560 ax-mulass 9561 ax-distr 9562 ax-i2m1 9563 ax-1ne0 9564 ax-1rid 9565 ax-rnegex 9566 ax-rrecex 9567 ax-cnre 9568 ax-pre-lttri 9569 ax-pre-lttrn 9570 ax-pre-ltadd 9571 ax-pre-mulgt0 9572 ax-pre-sup 9573

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 975 df-3an 976 df-tru 1386 df-fal 1389 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-nel 2641 df-ral 2798 df-rex 2799 df-reu 2800 df-rmo 2801 df-rab 2802 df-v 3097 df-sbc 3314 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3771 df-if 3927 df-pw 3999 df-sn 4015 df-pr 4017 df-tp 4019 df-op 4021 df-uni 4235 df-int 4272 df-iun 4317 df-disj 4408 df-br 4438 df-opab 4496 df-mpt 4497 df-tr 4531 df-eprel 4781 df-id 4785 df-po 4790 df-so 4791 df-fr 4828 df-se 4829 df-we 4830 df-ord 4871 df-on 4872 df-lim 4873 df-suc 4874 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-res 5001 df-ima 5002 df-iota 5541 df-fun 5580 df-fn 5581 df-f 5582 df-f1 5583 df-fo 5584 df-f1o 5585 df-fv 5586 df-isom 5587 df-riota 6242 df-ov 6284 df-oprab 6285 df-mpt2 6286 df-of 6525 df-om 6686 df-1st 6785 df-2nd 6786 df-recs 7044 df-rdg 7078 df-1o 7132 df-2o 7133 df-oadd 7136 df-omul 7137 df-er 7313 df-map 7424 df-pm 7425 df-en 7519 df-dom 7520 df-sdom 7521 df-fin 7522 df-fi 7873 df-sup 7903 df-oi 7938 df-card 8323 df-acn 8326 df-cda 8551 df-pnf 9633 df-mnf 9634 df-xr 9635 df-ltxr 9636 df-le 9637 df-sub 9812 df-neg 9813 df-div 10214 df-nn 10544 df-2 10601 df-3 10602 df-4 10603 df-n0 10803 df-z 10872 df-uz 11092 df-q 11193 df-rp 11231 df-xneg 11328 df-xadd 11329 df-xmul 11330 df-ioo 11543 df-ico 11545 df-icc 11546 df-fz 11683 df-fzo 11806 df-fl 11910 df-seq 12089 df-exp 12148 df-hash 12387 df-cj 12913 df-re 12914 df-im 12915 df-sqrt 13049 df-abs 13050 df-clim 13292 df-rlim 13293 df-sum 13490 df-rest 14801 df-topgen 14822 df-psmet 18389 df-xmet 18390 df-met 18391 df-bl 18392 df-mopn 18393 df-top 19376 df-bases 19378 df-topon 19379 df-cnp 19706 df-cmp 19864 df-ovol 21853 df-vol 21854 df-mbf 22005

This theorem is referenced by: (None)

W3C validator