cnambfre - Mathbox for Brendan Leahy

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

Theorem cnambfre 32035

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 5945	. . . . . . . . 9
3	2	cnveqd 5032	. . . . . . . 8
4	3	imaeq1d 5189	. . . . . . 7
5	4	ad2antrr 737	. . . . . 6 $/\$ $/\$
6		exmid 421	. . . . . . . . . . 11 ↾_t $\/$ ↾_t
7	6	biantrur 513	. . . . . . . . . 10 ↾_t $\/$ ↾_t $/\$
8		andir 884	. . . . . . . . . 10 ↾_t $\/$ ↾_t $/\$ ↾_t $/\$ $\/$ ↾_t $/\$
9	7, 8	bitri 257	. . . . . . . . 9 ↾_t $/\$ $\/$ ↾_t $/\$
10		retopbas 21836	. . . . . . . . . . . . . . . . . 18
11		bastg 20036	. . . . . . . . . . . . . . . . . 18
12	10, 11	ax-mp 5	. . . . . . . . . . . . . . . . 17
13	12	sseli 3440	. . . . . . . . . . . . . . . 16
14	13	ad2antlr 738	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
15		cnpimaex 20327	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ $/\$ ↾_t $/\$
16	15	3com12 1219	. . . . . . . . . . . . . . . 16 $/\$ ↾_t $/\$ ↾_t $/\$
17	16	3expa 1215	. . . . . . . . . . . . . . 15 $/\$ ↾_t $/\$ ↾_t $/\$
18	14, 17	sylanl1 660	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ↾_t $/\$ ↾_t $/\$
19	18	ex 440	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ↾_t ↾_t $/\$
20		simprrr 780	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ↾_t $/\$ $/\$
21		ffn 5755	. . . . . . . . . . . . . . . . . . 19
22	21	adantr 471	. . . . . . . . . . . . . . . . . 18 $/\$
23		restsspw 15385	. . . . . . . . . . . . . . . . . . . 20 ↾_t
24	23	sseli 3440	. . . . . . . . . . . . . . . . . . 19 ↾_t
25	24	elpwid 3973	. . . . . . . . . . . . . . . . . 18 ↾_t
26		simpl 463	. . . . . . . . . . . . . . . . . 18 $/\$
27		fnfvima 6173	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
28	22, 25, 26, 27	syl3an 1318	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ↾_t $/\$ $/\$
29	28	3expb 1216	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ↾_t $/\$ $/\$
30	20, 29	sseldd 3445	. . . . . . . . . . . . . . 15 $/\$ $/\$ ↾_t $/\$ $/\$
31	30	rexlimdvaa 2892	. . . . . . . . . . . . . 14 $/\$ ↾_t $/\$
32	31	ad3antrrr 741	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ↾_t ↾_t $/\$
33	19, 32	impbid 195	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ ↾_t ↾_t $/\$
34	33	pm5.32da 651	. . . . . . . . . . 11 $/\$ $/\$ $/\$ ↾_t $/\$ ↾_t $/\$ ↾_t $/\$
35		r19.42v 2957	. . . . . . . . . . 11 ↾_t ↾_t $/\$ $/\$ ↾_t $/\$ ↾_t $/\$
36	34, 35	syl6bbr 271	. . . . . . . . . 10 $/\$ $/\$ $/\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$
37	36	orbi1d 714	. . . . . . . . 9 $/\$ $/\$ $/\$ ↾_t $/\$ $\/$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ $\/$ ↾_t $/\$
38	9, 37	syl5bb 265	. . . . . . . 8 $/\$ $/\$ $/\$ ↾_t ↾_t $/\$ $/\$ $\/$ ↾_t $/\$
39	38	rabbidva 3047	. . . . . . 7 $/\$ $/\$ ↾_t ↾_t $/\$ $/\$ $\/$ ↾_t $/\$
40		eqid 2462	. . . . . . . 8
41	40	mptpreima 5351	. . . . . . 7
42		unrab 3726	. . . . . . 7 ↾_t ↾_t $/\$ $/\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ $\/$ ↾_t $/\$
43	39, 41, 42	3eqtr4g 2521	. . . . . 6 $/\$ $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
44	5, 43	eqtrd 2496	. . . . 5 $/\$ $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
45	44	3adantl3 1172	. . . 4 $/\$ $/\$ $\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
46		incom 3637	. . . . . . . . 9 ↾_t $/\$ ↾_t ↾_t ↾_t $/\$
47		dfin4 3695	. . . . . . . . 9 ↾_t $/\$ ↾_t ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
48		inrab 3727	. . . . . . . . . . . 12 ↾_t $/\$ ↾_t $/\$ $/\$
49	48	a1i 11	. . . . . . . . . . 11 ↾_t ↾_t $/\$ ↾_t $/\$ $/\$
50	49	iuneq2i 4311	. . . . . . . . . 10 ↾_t ↾_t $/\$ ↾_t ↾_t $/\$ $/\$
51		iunin2 4356	. . . . . . . . . 10 ↾_t ↾_t $/\$ ↾_t ↾_t $/\$
52		iunrab 4339	. . . . . . . . . 10 ↾_t ↾_t $/\$ $/\$ ↾_t ↾_t $/\$ $/\$
53	50, 51, 52	3eqtr3i 2492	. . . . . . . . 9 ↾_t ↾_t $/\$ ↾_t ↾_t $/\$ $/\$
54	46, 47, 53	3eqtr3i 2492	. . . . . . . 8 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$
55		eqeq2 2473	. . . . . . . . . . . . 13 $/\$ $/\$
56		eqeq2 2473	. . . . . . . . . . . . 13 $/\$ $/\$
57		simprrl 779	. . . . . . . . . . . . . . . 16 ↾_t $/\$ $/\$ $/\$ $/\$
58	25	adantr 471	. . . . . . . . . . . . . . . . . 18 ↾_t $/\$
59	58	sselda 3444	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ $/\$
60		pm3.22 455	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
61	60	adantll 725	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ $/\$ $/\$
62	59, 61	jca 539	. . . . . . . . . . . . . . . 16 ↾_t $/\$ $/\$ $/\$ $/\$
63	57, 62	impbida 848	. . . . . . . . . . . . . . 15 ↾_t $/\$ $/\$ $/\$
64	63	abbidv 2580	. . . . . . . . . . . . . 14 ↾_t $/\$ $/\$ $/\$
65		df-rab 2758	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
66		cvjust 2457	. . . . . . . . . . . . . 14
67	64, 65, 66	3eqtr4g 2521	. . . . . . . . . . . . 13 ↾_t $/\$ $/\$
68		simpr 467	. . . . . . . . . . . . . . . . 17 $/\$
69	68	con3i 142	. . . . . . . . . . . . . . . 16 $/\$
70	69	ralrimivw 2815	. . . . . . . . . . . . . . 15 $/\$
71		rabeq0 3766	. . . . . . . . . . . . . . 15 $/\$ $/\$
72	70, 71	sylibr 217	. . . . . . . . . . . . . 14 $/\$
73	72	adantl 472	. . . . . . . . . . . . 13 ↾_t $/\$ $/\$
74	55, 56, 67, 73	ifbothda 3928	. . . . . . . . . . . 12 ↾_t $/\$
75	74	iuneq2i 4311	. . . . . . . . . . 11 ↾_t $/\$ ↾_t
76		retop 21837	. . . . . . . . . . . . . 14
77		resttop 20231	. . . . . . . . . . . . . 14 $/\$ ↾_t
78	76, 77	mpan 681	. . . . . . . . . . . . 13 ↾_t
79		0opn 19989	. . . . . . . . . . . . . . . 16 ↾_t ↾_t
80	78, 79	syl 17	. . . . . . . . . . . . . . 15 ↾_t
81		ifcl 3935	. . . . . . . . . . . . . . . 16 ↾_t $/\$ ↾_t ↾_t
82	81	ancoms 459	. . . . . . . . . . . . . . 15 ↾_t $/\$ ↾_t ↾_t
83	80, 82	sylan 478	. . . . . . . . . . . . . 14 $/\$ ↾_t ↾_t
84	83	ralrimiva 2814	. . . . . . . . . . . . 13 ↾_t ↾_t
85		iunopn 19983	. . . . . . . . . . . . 13 ↾_t $/\$ ↾_t ↾_t ↾_t ↾_t
86	78, 84, 85	syl2anc 671	. . . . . . . . . . . 12 ↾_t ↾_t
87		eqid 2462	. . . . . . . . . . . . 13 ↾_t ↾_t
88	87	subopnmbl 22618	. . . . . . . . . . . 12 $/\$ ↾_t ↾_t ↾_t
89	86, 88	mpdan 679	. . . . . . . . . . 11 ↾_t
90	75, 89	syl5eqel 2544	. . . . . . . . . 10 ↾_t $/\$
91	90	adantr 471	. . . . . . . . 9 $/\$ $\$ ↾_t ↾_t $/\$
92		difss 3572	. . . . . . . . . . . . 13 ↾_t $/\$ $\$ ↾_t ↾_t $/\$
93		ssrab2 3526	. . . . . . . . . . . . . . 15 $/\$
94	93	rgenw 2761	. . . . . . . . . . . . . 14 ↾_t $/\$
95		iunss 4333	. . . . . . . . . . . . . 14 ↾_t $/\$ ↾_t $/\$
96	94, 95	mpbir 214	. . . . . . . . . . . . 13 ↾_t $/\$
97	92, 96	sstri 3453	. . . . . . . . . . . 12 ↾_t $/\$ $\$ ↾_t
98		mblss 22540	. . . . . . . . . . . 12
99	97, 98	syl5ss 3455	. . . . . . . . . . 11 ↾_t $/\$ $\$ ↾_t
100	99	adantr 471	. . . . . . . . . 10 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
101		ssdif 3580	. . . . . . . . . . . . . 14 ↾_t $/\$ ↾_t $/\$ $\$ ↾_t $\$ ↾_t
102	96, 101	ax-mp 5	. . . . . . . . . . . . 13 ↾_t $/\$ $\$ ↾_t $\$ ↾_t
103		ovex 6348	. . . . . . . . . . . . . . . . . . . . 21
104	103	rabex 4571	. . . . . . . . . . . . . . . . . . . 20 ↾_t $/\$
105		eqid 2462	. . . . . . . . . . . . . . . . . . . 20 ↾_t $/\$ ↾_t $/\$
106	104, 105	fnmpti 5732	. . . . . . . . . . . . . . . . . . 19 ↾_t $/\$
107		retopon 21839	. . . . . . . . . . . . . . . . . . . . . 22 TopOn
108		resttopon 20232	. . . . . . . . . . . . . . . . . . . . . 22 TopOn $/\$ ↾_t TopOn
109	107, 98, 108	sylancr 674	. . . . . . . . . . . . . . . . . . . . 21 ↾_t TopOn
110		cnpfval 20305	. . . . . . . . . . . . . . . . . . . . 21 ↾_t TopOn $/\$ TopOn ↾_t ↾_t $/\$
111	109, 107, 110	sylancl 673	. . . . . . . . . . . . . . . . . . . 20 ↾_t ↾_t $/\$
112	111	fneq1d 5692	. . . . . . . . . . . . . . . . . . 19 ↾_t ↾_t $/\$
113	106, 112	mpbiri 241	. . . . . . . . . . . . . . . . . 18 ↾_t
114		elpreima 6030	. . . . . . . . . . . . . . . . . 18 ↾_t ↾_t $/\$ ↾_t
115	113, 114	syl 17	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ ↾_t
116		rele 4985	. . . . . . . . . . . . . . . . . . . 20
117		elrelimasn 5214	. . . . . . . . . . . . . . . . . . . 20 ↾_t ↾_t
118	116, 117	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ↾_t ↾_t
119		fvex 5902	. . . . . . . . . . . . . . . . . . . 20 ↾_t
120	119	epelc 4769	. . . . . . . . . . . . . . . . . . 19 ↾_t ↾_t
121	118, 120	bitr2i 258	. . . . . . . . . . . . . . . . . 18 ↾_t ↾_t
122	121	anbi2i 705	. . . . . . . . . . . . . . . . 17 $/\$ ↾_t $/\$ ↾_t
123	115, 122	syl6rbbr 272	. . . . . . . . . . . . . . . 16 $/\$ ↾_t ↾_t
124	123	abbidv 2580	. . . . . . . . . . . . . . 15 $/\$ ↾_t ↾_t
125		df-rab 2758	. . . . . . . . . . . . . . 15 ↾_t $/\$ ↾_t
126		imaco 5363	. . . . . . . . . . . . . . . 16 ↾_t ↾_t
127		abid2 2584	. . . . . . . . . . . . . . . 16 ↾_t ↾_t
128	126, 127	eqtr4i 2487	. . . . . . . . . . . . . . 15 ↾_t ↾_t
129	124, 125, 128	3eqtr4g 2521	. . . . . . . . . . . . . 14 ↾_t ↾_t
130	129	difeq2d 3563	. . . . . . . . . . . . 13 $\$ ↾_t $\$ ↾_t
131	102, 130	syl5sseq 3492	. . . . . . . . . . . 12 ↾_t $/\$ $\$ ↾_t $\$ ↾_t
132		difss 3572	. . . . . . . . . . . . 13 $\$ ↾_t
133	132, 98	syl5ss 3455	. . . . . . . . . . . 12 $\$ ↾_t
134	131, 133	jca 539	. . . . . . . . . . 11 ↾_t $/\$ $\$ ↾_t $\$ ↾_t $/\$ $\$ ↾_t
135		ovolssnul 22495	. . . . . . . . . . . 12 ↾_t $/\$ $\$ ↾_t $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
136	135	3expa 1215	. . . . . . . . . . 11 ↾_t $/\$ $\$ ↾_t $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
137	134, 136	sylan 478	. . . . . . . . . 10 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
138		nulmbl 22544	. . . . . . . . . 10 ↾_t $/\$ $\$ ↾_t $/\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
139	100, 137, 138	syl2anc 671	. . . . . . . . 9 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t
140		difmbl 22552	. . . . . . . . 9 ↾_t $/\$ $/\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
141	91, 139, 140	syl2anc 671	. . . . . . . 8 $/\$ $\$ ↾_t ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
142	54, 141	syl5eqelr 2545	. . . . . . 7 $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$
143		ssrab2 3526	. . . . . . . . . 10 ↾_t $/\$
144	143, 98	syl5ss 3455	. . . . . . . . 9 ↾_t $/\$
145	144	adantr 471	. . . . . . . 8 $/\$ $\$ ↾_t ↾_t $/\$
146	126	eleq2i 2532	. . . . . . . . . . . . . . . 16 ↾_t ↾_t
147		ibar 511	. . . . . . . . . . . . . . . . . 18 ↾_t $/\$ ↾_t
148	121, 147	syl5rbb 266	. . . . . . . . . . . . . . . . 17 $/\$ ↾_t ↾_t
149	115, 148	sylan9bb 711	. . . . . . . . . . . . . . . 16 $/\$ ↾_t ↾_t
150	146, 149	syl5rbb 266	. . . . . . . . . . . . . . 15 $/\$ ↾_t ↾_t
151	150	notbid 300	. . . . . . . . . . . . . 14 $/\$ ↾_t ↾_t
152	151	biimpd 212	. . . . . . . . . . . . 13 $/\$ ↾_t ↾_t
153	152	adantrd 474	. . . . . . . . . . . 12 $/\$ ↾_t $/\$ ↾_t
154	153	ss2rabdv 3522	. . . . . . . . . . 11 ↾_t $/\$ ↾_t
155		dfdif2 3425	. . . . . . . . . . 11 $\$ ↾_t ↾_t
156	154, 155	syl6sseqr 3491	. . . . . . . . . 10 ↾_t $/\$ $\$ ↾_t
157	156, 133	jca 539	. . . . . . . . 9 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t
158		ovolssnul 22495	. . . . . . . . . 10 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$
159	158	3expa 1215	. . . . . . . . 9 ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t $/\$ $\$ ↾_t ↾_t $/\$
160	157, 159	sylan 478	. . . . . . . 8 $/\$ $\$ ↾_t ↾_t $/\$
161		nulmbl 22544	. . . . . . . 8 ↾_t $/\$ $/\$ ↾_t $/\$ ↾_t $/\$
162	145, 160, 161	syl2anc 671	. . . . . . 7 $/\$ $\$ ↾_t ↾_t $/\$
163		unmbl 22546	. . . . . . 7 ↾_t ↾_t $/\$ $/\$ $/\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
164	142, 162, 163	syl2anc 671	. . . . . 6 $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
165	164	3adant1 1032	. . . . 5 $/\$ $/\$ $\$ ↾_t ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
166	165	adantr 471	. . . 4 $/\$ $/\$ $\$ ↾_t $/\$ ↾_t ↾_t $/\$ $/\$ ↾_t $/\$
167	45, 166	eqeltrd 2540	. . 3 $/\$ $/\$ $\$ ↾_t $/\$
168	167	ralrimiva 2814	. 2 $/\$ $/\$ $\$ ↾_t
169		ismbf 22642	. . 3 MblFn
170	169	3ad2ant1 1035	. 2 $/\$ $/\$ $\$ ↾_t MblFn
171	168, 170	mpbird 240	1 $/\$ $/\$ $\$ ↾_t MblFn

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $\/$ wo 374 $/\$ wa 375 $/\$ w3a 991

