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 31415

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 5901	. . . . . . . . 9
3	2	cnveqd 4998	. . . . . . . 8
4	3	imaeq1d 5155	. . . . . . 7
5	4	ad2antrr 724	. . . . . 6 $/\$ $/\$
6		exmid 413	. . . . . . . . . . 11 ↾_t $\/$ ↾_t
7	6	biantrur 504	. . . . . . . . . 10 ↾_t $\/$ ↾_t $/\$
8		andir 869	. . . . . . . . . 10 ↾_t $\/$ ↾_t $/\$ ↾_t $/\$ $\/$ ↾_t $/\$
9	7, 8	bitri 249	. . . . . . . . 9 ↾_t $/\$ $\/$ ↾_t $/\$
10		retopbas 21557	. . . . . . . . . . . . . . . . . 18
11		bastg 19757	. . . . . . . . . . . . . . . . . 18
12	10, 11	ax-mp 5	. . . . . . . . . . . . . . . . 17
13	12	sseli 3437	. . . . . . . . . . . . . . . 16
14	13	ad2antlr 725	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
15		cnpimaex 20048	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ $/\$ ↾_t $/\$
16	15	3com12 1201	. . . . . . . . . . . . . . . 16 $/\$ ↾_t $/\$ ↾_t $/\$
17	16	3expa 1197	. . . . . . . . . . . . . . 15 $/\$ ↾_t $/\$ ↾_t $/\$
18	14, 17	sylanl1 648	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ↾_t $/\$ ↾_t $/\$
19	18	ex 432	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ↾_t ↾_t $/\$
20		simprrr 767	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ↾_t $/\$ $/\$
21		ffn 5713	. . . . . . . . . . . . . . . . . . 19
22	21	adantr 463	. . . . . . . . . . . . . . . . . 18 $/\$
23		restsspw 15044	. . . . . . . . . . . . . . . . . . . 20 ↾_t
24	23	sseli 3437	. . . . . . . . . . . . . . . . . . 19 ↾_t
25	24	elpwid 3964	. . . . . . . . . . . . . . . . . 18 ↾_t
26		simpl 455	. . . . . . . . . . . . . . . . . 18 $/\$
27		fnfvima 6130	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
28	22, 25, 26, 27	syl3an 1272	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ↾_t $/\$ $/\$
29	28	3expb 1198	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ↾_t $/\$ $/\$
30	20, 29	sseldd 3442	. . . . . . . . . . . . . . 15 $/\$ $/\$ ↾_t $/\$ $/\$
31	30	rexlimdvaa 2896	. . . . . . . . . . . . . 14 $/\$ ↾_t $/\$
32	31	ad3antrrr 728	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ↾_t ↾_t $/\$
33	19, 32	impbid 191	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ ↾_t ↾_t $/\$
34	33	pm5.32da 639	. . . . . . . . . . 11 $/\$ $/\$ $/\$ ↾_t $/\$ ↾_t $/\$ ↾_t $/\$
35		r19.42v 2961	. . . . . . . . . . 11 ↾_t ↾_t $/\$ $/\$ ↾_t $/\$ ↾_t $/\$
36	34, 35	syl6bbr 263	. . . . . . . . . 10 $/\$ $/\$ $/\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$
37	36	orbi1d 701	. . . . . . . . 9 $/\$ $/\$ $/\$ ↾_t $/\$ $\/$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ $\/$ ↾_t $/\$
38	9, 37	syl5bb 257	. . . . . . . 8 $/\$ $/\$ $/\$ ↾_t ↾_t $/\$ $/\$ $\/$ ↾_t $/\$
39	38	rabbidva 3049	. . . . . . 7 $/\$ $/\$ ↾_t ↾_t $/\$ $/\$ $\/$ ↾_t $/\$
40		eqid 2402	. . . . . . . 8
41	40	mptpreima 5315	. . . . . . 7
42		unrab 3720	. . . . . . 7 ↾_t ↾_t $/\$ $/\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ $\/$ ↾_t $/\$
43	39, 41, 42	3eqtr4g 2468	. . . . . 6 $/\$ $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
44	5, 43	eqtrd 2443	. . . . 5 $/\$ $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
45	44	3adantl3 1155	. . . 4 $/\$ $/\$ $\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
46		incom 3631	. . . . . . . . 9 ↾_t $/\$ ↾_t ↾_t ↾_t $/\$
47		dfin4 3689	. . . . . . . . 9 ↾_t $/\$ ↾_t ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
48		inrab 3721	. . . . . . . . . . . 12 ↾_t $/\$ ↾_t $/\$ $/\$
49	48	a1i 11	. . . . . . . . . . 11 ↾_t ↾_t $/\$ ↾_t $/\$ $/\$
50	49	iuneq2i 4289	. . . . . . . . . 10 ↾_t ↾_t $/\$ ↾_t ↾_t $/\$ $/\$
51		iunin2 4334	. . . . . . . . . 10 ↾_t ↾_t $/\$ ↾_t ↾_t $/\$
52		iunrab 4317	. . . . . . . . . 10 ↾_t ↾_t $/\$ $/\$ ↾_t ↾_t $/\$ $/\$
53	50, 51, 52	3eqtr3i 2439	. . . . . . . . 9 ↾_t ↾_t $/\$ ↾_t ↾_t $/\$ $/\$
54	46, 47, 53	3eqtr3i 2439	. . . . . . . 8 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$
55		eqeq2 2417	. . . . . . . . . . . . 13 $/\$ $/\$
56		eqeq2 2417	. . . . . . . . . . . . 13 $/\$ $/\$
57		simprrl 766	. . . . . . . . . . . . . . . 16 ↾_t $/\$ $/\$ $/\$ $/\$
58	25	adantr 463	. . . . . . . . . . . . . . . . . 18 ↾_t $/\$
59	58	sselda 3441	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ $/\$
60		pm3.22 447	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
61	60	adantll 712	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ $/\$ $/\$
62	59, 61	jca 530	. . . . . . . . . . . . . . . 16 ↾_t $/\$ $/\$ $/\$ $/\$
63	57, 62	impbida 833	. . . . . . . . . . . . . . 15 ↾_t $/\$ $/\$ $/\$
64	63	abbidv 2538	. . . . . . . . . . . . . 14 ↾_t $/\$ $/\$ $/\$
65		df-rab 2762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
66		cvjust 2396	. . . . . . . . . . . . . 14
67	64, 65, 66	3eqtr4g 2468	. . . . . . . . . . . . 13 ↾_t $/\$ $/\$
68		simpr 459	. . . . . . . . . . . . . . . . 17 $/\$
69	68	con3i 135	. . . . . . . . . . . . . . . 16 $/\$
70	69	ralrimivw 2818	. . . . . . . . . . . . . . 15 $/\$
71		rabeq0 3760	. . . . . . . . . . . . . . 15 $/\$ $/\$
72	70, 71	sylibr 212	. . . . . . . . . . . . . 14 $/\$
73	72	adantl 464	. . . . . . . . . . . . 13 ↾_t $/\$ $/\$
74	55, 56, 67, 73	ifbothda 3919	. . . . . . . . . . . 12 ↾_t $/\$
75	74	iuneq2i 4289	. . . . . . . . . . 11 ↾_t $/\$ ↾_t
76		retop 21558	. . . . . . . . . . . . . 14
77		resttop 19952	. . . . . . . . . . . . . 14 $/\$ ↾_t
78	76, 77	mpan 668	. . . . . . . . . . . . 13 ↾_t
79		0opn 19703	. . . . . . . . . . . . . . . 16 ↾_t ↾_t
80	78, 79	syl 17	. . . . . . . . . . . . . . 15 ↾_t
81		ifcl 3926	. . . . . . . . . . . . . . . 16 ↾_t $/\$ ↾_t ↾_t
82	81	ancoms 451	. . . . . . . . . . . . . . 15 ↾_t $/\$ ↾_t ↾_t
83	80, 82	sylan 469	. . . . . . . . . . . . . 14 $/\$ ↾_t ↾_t
84	83	ralrimiva 2817	. . . . . . . . . . . . 13 ↾_t ↾_t
85		iunopn 19697	. . . . . . . . . . . . 13 ↾_t $/\$ ↾_t ↾_t ↾_t ↾_t
86	78, 84, 85	syl2anc 659	. . . . . . . . . . . 12 ↾_t ↾_t
87		eqid 2402	. . . . . . . . . . . . 13 ↾_t ↾_t
88	87	subopnmbl 22303	. . . . . . . . . . . 12 $/\$ ↾_t ↾_t ↾_t
89	86, 88	mpdan 666	. . . . . . . . . . 11 ↾_t
90	75, 89	syl5eqel 2494	. . . . . . . . . 10 ↾_t $/\$
91	90	adantr 463	. . . . . . . . 9 $/\$ $\$ ↾_t ↾_t $/\$
92		difss 3569	. . . . . . . . . . . . 13 ↾_t $/\$ $\$ ↾_t ↾_t $/\$
93		ssrab2 3523	. . . . . . . . . . . . . . 15 $/\$
94	93	rgenw 2764	. . . . . . . . . . . . . 14 ↾_t $/\$
95		iunss 4311	. . . . . . . . . . . . . 14 ↾_t $/\$ ↾_t $/\$
96	94, 95	mpbir 209	. . . . . . . . . . . . 13 ↾_t $/\$
97	92, 96	sstri 3450	. . . . . . . . . . . 12 ↾_t $/\$ $\$ ↾_t
98		mblss 22232	. . . . . . . . . . . 12
99	97, 98	syl5ss 3452	. . . . . . . . . . 11 ↾_t $/\$ $\$ ↾_t
100	99	adantr 463	. . . . . . . . . 10 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
101		ssdif 3577	. . . . . . . . . . . . . 14 ↾_t $/\$ ↾_t $/\$ $\$ ↾_t $\$ ↾_t
102	96, 101	ax-mp 5	. . . . . . . . . . . . 13 ↾_t $/\$ $\$ ↾_t $\$ ↾_t
103		ovex 6305	. . . . . . . . . . . . . . . . . . . . 21
104	103	rabex 4544	. . . . . . . . . . . . . . . . . . . 20 ↾_t $/\$
105		eqid 2402	. . . . . . . . . . . . . . . . . . . 20 ↾_t $/\$ ↾_t $/\$
106	104, 105	fnmpti 5691	. . . . . . . . . . . . . . . . . . 19 ↾_t $/\$
107		retopon 21560	. . . . . . . . . . . . . . . . . . . . . 22 TopOn
108		resttopon 19953	. . . . . . . . . . . . . . . . . . . . . 22 TopOn $/\$ ↾_t TopOn
109	107, 98, 108	sylancr 661	. . . . . . . . . . . . . . . . . . . . 21 ↾_t TopOn
110		cnpfval 20026	. . . . . . . . . . . . . . . . . . . . 21 ↾_t TopOn $/\$ TopOn ↾_t ↾_t $/\$
111	109, 107, 110	sylancl 660	. . . . . . . . . . . . . . . . . . . 20 ↾_t ↾_t $/\$
112	111	fneq1d 5651	. . . . . . . . . . . . . . . . . . 19 ↾_t ↾_t $/\$
113	106, 112	mpbiri 233	. . . . . . . . . . . . . . . . . 18 ↾_t
114		elpreima 5984	. . . . . . . . . . . . . . . . . 18 ↾_t ↾_t $/\$ ↾_t
115	113, 114	syl 17	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ ↾_t
116		rele 4951	. . . . . . . . . . . . . . . . . . . 20
117		elrelimasn 5180	. . . . . . . . . . . . . . . . . . . 20 ↾_t ↾_t
118	116, 117	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ↾_t ↾_t
119		fvex 5858	. . . . . . . . . . . . . . . . . . . 20 ↾_t
120	119	epelc 4735	. . . . . . . . . . . . . . . . . . 19 ↾_t ↾_t
121	118, 120	bitr2i 250	. . . . . . . . . . . . . . . . . 18 ↾_t ↾_t
122	121	anbi2i 692	. . . . . . . . . . . . . . . . 17 $/\$ ↾_t $/\$ ↾_t
123	115, 122	syl6rbbr 264	. . . . . . . . . . . . . . . 16 $/\$ ↾_t ↾_t
124	123	abbidv 2538	. . . . . . . . . . . . . . 15 $/\$ ↾_t ↾_t
125		df-rab 2762	. . . . . . . . . . . . . . 15 ↾_t $/\$ ↾_t
126		imaco 5327	. . . . . . . . . . . . . . . 16 ↾_t ↾_t
127		abid2 2542	. . . . . . . . . . . . . . . 16 ↾_t ↾_t
128	126, 127	eqtr4i 2434	. . . . . . . . . . . . . . 15 ↾_t ↾_t
129	124, 125, 128	3eqtr4g 2468	. . . . . . . . . . . . . 14 ↾_t ↾_t
130	129	difeq2d 3560	. . . . . . . . . . . . 13 $\$ ↾_t $\$ ↾_t
131	102, 130	syl5sseq 3489	. . . . . . . . . . . 12 ↾_t $/\$ $\$ ↾_t $\$ ↾_t
132		difss 3569	. . . . . . . . . . . . 13 $\$ ↾_t
133	132, 98	syl5ss 3452	. . . . . . . . . . . 12 $\$ ↾_t
134	131, 133	jca 530	. . . . . . . . . . 11 ↾_t $/\$ $\$ ↾_t $\$ ↾_t $/\$ $\$ ↾_t
135		ovolssnul 22188	. . . . . . . . . . . 12 ↾_t $/\$ $\$ ↾_t $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
136	135	3expa 1197	. . . . . . . . . . 11 ↾_t $/\$ $\$ ↾_t $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
137	134, 136	sylan 469	. . . . . . . . . 10 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
138		nulmbl 22236	. . . . . . . . . 10 ↾_t $/\$ $\$ ↾_t $/\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
139	100, 137, 138	syl2anc 659	. . . . . . . . 9 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
140		difmbl 22243	. . . . . . . . 9 ↾_t $/\$ $/\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
141	91, 139, 140	syl2anc 659	. . . . . . . 8 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
142	54, 141	syl5eqelr 2495	. . . . . . 7 $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$
143		ssrab2 3523	. . . . . . . . . 10 ↾_t $/\$
144	143, 98	syl5ss 3452	. . . . . . . . 9 ↾_t $/\$
145	144	adantr 463	. . . . . . . 8 $/\$ $\$ ↾_t ↾_t $/\$
146	126	eleq2i 2480	. . . . . . . . . . . . . . . 16 ↾_t ↾_t
147		ibar 502	. . . . . . . . . . . . . . . . . 18 ↾_t $/\$ ↾_t
148	121, 147	syl5rbb 258	. . . . . . . . . . . . . . . . 17 $/\$ ↾_t ↾_t
149	115, 148	sylan9bb 698	. . . . . . . . . . . . . . . 16 $/\$ ↾_t ↾_t
150	146, 149	syl5rbb 258	. . . . . . . . . . . . . . 15 $/\$ ↾_t ↾_t
151	150	notbid 292	. . . . . . . . . . . . . 14 $/\$ ↾_t ↾_t
152	151	biimpd 207	. . . . . . . . . . . . 13 $/\$ ↾_t ↾_t
153	152	adantrd 466	. . . . . . . . . . . 12 $/\$ ↾_t $/\$ ↾_t
154	153	ss2rabdv 3519	. . . . . . . . . . 11 ↾_t $/\$ ↾_t
155		dfdif2 3422	. . . . . . . . . . 11 $\$ ↾_t ↾_t
156	154, 155	syl6sseqr 3488	. . . . . . . . . 10 ↾_t $/\$ $\$ ↾_t
157	156, 133	jca 530	. . . . . . . . 9 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
158		ovolssnul 22188	. . . . . . . . . 10 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$
159	158	3expa 1197	. . . . . . . . 9 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$
160	157, 159	sylan 469	. . . . . . . 8 $/\$ $\$ ↾_t ↾_t $/\$
161		nulmbl 22236	. . . . . . . 8 ↾_t $/\$ $/\$ ↾_t $/\$ ↾_t $/\$
162	145, 160, 161	syl2anc 659	. . . . . . 7 $/\$ $\$ ↾_t ↾_t $/\$
163		unmbl 22238	. . . . . . 7 ↾_t ↾_t $/\$ $/\$ $/\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
164	142, 162, 163	syl2anc 659	. . . . . 6 $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
165	164	3adant1 1015	. . . . 5 $/\$ $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
166	165	adantr 463	. . . 4 $/\$ $/\$ $\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
167	45, 166	eqeltrd 2490	. . 3 $/\$ $/\$ $\$ ↾_t $/\$
168	167	ralrimiva 2817	. 2 $/\$ $/\$ $\$ ↾_t
169		ismbf 22327	. . 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 366 $/\$ wa 367 $/\$ w3a 974

