poimir - Mathbox for Brendan Leahy

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

Theorem poimir 31881

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 31880	. 2 ↾_t
8		ovex 6325	. . . . . . . . . . . . . . . . . . . . . 22
9		retopon 21761	. . . . . . . . . . . . . . . . . . . . . 22 TopOn
10	3	pttoponconst 20589	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ TopOn TopOn
11	8, 9, 10	mp2an 676	. . . . . . . . . . . . . . . . . . . . 21 TopOn
12	11	topontopi 19923	. . . . . . . . . . . . . . . . . . . 20
13		reex 9626	. . . . . . . . . . . . . . . . . . . . . 22
14		unitssre 11773	. . . . . . . . . . . . . . . . . . . . . 22
15		mapss 7514	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
16	13, 14, 15	mp2an 676	. . . . . . . . . . . . . . . . . . . . 21
17	2, 16	eqsstri 3491	. . . . . . . . . . . . . . . . . . . 20
18	11	toponunii 19924	. . . . . . . . . . . . . . . . . . . . 21
19	18	restuni 20155	. . . . . . . . . . . . . . . . . . . 20 $/\$ ↾_t
20	12, 17, 19	mp2an 676	. . . . . . . . . . . . . . . . . . 19 ↾_t
21	20, 18	cnf 20239	. . . . . . . . . . . . . . . . . 18 ↾_t
22	4, 21	syl 17	. . . . . . . . . . . . . . . . 17
23	22	ffvelrnda 6029	. . . . . . . . . . . . . . . 16 $/\$
24		elmapi 7493	. . . . . . . . . . . . . . . 16
25	23, 24	syl 17	. . . . . . . . . . . . . . 15 $/\$
26	25	ffvelrnda 6029	. . . . . . . . . . . . . 14 $/\$ $/\$
27		recn 9625	. . . . . . . . . . . . . . . . 17
28		absrpcl 13330	. . . . . . . . . . . . . . . . . 18 $/\$
29	28	ex 435	. . . . . . . . . . . . . . . . 17
30	27, 29	syl 17	. . . . . . . . . . . . . . . 16
31		ltsubrp 11331	. . . . . . . . . . . . . . . . . 18 $/\$
32		ltaddrp 11332	. . . . . . . . . . . . . . . . . 18 $/\$
33	31, 32	jca 534	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
34	33	ex 435	. . . . . . . . . . . . . . . 16 $/\$
35	30, 34	syld 45	. . . . . . . . . . . . . . 15 $/\$
36	27	abscld 13476	. . . . . . . . . . . . . . . . . 18
37		resubcl 9934	. . . . . . . . . . . . . . . . . 18 $/\$
38	36, 37	mpdan 672	. . . . . . . . . . . . . . . . 17
39	38	rexrd 9686	. . . . . . . . . . . . . . . 16
40		readdcl 9618	. . . . . . . . . . . . . . . . . 18 $/\$
41	36, 40	mpdan 672	. . . . . . . . . . . . . . . . 17
42	41	rexrd 9686	. . . . . . . . . . . . . . . 16
43		rexr 9682	. . . . . . . . . . . . . . . 16
44		elioo5 11688	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
45	39, 42, 43, 44	syl3anc 1264	. . . . . . . . . . . . . . 15 $/\$
46	35, 45	sylibrd 237	. . . . . . . . . . . . . 14
47	26, 46	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
48		fveq2 5873	. . . . . . . . . . . . . . . . 17
49	48	fveq1d 5875	. . . . . . . . . . . . . . . 16
50		eqid 2420	. . . . . . . . . . . . . . . 16
51		fvex 5883	. . . . . . . . . . . . . . . 16
52	49, 50, 51	fvmpt 5956	. . . . . . . . . . . . . . 15
53	52	eleq1d 2489	. . . . . . . . . . . . . 14
54	53	ad2antlr 731	. . . . . . . . . . . . 13 $/\$ $/\$
55	47, 54	sylibrd 237	. . . . . . . . . . . 12 $/\$ $/\$
56		iooretop 21763	. . . . . . . . . . . . 13
57		resttopon 20154	. . . . . . . . . . . . . . . . . . . 20 TopOn $/\$ ↾_t TopOn
58	11, 17, 57	mp2an 676	. . . . . . . . . . . . . . . . . . 19 ↾_t TopOn
59	58	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ ↾_t TopOn
60	22	feqmptd 5926	. . . . . . . . . . . . . . . . . . . 20
61	60, 4	eqeltrrd 2509	. . . . . . . . . . . . . . . . . . 19 ↾_t
62	61	adantr 466	. . . . . . . . . . . . . . . . . 18 $/\$ ↾_t
63	11	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ TopOn
64		retop 21759	. . . . . . . . . . . . . . . . . . . . . 22
65	64	fconst6 5782	. . . . . . . . . . . . . . . . . . . . 21
66	18, 3	ptpjcn 20603	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
67	8, 65, 66	mp3an12 1350	. . . . . . . . . . . . . . . . . . . 20
68		fvex 5883	. . . . . . . . . . . . . . . . . . . . . 22
69	68	fvconst2 6127	. . . . . . . . . . . . . . . . . . . . 21
70	69	oveq2d 6313	. . . . . . . . . . . . . . . . . . . 20
71	67, 70	eleqtrd 2510	. . . . . . . . . . . . . . . . . . 19
72	71	adantl 467	. . . . . . . . . . . . . . . . . 18 $/\$
73		fveq1 5872	. . . . . . . . . . . . . . . . . 18
74	59, 62, 63, 72, 73	cnmpt11 20655	. . . . . . . . . . . . . . . . 17 $/\$ ↾_t
75	20	cncnpi 20271	. . . . . . . . . . . . . . . . 17 ↾_t $/\$ ↾_t
76	74, 75	sylan 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ↾_t
77	76	an32s 811	. . . . . . . . . . . . . . 15 $/\$ $/\$ ↾_t
78		iscnp 20230	. . . . . . . . . . . . . . . . 17 ↾_t TopOn $/\$ TopOn $/\$ ↾_t $/\$ ↾_t $/\$
79	58, 9, 78	mp3an12 1350	. . . . . . . . . . . . . . . 16 ↾_t $/\$ ↾_t $/\$
80	79	ad2antlr 731	. . . . . . . . . . . . . . 15 $/\$ $/\$ ↾_t $/\$ ↾_t $/\$
81	77, 80	mpbid 213	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ ↾_t $/\$
82	81	simprd 464	. . . . . . . . . . . . 13 $/\$ $/\$ ↾_t $/\$
83		eleq2 2493	. . . . . . . . . . . . . . 15
84		sseq2 3483	. . . . . . . . . . . . . . . . 17
85	84	anbi2d 708	. . . . . . . . . . . . . . . 16 $/\$ $/\$
86	85	rexbidv 2937	. . . . . . . . . . . . . . 15 ↾_t $/\$ ↾_t $/\$
87	83, 86	imbi12d 321	. . . . . . . . . . . . . 14 ↾_t $/\$ ↾_t $/\$
88	87	rspcv 3175	. . . . . . . . . . . . 13 ↾_t $/\$ ↾_t $/\$
89	56, 82, 88	mpsyl 65	. . . . . . . . . . . 12 $/\$ $/\$ ↾_t $/\$
90	55, 89	syld 45	. . . . . . . . . . 11 $/\$ $/\$ ↾_t $/\$
91		0re 9639	. . . . . . . . . . . 12
92		letric 9730	. . . . . . . . . . . 12 $/\$ $\/$
93	26, 91, 92	sylancl 666	. . . . . . . . . . 11 $/\$ $/\$ $\/$
94	90, 93	jctird 546	. . . . . . . . . 10 $/\$ $/\$ ↾_t $/\$ $/\$ $\/$
95		r19.41v 2978	. . . . . . . . . . 11 ↾_t $/\$ $/\$ $\/$ ↾_t $/\$ $/\$ $\/$
96		anass 653	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$
97	96	rexbii 2925	. . . . . . . . . . 11 ↾_t $/\$ $/\$ $\/$ ↾_t $/\$ $/\$ $\/$
98	95, 97	bitr3i 254	. . . . . . . . . 10 ↾_t $/\$ $/\$ $\/$ ↾_t $/\$ $/\$ $\/$
99	94, 98	syl6ib 229	. . . . . . . . 9 $/\$ $/\$ ↾_t $/\$ $/\$ $\/$
100	58	topontopi 19923	. . . . . . . . . . . . 13 ↾_t
101	20	eltopss 19914	. . . . . . . . . . . . 13 ↾_t $/\$ ↾_t
102	100, 101	mpan 674	. . . . . . . . . . . 12 ↾_t
103		fvex 5883	. . . . . . . . . . . . . . . . . 18
104	103, 50	dmmpti 5717	. . . . . . . . . . . . . . . . 17
105	104	sseq2i 3486	. . . . . . . . . . . . . . . 16
106		funmpt 5629	. . . . . . . . . . . . . . . . 17
107		funimass4 5924	. . . . . . . . . . . . . . . . 17 $/\$
108	106, 107	mpan 674	. . . . . . . . . . . . . . . 16
109	105, 108	sylbir 216	. . . . . . . . . . . . . . 15
110		ssel2 3456	. . . . . . . . . . . . . . . . 17 $/\$
111		fveq2 5873	. . . . . . . . . . . . . . . . . . . . 21
112	111	fveq1d 5875	. . . . . . . . . . . . . . . . . . . 20
113		fvex 5883	. . . . . . . . . . . . . . . . . . . 20
114	112, 50, 113	fvmpt 5956	. . . . . . . . . . . . . . . . . . 19
115	114	eleq1d 2489	. . . . . . . . . . . . . . . . . 18
116		eliooord 11690	. . . . . . . . . . . . . . . . . 18 $/\$
117	115, 116	syl6bi 231	. . . . . . . . . . . . . . . . 17 $/\$
118	110, 117	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
119	118	ralimdva 2831	. . . . . . . . . . . . . . 15 $/\$
120	109, 119	sylbid 218	. . . . . . . . . . . . . 14 $/\$
121	120	adantl 467	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
122		absnid 13340	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
123	122	oveq2d 6313	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
124	27	negidd 9972	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
125	124	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
126	123, 125	eqtrd 2461	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
127	26, 126	sylan 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
128	127	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
129	128	breq2d 4429	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
130	22	ffvelrnda 6029	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
131		elmapi 7493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
132	130, 131	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
133	132	ffvelrnda 6029	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
134	133	an32s 811	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
135		0red 9640	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
136	134, 135	ltnled 9778	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
137	136	adantllr 723	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
138	137	adantlr 719	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
139	129, 138	bitrd 256	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
140	139	biimpd 210	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
141	110, 140	sylan2 476	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
142	141	anassrs 652	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
143	142	adantld 468	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
144	143	ralimdva 2831	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
145	144	an32s 811	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
146	145	impancom 441	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
147		absid 13338	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
148	147	oveq2d 6313	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
149	27	subidd 9970	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
150	149	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
151	148, 150	eqtrd 2461	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
152	26, 151	sylan 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
153	152	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
154	153	breq1d 4427	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
155	135, 134	ltnled 9778	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
156	155	adantllr 723	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
157	156	adantlr 719	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
158	154, 157	bitrd 256	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
159	158	biimpd 210	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
160	110, 159	sylan2 476	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
161	160	anassrs 652	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
162	161	adantrd 469	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163	162	ralimdva 2831	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
164	163	an32s 811	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
165	164	impancom 441	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
166	146, 165	orim12d 846	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
167	166	expimpd 606	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
168	121, 167	syland 483	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
169	102, 168	sylan2 476	. . . . . . . . . . 11 $/\$ $/\$ $/\$ ↾_t $/\$ $\/$ $\/$
170	169	anim2d 567	. . . . . . . . . 10 $/\$ $/\$ $/\$ ↾_t $/\$ $/\$ $\/$ $/\$ $\/$
171	170	reximdva 2898	. . . . . . . . 9 $/\$ $/\$ ↾_t $/\$ $/\$ $\/$ ↾_t $/\$ $\/$
172	99, 171	syld 45	. . . . . . . 8 $/\$ $/\$ ↾_t $/\$ $\/$
173		ralnex 2869	. . . . . . . . . . . . . 14
174	173	rexbii 2925	. . . . . . . . . . . . 13
175		letsr 16451	. . . . . . . . . . . . . . 15
176	175	elexi 3088	. . . . . . . . . . . . . 14
177	176	cnvex 6746	. . . . . . . . . . . . . 14
178		breq 4419	. . . . . . . . . . . . . . . 16
179	178	notbid 295	. . . . . . . . . . . . . . 15
180	179	ralbidv 2862	. . . . . . . . . . . . . 14
181		breq 4419	. . . . . . . . . . . . . . . . 17
182		c0ex 9633	. . . . . . . . . . . . . . . . . 18
183	182, 113	brcnv 5029	. . . . . . . . . . . . . . . . 17
184	181, 183	syl6bb 264	. . . . . . . . . . . . . . . 16
185	184	notbid 295	. . . . . . . . . . . . . . 15
186	185	ralbidv 2862	. . . . . . . . . . . . . 14
187	176, 177, 180, 186	rexpr 4048	. . . . . . . . . . . . 13 $\/$
188		rexnal 2871	. . . . . . . . . . . . 13
189	174, 187, 188	3bitr3i 278	. . . . . . . . . . . 12 $\/$
190	189	anbi2i 698	. . . . . . . . . . 11 $/\$ $\/$ $/\$
191		annim 426	. . . . . . . . . . 11 $/\$
192	190, 191	bitri 252	. . . . . . . . . 10 $/\$ $\/$
193	192	rexbii 2925	. . . . . . . . 9 ↾_t $/\$ $\/$ ↾_t
194		rexnal 2871	. . . . . . . . 9 ↾_t ↾_t
195	193, 194	bitri 252	. . . . . . . 8 ↾_t $/\$ $\/$ ↾_t
196	172, 195	syl6ib 229	. . . . . . 7 $/\$ $/\$ ↾_t
197	196	necon4ad 2642	. . . . . 6 $/\$ $/\$ ↾_t
198	197	ralimdva 2831	. . . . 5 $/\$ ↾_t
199		ffn 5738	. . . . . 6
200	25, 199	syl 17	. . . . 5 $/\$
201	198, 200	jctild 545	. . . 4 $/\$ ↾_t $/\$
202		fconstfv 6133	. . . . 5 $/\$
203	182	fconst2 6128	. . . . 5
204	202, 203	bitr3i 254	. . . 4 $/\$
205	201, 204	syl6ib 229	. . 3 $/\$ ↾_t
206	205	reximdva 2898	. 2 ↾_t
207	7, 206	mpd 15	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1437