wceq 1455

wcel 1898

cab 2448

wral 2749

wrex 2750

crab 2753 $\$ cdif 3413

cun 3414

cin 3415

wss 3416

c0 3743

cif 3893

cpw 3963

csn 3980

ciun 4292 class class class wbr 4418

cmpt 4477

cep 4765

ccnv 4855

cdm 4856

crn 4857

cima 4859

ccom 4860

wrel 4861

wfn 5600

wf 5601

cfv 5605 (class class class)co 6320

cmap 7503

cr 9569

cc0 9570

cioo 11669 ↾_t crest 15374

ctg 15391

ctop 19972 TopOnctopon 19973

ctb 19975

ccnp 20296

covol 22468

cvol 22470 MblFncmbf 22628

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-rep 4531 ax-sep 4541 ax-nul 4550 ax-pow 4598 ax-pr 4656 ax-un 6615 ax-inf2 8177 ax-cnex 9626 ax-resscn 9627 ax-1cn 9628 ax-icn 9629 ax-addcl 9630 ax-addrcl 9631 ax-mulcl 9632 ax-mulrcl 9633 ax-mulcom 9634 ax-addass 9635 ax-mulass 9636 ax-distr 9637 ax-i2m1 9638 ax-1ne0 9639 ax-1rid 9640 ax-rnegex 9641 ax-rrecex 9642 ax-cnre 9643 ax-pre-lttri 9644 ax-pre-lttrn 9645 ax-pre-ltadd 9646 ax-pre-mulgt0 9647 ax-pre-sup 9648

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1458 df-fal 1461 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-nel 2636 df-ral 2754 df-rex 2755 df-reu 2756 df-rmo 2757 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-tp 3985 df-op 3987 df-uni 4213 df-int 4249 df-iun 4294 df-disj 4390 df-br 4419 df-opab 4478 df-mpt 4479 df-tr 4514 df-eprel 4767 df-id 4771 df-po 4777 df-so 4778 df-fr 4815 df-se 4816 df-we 4817 df-xp 4862 df-rel 4863 df-cnv 4864 df-co 4865 df-dm 4866 df-rn 4867 df-res 4868 df-ima 4869 df-pred 5403 df-ord 5449 df-on 5450 df-lim 5451 df-suc 5452 df-iota 5569 df-fun 5607 df-fn 5608 df-f 5609 df-f1 5610 df-fo 5611 df-f1o 5612 df-fv 5613 df-isom 5614 df-riota 6282 df-ov 6323 df-oprab 6324 df-mpt2 6325 df-of 6563 df-om 6725 df-1st 6825 df-2nd 6826 df-wrecs 7059 df-recs 7121 df-rdg 7159 df-1o 7213 df-2o 7214 df-oadd 7217 df-omul 7218 df-er 7394 df-map 7505 df-pm 7506 df-en 7601 df-dom 7602 df-sdom 7603 df-fin 7604 df-fi 7956 df-sup 7987 df-inf 7988 df-oi 8056 df-card 8404 df-acn 8407 df-cda 8629 df-pnf 9708 df-mnf 9709 df-xr 9710 df-ltxr 9711 df-le 9712 df-sub 9893 df-neg 9894 df-div 10303 df-nn 10643 df-2 10701 df-3 10702 df-4 10703 df-n0 10904 df-z 10972 df-uz 11194 df-q 11299 df-rp 11337 df-xneg 11443 df-xadd 11444 df-xmul 11445 df-ioo 11673 df-ico 11675 df-icc 11676 df-fz 11820 df-fzo 11953 df-fl 12066 df-seq 12252 df-exp 12311 df-hash 12554 df-cj 13217 df-re 13218 df-im 13219 df-sqrt 13353 df-abs 13354 df-clim 13607 df-rlim 13608 df-sum 13808 df-rest 15376 df-topgen 15397 df-psmet 19017 df-xmet 19018 df-met 19019 df-bl 19020 df-mopn 19021 df-top 19976 df-bases 19977 df-topon 19978 df-cnp 20299 df-cmp 20457 df-ovol 22471 df-vol 22473 df-mbf 22633

This theorem is referenced by: (None)

W3C validator