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 31953

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 5934	. . . . . . . . 9
3	2	cnveqd 5029	. . . . . . . 8
4	3	imaeq1d 5186	. . . . . . 7
5	4	ad2antrr 730	. . . . . 6 $/\$ $/\$
6		exmid 416	. . . . . . . . . . 11 ↾_t $\/$ ↾_t
7	6	biantrur 508	. . . . . . . . . 10 ↾_t $\/$ ↾_t $/\$
8		andir 876	. . . . . . . . . 10 ↾_t $\/$ ↾_t $/\$ ↾_t $/\$ $\/$ ↾_t $/\$
9	7, 8	bitri 252	. . . . . . . . 9 ↾_t $/\$ $\/$ ↾_t $/\$
10		retopbas 21779	. . . . . . . . . . . . . . . . . 18
11		bastg 19979	. . . . . . . . . . . . . . . . . 18
12	10, 11	ax-mp 5	. . . . . . . . . . . . . . . . 17
13	12	sseli 3460	. . . . . . . . . . . . . . . 16
14	13	ad2antlr 731	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
15		cnpimaex 20270	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ $/\$ ↾_t $/\$
16	15	3com12 1209	. . . . . . . . . . . . . . . 16 $/\$ ↾_t $/\$ ↾_t $/\$
17	16	3expa 1205	. . . . . . . . . . . . . . 15 $/\$ ↾_t $/\$ ↾_t $/\$
18	14, 17	sylanl1 654	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ↾_t $/\$ ↾_t $/\$
19	18	ex 435	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ↾_t ↾_t $/\$
20		simprrr 773	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ↾_t $/\$ $/\$
21		ffn 5746	. . . . . . . . . . . . . . . . . . 19
22	21	adantr 466	. . . . . . . . . . . . . . . . . 18 $/\$
23		restsspw 15329	. . . . . . . . . . . . . . . . . . . 20 ↾_t
24	23	sseli 3460	. . . . . . . . . . . . . . . . . . 19 ↾_t
25	24	elpwid 3991	. . . . . . . . . . . . . . . . . 18 ↾_t
26		simpl 458	. . . . . . . . . . . . . . . . . 18 $/\$
27		fnfvima 6158	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
28	22, 25, 26, 27	syl3an 1306	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ↾_t $/\$ $/\$
29	28	3expb 1206	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ↾_t $/\$ $/\$
30	20, 29	sseldd 3465	. . . . . . . . . . . . . . 15 $/\$ $/\$ ↾_t $/\$ $/\$
31	30	rexlimdvaa 2915	. . . . . . . . . . . . . 14 $/\$ ↾_t $/\$
32	31	ad3antrrr 734	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ↾_t ↾_t $/\$
33	19, 32	impbid 193	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ ↾_t ↾_t $/\$
34	33	pm5.32da 645	. . . . . . . . . . 11 $/\$ $/\$ $/\$ ↾_t $/\$ ↾_t $/\$ ↾_t $/\$
35		r19.42v 2980	. . . . . . . . . . 11 ↾_t ↾_t $/\$ $/\$ ↾_t $/\$ ↾_t $/\$
36	34, 35	syl6bbr 266	. . . . . . . . . 10 $/\$ $/\$ $/\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$
37	36	orbi1d 707	. . . . . . . . 9 $/\$ $/\$ $/\$ ↾_t $/\$ $\/$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ $\/$ ↾_t $/\$
38	9, 37	syl5bb 260	. . . . . . . 8 $/\$ $/\$ $/\$ ↾_t ↾_t $/\$ $/\$ $\/$ ↾_t $/\$
39	38	rabbidva 3070	. . . . . . 7 $/\$ $/\$ ↾_t ↾_t $/\$ $/\$ $\/$ ↾_t $/\$
40		eqid 2422	. . . . . . . 8
41	40	mptpreima 5347	. . . . . . 7
42		unrab 3744	. . . . . . 7 ↾_t ↾_t $/\$ $/\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ $\/$ ↾_t $/\$
43	39, 41, 42	3eqtr4g 2488	. . . . . 6 $/\$ $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
44	5, 43	eqtrd 2463	. . . . 5 $/\$ $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
45	44	3adantl3 1163	. . . 4 $/\$ $/\$ $\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
46		incom 3655	. . . . . . . . 9 ↾_t $/\$ ↾_t ↾_t ↾_t $/\$
47		dfin4 3713	. . . . . . . . 9 ↾_t $/\$ ↾_t ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
48		inrab 3745	. . . . . . . . . . . 12 ↾_t $/\$ ↾_t $/\$ $/\$
49	48	a1i 11	. . . . . . . . . . 11 ↾_t ↾_t $/\$ ↾_t $/\$ $/\$
50	49	iuneq2i 4318	. . . . . . . . . 10 ↾_t ↾_t $/\$ ↾_t ↾_t $/\$ $/\$
51		iunin2 4363	. . . . . . . . . 10 ↾_t ↾_t $/\$ ↾_t ↾_t $/\$
52		iunrab 4346	. . . . . . . . . 10 ↾_t ↾_t $/\$ $/\$ ↾_t ↾_t $/\$ $/\$
53	50, 51, 52	3eqtr3i 2459	. . . . . . . . 9 ↾_t ↾_t $/\$ ↾_t ↾_t $/\$ $/\$
54	46, 47, 53	3eqtr3i 2459	. . . . . . . 8 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$
55		eqeq2 2437	. . . . . . . . . . . . 13 $/\$ $/\$
56		eqeq2 2437	. . . . . . . . . . . . 13 $/\$ $/\$
57		simprrl 772	. . . . . . . . . . . . . . . 16 ↾_t $/\$ $/\$ $/\$ $/\$
58	25	adantr 466	. . . . . . . . . . . . . . . . . 18 ↾_t $/\$
59	58	sselda 3464	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ $/\$
60		pm3.22 450	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
61	60	adantll 718	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ $/\$ $/\$
62	59, 61	jca 534	. . . . . . . . . . . . . . . 16 ↾_t $/\$ $/\$ $/\$ $/\$
63	57, 62	impbida 840	. . . . . . . . . . . . . . 15 ↾_t $/\$ $/\$ $/\$
64	63	abbidv 2553	. . . . . . . . . . . . . 14 ↾_t $/\$ $/\$ $/\$
65		df-rab 2780	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
66		cvjust 2416	. . . . . . . . . . . . . 14
67	64, 65, 66	3eqtr4g 2488	. . . . . . . . . . . . 13 ↾_t $/\$ $/\$
68		simpr 462	. . . . . . . . . . . . . . . . 17 $/\$
69	68	con3i 140	. . . . . . . . . . . . . . . 16 $/\$
70	69	ralrimivw 2837	. . . . . . . . . . . . . . 15 $/\$
71		rabeq0 3784	. . . . . . . . . . . . . . 15 $/\$ $/\$
72	70, 71	sylibr 215	. . . . . . . . . . . . . 14 $/\$
73	72	adantl 467	. . . . . . . . . . . . 13 ↾_t $/\$ $/\$
74	55, 56, 67, 73	ifbothda 3946	. . . . . . . . . . . 12 ↾_t $/\$
75	74	iuneq2i 4318	. . . . . . . . . . 11 ↾_t $/\$ ↾_t
76		retop 21780	. . . . . . . . . . . . . 14
77		resttop 20174	. . . . . . . . . . . . . 14 $/\$ ↾_t
78	76, 77	mpan 674	. . . . . . . . . . . . 13 ↾_t
79		0opn 19932	. . . . . . . . . . . . . . . 16 ↾_t ↾_t
80	78, 79	syl 17	. . . . . . . . . . . . . . 15 ↾_t
81		ifcl 3953	. . . . . . . . . . . . . . . 16 ↾_t $/\$ ↾_t ↾_t
82	81	ancoms 454	. . . . . . . . . . . . . . 15 ↾_t $/\$ ↾_t ↾_t
83	80, 82	sylan 473	. . . . . . . . . . . . . 14 $/\$ ↾_t ↾_t
84	83	ralrimiva 2836	. . . . . . . . . . . . 13 ↾_t ↾_t
85		iunopn 19926	. . . . . . . . . . . . 13 ↾_t $/\$ ↾_t ↾_t ↾_t ↾_t
86	78, 84, 85	syl2anc 665	. . . . . . . . . . . 12 ↾_t ↾_t
87		eqid 2422	. . . . . . . . . . . . 13 ↾_t ↾_t
88	87	subopnmbl 22560	. . . . . . . . . . . 12 $/\$ ↾_t ↾_t ↾_t
89	86, 88	mpdan 672	. . . . . . . . . . 11 ↾_t
90	75, 89	syl5eqel 2511	. . . . . . . . . 10 ↾_t $/\$
91	90	adantr 466	. . . . . . . . 9 $/\$ $\$ ↾_t ↾_t $/\$
92		difss 3592	. . . . . . . . . . . . 13 ↾_t $/\$ $\$ ↾_t ↾_t $/\$
93		ssrab2 3546	. . . . . . . . . . . . . . 15 $/\$
94	93	rgenw 2783	. . . . . . . . . . . . . 14 ↾_t $/\$
95		iunss 4340	. . . . . . . . . . . . . 14 ↾_t $/\$ ↾_t $/\$
96	94, 95	mpbir 212	. . . . . . . . . . . . 13 ↾_t $/\$
97	92, 96	sstri 3473	. . . . . . . . . . . 12 ↾_t $/\$ $\$ ↾_t
98		mblss 22483	. . . . . . . . . . . 12
99	97, 98	syl5ss 3475	. . . . . . . . . . 11 ↾_t $/\$ $\$ ↾_t
100	99	adantr 466	. . . . . . . . . 10 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
101		ssdif 3600	. . . . . . . . . . . . . 14 ↾_t $/\$ ↾_t $/\$ $\$ ↾_t $\$ ↾_t
102	96, 101	ax-mp 5	. . . . . . . . . . . . 13 ↾_t $/\$ $\$ ↾_t $\$ ↾_t
103		ovex 6333	. . . . . . . . . . . . . . . . . . . . 21
104	103	rabex 4575	. . . . . . . . . . . . . . . . . . . 20 ↾_t $/\$
105		eqid 2422	. . . . . . . . . . . . . . . . . . . 20 ↾_t $/\$ ↾_t $/\$
106	104, 105	fnmpti 5724	. . . . . . . . . . . . . . . . . . 19 ↾_t $/\$
107		retopon 21782	. . . . . . . . . . . . . . . . . . . . . 22 TopOn
108		resttopon 20175	. . . . . . . . . . . . . . . . . . . . . 22 TopOn $/\$ ↾_t TopOn
109	107, 98, 108	sylancr 667	. . . . . . . . . . . . . . . . . . . . 21 ↾_t TopOn
110		cnpfval 20248	. . . . . . . . . . . . . . . . . . . . 21 ↾_t TopOn $/\$ TopOn ↾_t ↾_t $/\$
111	109, 107, 110	sylancl 666	. . . . . . . . . . . . . . . . . . . 20 ↾_t ↾_t $/\$
112	111	fneq1d 5684	. . . . . . . . . . . . . . . . . . 19 ↾_t ↾_t $/\$
113	106, 112	mpbiri 236	. . . . . . . . . . . . . . . . . 18 ↾_t
114		elpreima 6017	. . . . . . . . . . . . . . . . . 18 ↾_t ↾_t $/\$ ↾_t
115	113, 114	syl 17	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ ↾_t
116		rele 4982	. . . . . . . . . . . . . . . . . . . 20
117		elrelimasn 5211	. . . . . . . . . . . . . . . . . . . 20 ↾_t ↾_t
118	116, 117	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ↾_t ↾_t
119		fvex 5891	. . . . . . . . . . . . . . . . . . . 20 ↾_t
120	119	epelc 4766	. . . . . . . . . . . . . . . . . . 19 ↾_t ↾_t
121	118, 120	bitr2i 253	. . . . . . . . . . . . . . . . . 18 ↾_t ↾_t
122	121	anbi2i 698	. . . . . . . . . . . . . . . . 17 $/\$ ↾_t $/\$ ↾_t
123	115, 122	syl6rbbr 267	. . . . . . . . . . . . . . . 16 $/\$ ↾_t ↾_t
124	123	abbidv 2553	. . . . . . . . . . . . . . 15 $/\$ ↾_t ↾_t
125		df-rab 2780	. . . . . . . . . . . . . . 15 ↾_t $/\$ ↾_t
126		imaco 5359	. . . . . . . . . . . . . . . 16 ↾_t ↾_t
127		abid2 2558	. . . . . . . . . . . . . . . 16 ↾_t ↾_t
128	126, 127	eqtr4i 2454	. . . . . . . . . . . . . . 15 ↾_t ↾_t
129	124, 125, 128	3eqtr4g 2488	. . . . . . . . . . . . . 14 ↾_t ↾_t
130	129	difeq2d 3583	. . . . . . . . . . . . 13 $\$ ↾_t $\$ ↾_t
131	102, 130	syl5sseq 3512	. . . . . . . . . . . 12 ↾_t $/\$ $\$ ↾_t $\$ ↾_t
132		difss 3592	. . . . . . . . . . . . 13 $\$ ↾_t
133	132, 98	syl5ss 3475	. . . . . . . . . . . 12 $\$ ↾_t
134	131, 133	jca 534	. . . . . . . . . . 11 ↾_t $/\$ $\$ ↾_t $\$ ↾_t $/\$ $\$ ↾_t
135		ovolssnul 22438	. . . . . . . . . . . 12 ↾_t $/\$ $\$ ↾_t $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
136	135	3expa 1205	. . . . . . . . . . 11 ↾_t $/\$ $\$ ↾_t $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
137	134, 136	sylan 473	. . . . . . . . . 10 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
138		nulmbl 22487	. . . . . . . . . 10 ↾_t $/\$ $\$ ↾_t $/\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
139	100, 137, 138	syl2anc 665	. . . . . . . . 9 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
140		difmbl 22494	. . . . . . . . 9 ↾_t $/\$ $/\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
141	91, 139, 140	syl2anc 665	. . . . . . . 8 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
142	54, 141	syl5eqelr 2512	. . . . . . 7 $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$
143		ssrab2 3546	. . . . . . . . . 10 ↾_t $/\$
144	143, 98	syl5ss 3475	. . . . . . . . 9 ↾_t $/\$
145	144	adantr 466	. . . . . . . 8 $/\$ $\$ ↾_t ↾_t $/\$
146	126	eleq2i 2499	. . . . . . . . . . . . . . . 16 ↾_t ↾_t
147		ibar 506	. . . . . . . . . . . . . . . . . 18 ↾_t $/\$ ↾_t
148	121, 147	syl5rbb 261	. . . . . . . . . . . . . . . . 17 $/\$ ↾_t ↾_t
149	115, 148	sylan9bb 704	. . . . . . . . . . . . . . . 16 $/\$ ↾_t ↾_t
150	146, 149	syl5rbb 261	. . . . . . . . . . . . . . 15 $/\$ ↾_t ↾_t
151	150	notbid 295	. . . . . . . . . . . . . 14 $/\$ ↾_t ↾_t
152	151	biimpd 210	. . . . . . . . . . . . 13 $/\$ ↾_t ↾_t
153	152	adantrd 469	. . . . . . . . . . . 12 $/\$ ↾_t $/\$ ↾_t
154	153	ss2rabdv 3542	. . . . . . . . . . 11 ↾_t $/\$ ↾_t
155		dfdif2 3445	. . . . . . . . . . 11 $\$ ↾_t ↾_t
156	154, 155	syl6sseqr 3511	. . . . . . . . . 10 ↾_t $/\$ $\$ ↾_t
157	156, 133	jca 534	. . . . . . . . 9 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
158		ovolssnul 22438	. . . . . . . . . 10 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$
159	158	3expa 1205	. . . . . . . . 9 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$
160	157, 159	sylan 473	. . . . . . . 8 $/\$ $\$ ↾_t ↾_t $/\$
161		nulmbl 22487	. . . . . . . 8 ↾_t $/\$ $/\$ ↾_t $/\$ ↾_t $/\$
162	145, 160, 161	syl2anc 665	. . . . . . 7 $/\$ $\$ ↾_t ↾_t $/\$
163		unmbl 22489	. . . . . . 7 ↾_t ↾_t $/\$ $/\$ $/\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
164	142, 162, 163	syl2anc 665	. . . . . 6 $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
165	164	3adant1 1023	. . . . 5 $/\$ $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
166	165	adantr 466	. . . 4 $/\$ $/\$ $\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
167	45, 166	eqeltrd 2507	. . 3 $/\$ $/\$ $\$ ↾_t $/\$
168	167	ralrimiva 2836	. 2 $/\$ $/\$ $\$ ↾_t
169		ismbf 22584	. . 3 MblFn
170	169	3ad2ant1 1026	. 2 $/\$ $/\$ $\$ ↾_t MblFn
171	168, 170	mpbird 235	1 $/\$ $/\$ $\$ ↾_t MblFn

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $\/$ wo 369 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1872

