poimir - Mathbox for Brendan Leahy

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

Theorem poimir 31966

Description: Poincare-Miranda theorem. Theorem on [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0
poimir.i
poimir.r
poimir.1	↾_t
poimir.2	$/\$ $/\$ $/\$
poimir.3	$/\$ $/\$ $/\$

**Assertion**
Ref	Expression
poimir

Distinct variable groups:

Proof of Theorem poimir Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		poimir.0	. . 3
2		poimir.i	. . 3
3		poimir.r	. . 3
4		poimir.1	. . 3 ↾_t
5		poimir.2	. . 3 $/\$ $/\$ $/\$
6		poimir.3	. . 3 $/\$ $/\$ $/\$
7	1, 2, 3, 4, 5, 6	poimirlem32 31965	. 2 ↾_t
8		ovex 6316	. . . . . . . . . . . . . . . . . . . . . 22
9		retopon 21777	. . . . . . . . . . . . . . . . . . . . . 22 TopOn
10	3	pttoponconst 20605	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ TopOn TopOn
11	8, 9, 10	mp2an 677	. . . . . . . . . . . . . . . . . . . . 21 TopOn
12	11	topontopi 19939	. . . . . . . . . . . . . . . . . . . 20
13		reex 9627	. . . . . . . . . . . . . . . . . . . . . 22
14		unitssre 11776	. . . . . . . . . . . . . . . . . . . . . 22
15		mapss 7511	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
16	13, 14, 15	mp2an 677	. . . . . . . . . . . . . . . . . . . . 21
17	2, 16	eqsstri 3461	. . . . . . . . . . . . . . . . . . . 20
18	11	toponunii 19940	. . . . . . . . . . . . . . . . . . . . 21
19	18	restuni 20171	. . . . . . . . . . . . . . . . . . . 20 $/\$ ↾_t
20	12, 17, 19	mp2an 677	. . . . . . . . . . . . . . . . . . 19 ↾_t
21	20, 18	cnf 20255	. . . . . . . . . . . . . . . . . 18 ↾_t
22	4, 21	syl 17	. . . . . . . . . . . . . . . . 17
23	22	ffvelrnda 6020	. . . . . . . . . . . . . . . 16 $/\$
24		elmapi 7490	. . . . . . . . . . . . . . . 16
25	23, 24	syl 17	. . . . . . . . . . . . . . 15 $/\$
26	25	ffvelrnda 6020	. . . . . . . . . . . . . 14 $/\$ $/\$
27		recn 9626	. . . . . . . . . . . . . . . . 17
28		absrpcl 13344	. . . . . . . . . . . . . . . . . 18 $/\$
29	28	ex 436	. . . . . . . . . . . . . . . . 17
30	27, 29	syl 17	. . . . . . . . . . . . . . . 16
31		ltsubrp 11332	. . . . . . . . . . . . . . . . . 18 $/\$
32		ltaddrp 11333	. . . . . . . . . . . . . . . . . 18 $/\$
33	31, 32	jca 535	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
34	33	ex 436	. . . . . . . . . . . . . . . 16 $/\$
35	30, 34	syld 45	. . . . . . . . . . . . . . 15 $/\$
36	27	abscld 13491	. . . . . . . . . . . . . . . . . 18
37		resubcl 9935	. . . . . . . . . . . . . . . . . 18 $/\$
38	36, 37	mpdan 673	. . . . . . . . . . . . . . . . 17
39	38	rexrd 9687	. . . . . . . . . . . . . . . 16
40		readdcl 9619	. . . . . . . . . . . . . . . . . 18 $/\$
41	36, 40	mpdan 673	. . . . . . . . . . . . . . . . 17
42	41	rexrd 9687	. . . . . . . . . . . . . . . 16
43		rexr 9683	. . . . . . . . . . . . . . . 16
44		elioo5 11689	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
45	39, 42, 43, 44	syl3anc 1267	. . . . . . . . . . . . . . 15 $/\$
46	35, 45	sylibrd 238	. . . . . . . . . . . . . 14
47	26, 46	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
48		fveq2 5863	. . . . . . . . . . . . . . . . 17
49	48	fveq1d 5865	. . . . . . . . . . . . . . . 16
50		eqid 2450	. . . . . . . . . . . . . . . 16
51		fvex 5873	. . . . . . . . . . . . . . . 16
52	49, 50, 51	fvmpt 5946	. . . . . . . . . . . . . . 15
53	52	eleq1d 2512	. . . . . . . . . . . . . 14
54	53	ad2antlr 732	. . . . . . . . . . . . 13 $/\$ $/\$
55	47, 54	sylibrd 238	. . . . . . . . . . . 12 $/\$ $/\$
56		iooretop 21779	. . . . . . . . . . . . 13
57		resttopon 20170	. . . . . . . . . . . . . . . . . . . 20 TopOn $/\$ ↾_t TopOn
58	11, 17, 57	mp2an 677	. . . . . . . . . . . . . . . . . . 19 ↾_t TopOn
59	58	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ ↾_t TopOn
60	22	feqmptd 5916	. . . . . . . . . . . . . . . . . . . 20
61	60, 4	eqeltrrd 2529	. . . . . . . . . . . . . . . . . . 19 ↾_t
62	61	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$ ↾_t
63	11	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ TopOn
64		retop 21775	. . . . . . . . . . . . . . . . . . . . . 22
65	64	fconst6 5771	. . . . . . . . . . . . . . . . . . . . 21
66	18, 3	ptpjcn 20619	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
67	8, 65, 66	mp3an12 1353	. . . . . . . . . . . . . . . . . . . 20
68		fvex 5873	. . . . . . . . . . . . . . . . . . . . . 22
69	68	fvconst2 6118	. . . . . . . . . . . . . . . . . . . . 21
70	69	oveq2d 6304	. . . . . . . . . . . . . . . . . . . 20
71	67, 70	eleqtrd 2530	. . . . . . . . . . . . . . . . . . 19
72	71	adantl 468	. . . . . . . . . . . . . . . . . 18 $/\$
73		fveq1 5862	. . . . . . . . . . . . . . . . . 18
74	59, 62, 63, 72, 73	cnmpt11 20671	. . . . . . . . . . . . . . . . 17 $/\$ ↾_t
75	20	cncnpi 20287	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ ↾_t
76	74, 75	sylan 474	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ↾_t
77	76	an32s 812	. . . . . . . . . . . . . . 15 $/\$ $/\$ ↾_t
78		iscnp 20246	. . . . . . . . . . . . . . . . 17 ↾_t TopOn $/\$ TopOn $/\$ ↾_t $/\$ ↾_t $/\$
79	58, 9, 78	mp3an12 1353	. . . . . . . . . . . . . . . 16 ↾_t $/\$ ↾_t $/\$
80	79	ad2antlr 732	. . . . . . . . . . . . . . 15 $/\$ $/\$ ↾_t $/\$ ↾_t $/\$
81	77, 80	mpbid 214	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ ↾_t $/\$
82	81	simprd 465	. . . . . . . . . . . . 13 $/\$ $/\$ ↾_t $/\$
83		eleq2 2517	. . . . . . . . . . . . . . 15
84		sseq2 3453	. . . . . . . . . . . . . . . . 17
85	84	anbi2d 709	. . . . . . . . . . . . . . . 16 $/\$ $/\$
86	85	rexbidv 2900	. . . . . . . . . . . . . . 15 ↾_t $/\$ ↾_t $/\$
87	83, 86	imbi12d 322	. . . . . . . . . . . . . 14 ↾_t $/\$ ↾_t $/\$
88	87	rspcv 3145	. . . . . . . . . . . . 13 ↾_t $/\$ ↾_t $/\$
89	56, 82, 88	mpsyl 65	. . . . . . . . . . . 12 $/\$ $/\$ ↾_t $/\$
90	55, 89	syld 45	. . . . . . . . . . 11 $/\$ $/\$ ↾_t $/\$
91		0re 9640	. . . . . . . . . . . 12
92		letric 9731	. . . . . . . . . . . 12 $/\$ $\/$
93	26, 91, 92	sylancl 667	. . . . . . . . . . 11 $/\$ $/\$ $\/$
94	90, 93	jctird 547	. . . . . . . . . 10 $/\$ $/\$ ↾_t $/\$ $/\$ $\/$
95		r19.41v 2941	. . . . . . . . . . 11 ↾_t $/\$ $/\$ $\/$ ↾_t $/\$ $/\$ $\/$
96		anass 654	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$
97	96	rexbii 2888	. . . . . . . . . . 11 ↾_t $/\$ $/\$ $\/$ ↾_t $/\$ $/\$ $\/$
98	95, 97	bitr3i 255	. . . . . . . . . 10 ↾_t $/\$ $/\$ $\/$ ↾_t $/\$ $/\$ $\/$
99	94, 98	syl6ib 230	. . . . . . . . 9 $/\$ $/\$ ↾_t $/\$ $/\$ $\/$
100	58	topontopi 19939	. . . . . . . . . . . . 13 ↾_t
101	20	eltopss 19930	. . . . . . . . . . . . 13 ↾_t $/\$ ↾_t
102	100, 101	mpan 675	. . . . . . . . . . . 12 ↾_t
103		fvex 5873	. . . . . . . . . . . . . . . . . 18
104	103, 50	dmmpti 5705	. . . . . . . . . . . . . . . . 17
105	104	sseq2i 3456	. . . . . . . . . . . . . . . 16
106		funmpt 5617	. . . . . . . . . . . . . . . . 17
107		funimass4 5914	. . . . . . . . . . . . . . . . 17 $/\$
108	106, 107	mpan 675	. . . . . . . . . . . . . . . 16
109	105, 108	sylbir 217	. . . . . . . . . . . . . . 15
110		ssel2 3426	. . . . . . . . . . . . . . . . 17 $/\$
111		fveq2 5863	. . . . . . . . . . . . . . . . . . . . 21
112	111	fveq1d 5865	. . . . . . . . . . . . . . . . . . . 20
113		fvex 5873	. . . . . . . . . . . . . . . . . . . 20
114	112, 50, 113	fvmpt 5946	. . . . . . . . . . . . . . . . . . 19
115	114	eleq1d 2512	. . . . . . . . . . . . . . . . . 18
116		eliooord 11691	. . . . . . . . . . . . . . . . . 18 $/\$
117	115, 116	syl6bi 232	. . . . . . . . . . . . . . . . 17 $/\$
118	110, 117	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
119	118	ralimdva 2795	. . . . . . . . . . . . . . 15 $/\$
120	109, 119	sylbid 219	. . . . . . . . . . . . . 14 $/\$
121	120	adantl 468	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
122		absnid 13354	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
123	122	oveq2d 6304	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
124	27	negidd 9973	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
125	124	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
126	123, 125	eqtrd 2484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
127	26, 126	sylan 474	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
128	127	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
129	128	breq2d 4413	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
130	22	ffvelrnda 6020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
131		elmapi 7490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
132	130, 131	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
133	132	ffvelrnda 6020	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
134	133	an32s 812	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
135		0red 9641	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
136	134, 135	ltnled 9779	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
137	136	adantllr 724	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
138	137	adantlr 720	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
139	129, 138	bitrd 257	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
140	139	biimpd 211	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
141	110, 140	sylan2 477	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
142	141	anassrs 653	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
143	142	adantld 469	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
144	143	ralimdva 2795	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
145	144	an32s 812	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
146	145	impancom 442	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
147		absid 13352	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
148	147	oveq2d 6304	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
149	27	subidd 9971	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
150	149	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
151	148, 150	eqtrd 2484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
152	26, 151	sylan 474	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
153	152	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
154	153	breq1d 4411	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
155	135, 134	ltnled 9779	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
156	155	adantllr 724	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
157	156	adantlr 720	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
158	154, 157	bitrd 257	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
159	158	biimpd 211	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
160	110, 159	sylan2 477	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
161	160	anassrs 653	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
162	161	adantrd 470	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163	162	ralimdva 2795	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
164	163	an32s 812	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
165	164	impancom 442	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
166	146, 165	orim12d 848	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
167	166	expimpd 607	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
168	121, 167	syland 484	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
169	102, 168	sylan2 477	. . . . . . . . . . 11 $/\$ $/\$ $/\$ ↾_t $/\$ $\/$ $\/$
170	169	anim2d 568	. . . . . . . . . 10 $/\$ $/\$ $/\$ ↾_t $/\$ $/\$ $\/$ $/\$ $\/$
171	170	reximdva 2861	. . . . . . . . 9 $/\$ $/\$ ↾_t $/\$ $/\$ $\/$ ↾_t $/\$ $\/$
172	99, 171	syld 45	. . . . . . . 8 $/\$ $/\$ ↾_t $/\$ $\/$
173		ralnex 2833	. . . . . . . . . . . . . 14
174	173	rexbii 2888	. . . . . . . . . . . . 13
175		letsr 16466	. . . . . . . . . . . . . . 15
176	175	elexi 3054	. . . . . . . . . . . . . 14
177	176	cnvex 6737	. . . . . . . . . . . . . 14
178		breq 4403	. . . . . . . . . . . . . . . 16
179	178	notbid 296	. . . . . . . . . . . . . . 15
180	179	ralbidv 2826	. . . . . . . . . . . . . 14
181		breq 4403	. . . . . . . . . . . . . . . . 17
182		c0ex 9634	. . . . . . . . . . . . . . . . . 18
183	182, 113	brcnv 5016	. . . . . . . . . . . . . . . . 17
184	181, 183	syl6bb 265	. . . . . . . . . . . . . . . 16
185	184	notbid 296	. . . . . . . . . . . . . . 15
186	185	ralbidv 2826	. . . . . . . . . . . . . 14
187	176, 177, 180, 186	rexpr 4025	. . . . . . . . . . . . 13 $\/$
188		rexnal 2835	. . . . . . . . . . . . 13
189	174, 187, 188	3bitr3i 279	. . . . . . . . . . . 12 $\/$
190	189	anbi2i 699	. . . . . . . . . . 11 $/\$ $\/$ $/\$
191		annim 427	. . . . . . . . . . 11 $/\$
192	190, 191	bitri 253	. . . . . . . . . 10 $/\$ $\/$
193	192	rexbii 2888	. . . . . . . . 9 ↾_t $/\$ $\/$ ↾_t
194		rexnal 2835	. . . . . . . . 9 ↾_t ↾_t
195	193, 194	bitri 253	. . . . . . . 8 ↾_t $/\$ $\/$ ↾_t
196	172, 195	syl6ib 230	. . . . . . 7 $/\$ $/\$ ↾_t
197	196	necon4ad 2642	. . . . . 6 $/\$ $/\$ ↾_t
198	197	ralimdva 2795	. . . . 5 $/\$ ↾_t
199		ffn 5726	. . . . . 6
200	25, 199	syl 17	. . . . 5 $/\$
201	198, 200	jctild 546	. . . 4 $/\$ ↾_t $/\$
202		fconstfv 6124	. . . . 5 $/\$
203	182	fconst2 6119	. . . . 5
204	202, 203	bitr3i 255	. . . 4 $/\$
205	201, 204	syl6ib 230	. . 3 $/\$ ↾_t
206	205	reximdva 2861	. 2 ↾_t
207	7, 206	mpd 15	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371 $/\$ w3a 984

wceq 1443

wcel 1886

wne 2621

wral 2736

wrex 2737

cvv 3044

wss 3403

csn 3967

cpr 3969

cuni 4197 class class class wbr 4401

cmpt 4460

cxp 4831

ccnv 4832

cdm 4833

crn 4834

cima 4836

wfun 5575

wfn 5576

wf 5577

cfv 5581 (class class class)co 6288

cmap 7469

cc 9534

cr 9535

cc0 9536

c1 9537

caddc 9539

cxr 9671

clt 9672

cle 9673

cmin 9857

cneg 9858

cn 10606

crp 11299

cioo 11632

cicc 11635

cfz 11781

cabs 13290 ↾_t crest 15312

ctg 15329

cpt 15330

ctsr 16438

ctop 19910 TopOnctopon 19911

ccn 20233

ccnp 20234

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-rep 4514 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-inf2 8143 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613 ax-pre-sup 9614

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-fal 1449 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-uni 4198 df-int 4234 df-iun 4279 df-iin 4280 df-disj 4373 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-se 4793 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-isom 5590 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-of 6528 df-om 6690 df-1st 6790 df-2nd 6791 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-1o 7179 df-2o 7180 df-oadd 7183 df-omul 7184 df-er 7360 df-map 7471 df-pm 7472 df-ixp 7520 df-en 7567 df-dom 7568 df-sdom 7569 df-fin 7570 df-fi 7922 df-sup 7953 df-inf 7954 df-oi 8022 df-card 8370 df-acn 8373 df-cda 8595 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-div 10267 df-nn 10607 df-2 10665 df-3 10666 df-n0 10867 df-z 10935 df-uz 11157 df-q 11262 df-rp 11300 df-xneg 11406 df-xadd 11407 df-xmul 11408 df-ioo 11636 df-icc 11639 df-fz 11782 df-fzo 11913 df-fl 12025 df-seq 12211 df-exp 12270 df-fac 12457 df-bc 12485 df-hash 12513 df-cj 13155 df-re 13156 df-im 13157 df-sqrt 13291 df-abs 13292 df-clim 13545 df-sum 13746 df-dvds 14299 df-rest 15314 df-topgen 15335 df-pt 15336 df-ps 16439 df-tsr 16440 df-psmet 18955 df-xmet 18956 df-met 18957 df-bl 18958 df-mopn 18959 df-top 19914 df-bases 19915 df-topon 19916 df-cld 20027 df-ntr 20028 df-cls 20029 df-lp 20145 df-cn 20236 df-cnp 20237 df-t1 20323 df-haus 20324 df-cmp 20395 df-tx 20570 df-hmeo 20763 df-hmph 20764 df-ii 21902

This theorem is referenced by: broucube 31967

W3C validator