wcel 1867

wne 2616

wral 2773

wrex 2774

cvv 3078

wss 3433

csn 3993

cpr 3995

cuni 4213 class class class wbr 4417

cmpt 4476

cxp 4844

ccnv 4845

cdm 4846

crn 4847

cima 4849

wfun 5587

wfn 5588

wf 5589

cfv 5593 (class class class)co 6297

cmap 7472

cc 9533

cr 9534

cc0 9535

c1 9536

caddc 9538

cxr 9670

clt 9671

cle 9672

cmin 9856

cneg 9857

cn 10605

crp 11298

cioo 11631

cicc 11634

cfz 11778

cabs 13276 ↾_t crest 15297

ctg 15314

cpt 15315

ctsr 16423

ctop 19894 TopOnctopon 19895

ccn 20217

ccnp 20218

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1838 ax-8 1869 ax-9 1871 ax-10 1886 ax-11 1891 ax-12 1904 ax-13 2052 ax-ext 2398 ax-rep 4530 ax-sep 4540 ax-nul 4548 ax-pow 4595 ax-pr 4653 ax-un 6589 ax-inf2 8144 ax-cnex 9591 ax-resscn 9592 ax-1cn 9593 ax-icn 9594 ax-addcl 9595 ax-addrcl 9596 ax-mulcl 9597 ax-mulrcl 9598 ax-mulcom 9599 ax-addass 9600 ax-mulass 9601 ax-distr 9602 ax-i2m1 9603 ax-1ne0 9604 ax-1rid 9605 ax-rnegex 9606 ax-rrecex 9607 ax-cnre 9608 ax-pre-lttri 9609 ax-pre-lttrn 9610 ax-pre-ltadd 9611 ax-pre-mulgt0 9612 ax-pre-sup 9613

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 1660 df-nf 1664 df-sb 1787 df-eu 2267 df-mo 2268 df-clab 2406 df-cleq 2412 df-clel 2415 df-nfc 2570 df-ne 2618 df-nel 2619 df-ral 2778 df-rex 2779 df-reu 2780 df-rmo 2781 df-rab 2782 df-v 3080 df-sbc 3297 df-csb 3393 df-dif 3436 df-un 3438 df-in 3440 df-ss 3447 df-pss 3449 df-nul 3759 df-if 3907 df-pw 3978 df-sn 3994 df-pr 3996 df-tp 3998 df-op 4000 df-uni 4214 df-int 4250 df-iun 4295 df-iin 4296 df-disj 4389 df-br 4418 df-opab 4477 df-mpt 4478 df-tr 4513 df-eprel 4757 df-id 4761 df-po 4767 df-so 4768 df-fr 4805 df-se 4806 df-we 4807 df-xp 4852 df-rel 4853 df-cnv 4854 df-co 4855 df-dm 4856 df-rn 4857 df-res 4858 df-ima 4859 df-pred 5391 df-ord 5437 df-on 5438 df-lim 5439 df-suc 5440 df-iota 5557 df-fun 5595 df-fn 5596 df-f 5597 df-f1 5598 df-fo 5599 df-f1o 5600 df-fv 5601 df-isom 5602 df-riota 6259 df-ov 6300 df-oprab 6301 df-mpt2 6302 df-of 6537 df-om 6699 df-1st 6799 df-2nd 6800 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-2o 7183 df-oadd 7186 df-omul 7187 df-er 7363 df-map 7474 df-pm 7475 df-ixp 7523 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-fi 7923 df-sup 7954 df-inf 7955 df-oi 8023 df-card 8370 df-acn 8373 df-cda 8594 df-pnf 9673 df-mnf 9674 df-xr 9675 df-ltxr 9676 df-le 9677 df-sub 9858 df-neg 9859 df-div 10266 df-nn 10606 df-2 10664 df-3 10665 df-n0 10866 df-z 10934 df-uz 11156 df-q 11261 df-rp 11299 df-xneg 11405 df-xadd 11406 df-xmul 11407 df-ioo 11635 df-icc 11638 df-fz 11779 df-fzo 11910 df-fl 12021 df-seq 12207 df-exp 12266 df-fac 12453 df-bc 12481 df-hash 12509 df-cj 13141 df-re 13142 df-im 13143 df-sqrt 13277 df-abs 13278 df-clim 13530 df-sum 13731 df-dvds 14284 df-rest 15299 df-topgen 15320 df-pt 15321 df-ps 16424 df-tsr 16425 df-psmet 18940 df-xmet 18941 df-met 18942 df-bl 18943 df-mopn 18944 df-top 19898 df-bases 19899 df-topon 19900 df-cld 20011 df-ntr 20012 df-cls 20013 df-lp 20129 df-cn 20220 df-cnp 20221 df-t1 20307 df-haus 20308 df-cmp 20379 df-tx 20554 df-hmeo 20747 df-hmph 20748 df-ii 21886

This theorem is referenced by: broucube 31882

W3C validator