cab 2407

wral 2771

wrex 2772

crab 2775 $\$ cdif 3433

cun 3434

cin 3435

wss 3436

c0 3761

cif 3911

cpw 3981

csn 3998

ciun 4299 class class class wbr 4423

cmpt 4482

cep 4762

ccnv 4852

cdm 4853

crn 4854

cima 4856

ccom 4857

wrel 4858

wfn 5596

wf 5597

cfv 5601 (class class class)co 6305

cmap 7483

cr 9545

cc0 9546

cioo 11642 ↾_t crest 15318

ctg 15335

ctop 19915 TopOnctopon 19916

ctb 19918

ccnp 20239

covol 22411

cvol 22413 MblFncmbf 22570

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2057 ax-ext 2401 ax-rep 4536 ax-sep 4546 ax-nul 4555 ax-pow 4602 ax-pr 4660 ax-un 6597 ax-inf2 8155 ax-cnex 9602 ax-resscn 9603 ax-1cn 9604 ax-icn 9605 ax-addcl 9606 ax-addrcl 9607 ax-mulcl 9608 ax-mulrcl 9609 ax-mulcom 9610 ax-addass 9611 ax-mulass 9612 ax-distr 9613 ax-i2m1 9614 ax-1ne0 9615 ax-1rid 9616 ax-rnegex 9617 ax-rrecex 9618 ax-cnre 9619 ax-pre-lttri 9620 ax-pre-lttrn 9621 ax-pre-ltadd 9622 ax-pre-mulgt0 9623 ax-pre-sup 9624

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2273 df-mo 2274 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2568 df-ne 2616 df-nel 2617 df-ral 2776 df-rex 2777 df-reu 2778 df-rmo 2779 df-rab 2780 df-v 3082 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3912 df-pw 3983 df-sn 3999 df-pr 4001 df-tp 4003 df-op 4005 df-uni 4220 df-int 4256 df-iun 4301 df-disj 4395 df-br 4424 df-opab 4483 df-mpt 4484 df-tr 4519 df-eprel 4764 df-id 4768 df-po 4774 df-so 4775 df-fr 4812 df-se 4813 df-we 4814 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-isom 5610 df-riota 6267 df-ov 6308 df-oprab 6309 df-mpt2 6310 df-of 6545 df-om 6707 df-1st 6807 df-2nd 6808 df-wrecs 7039 df-recs 7101 df-rdg 7139 df-1o 7193 df-2o 7194 df-oadd 7197 df-omul 7198 df-er 7374 df-map 7485 df-pm 7486 df-en 7581 df-dom 7582 df-sdom 7583 df-fin 7584 df-fi 7934 df-sup 7965 df-inf 7966 df-oi 8034 df-card 8381 df-acn 8384 df-cda 8605 df-pnf 9684 df-mnf 9685 df-xr 9686 df-ltxr 9687 df-le 9688 df-sub 9869 df-neg 9870 df-div 10277 df-nn 10617 df-2 10675 df-3 10676 df-4 10677 df-n0 10877 df-z 10945 df-uz 11167 df-q 11272 df-rp 11310 df-xneg 11416 df-xadd 11417 df-xmul 11418 df-ioo 11646 df-ico 11648 df-icc 11649 df-fz 11792 df-fzo 11923 df-fl 12034 df-seq 12220 df-exp 12279 df-hash 12522 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs 13299 df-clim 13551 df-rlim 13552 df-sum 13752 df-rest 15320 df-topgen 15341 df-psmet 18961 df-xmet 18962 df-met 18963 df-bl 18964 df-mopn 18965 df-top 19919 df-bases 19920 df-topon 19921 df-cnp 20242 df-cmp 20400 df-ovol 22414 df-vol 22416 df-mbf 22575

This theorem is referenced by: (None)

W3C validator