wceq 1405

wcel 1842

cab 2387

wral 2753

wrex 2754

crab 2757 $\$ cdif 3410

cun 3411

cin 3412

wss 3413

c0 3737

cif 3884

cpw 3954

csn 3971

ciun 4270 class class class wbr 4394

cmpt 4452

cep 4731

ccnv 4821

cdm 4822

crn 4823

cima 4825

ccom 4826

wrel 4827

wfn 5563

wf 5564

cfv 5568 (class class class)co 6277

cmap 7456

cr 9520

cc0 9521

cioo 11581 ↾_t crest 15033

ctg 15050

ctop 19684 TopOnctopon 19685

ctb 19688

ccnp 20017

covol 22164

cvol 22165 MblFncmbf 22313

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-rep 4506 ax-sep 4516 ax-nul 4524 ax-pow 4571 ax-pr 4629 ax-un 6573 ax-inf2 8090 ax-cnex 9577 ax-resscn 9578 ax-1cn 9579 ax-icn 9580 ax-addcl 9581 ax-addrcl 9582 ax-mulcl 9583 ax-mulrcl 9584 ax-mulcom 9585 ax-addass 9586 ax-mulass 9587 ax-distr 9588 ax-i2m1 9589 ax-1ne0 9590 ax-1rid 9591 ax-rnegex 9592 ax-rrecex 9593 ax-cnre 9594 ax-pre-lttri 9595 ax-pre-lttrn 9596 ax-pre-ltadd 9597 ax-pre-mulgt0 9598 ax-pre-sup 9599

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 975 df-3an 976 df-tru 1408 df-fal 1411 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-nel 2601 df-ral 2758 df-rex 2759 df-reu 2760 df-rmo 2761 df-rab 2762 df-v 3060 df-sbc 3277 df-csb 3373 df-dif 3416 df-un 3418 df-in 3420 df-ss 3427 df-pss 3429 df-nul 3738 df-if 3885 df-pw 3956 df-sn 3972 df-pr 3974 df-tp 3976 df-op 3978 df-uni 4191 df-int 4227 df-iun 4272 df-disj 4366 df-br 4395 df-opab 4453 df-mpt 4454 df-tr 4489 df-eprel 4733 df-id 4737 df-po 4743 df-so 4744 df-fr 4781 df-se 4782 df-we 4783 df-xp 4828 df-rel 4829 df-cnv 4830 df-co 4831 df-dm 4832 df-rn 4833 df-res 4834 df-ima 4835 df-pred 5366 df-ord 5412 df-on 5413 df-lim 5414 df-suc 5415 df-iota 5532 df-fun 5570 df-fn 5571 df-f 5572 df-f1 5573 df-fo 5574 df-f1o 5575 df-fv 5576 df-isom 5577 df-riota 6239 df-ov 6280 df-oprab 6281 df-mpt2 6282 df-of 6520 df-om 6683 df-1st 6783 df-2nd 6784 df-wrecs 7012 df-recs 7074 df-rdg 7112 df-1o 7166 df-2o 7167 df-oadd 7170 df-omul 7171 df-er 7347 df-map 7458 df-pm 7459 df-en 7554 df-dom 7555 df-sdom 7556 df-fin 7557 df-fi 7904 df-sup 7934 df-oi 7968 df-card 8351 df-acn 8354 df-cda 8579 df-pnf 9659 df-mnf 9660 df-xr 9661 df-ltxr 9662 df-le 9663 df-sub 9842 df-neg 9843 df-div 10247 df-nn 10576 df-2 10634 df-3 10635 df-4 10636 df-n0 10836 df-z 10905 df-uz 11127 df-q 11227 df-rp 11265 df-xneg 11370 df-xadd 11371 df-xmul 11372 df-ioo 11585 df-ico 11587 df-icc 11588 df-fz 11725 df-fzo 11853 df-fl 11964 df-seq 12150 df-exp 12209 df-hash 12451 df-cj 13079 df-re 13080 df-im 13081 df-sqrt 13215 df-abs 13216 df-clim 13458 df-rlim 13459 df-sum 13656 df-rest 15035 df-topgen 15056 df-psmet 18729 df-xmet 18730 df-met 18731 df-bl 18732 df-mopn 18733 df-top 19689 df-bases 19691 df-topon 19692 df-cnp 20020 df-cmp 20178 df-ovol 22166 df-vol 22167 df-mbf 22318

This theorem is referenced by: (None)

W3C validator