tpr2rico - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > tpr2rico		Structured version Unicode version

Theorem tpr2rico 26196

Description: For any point of an open set of the usual topology on

there is an open square which contains that point and is entirely in the open set. This is square is actually a ball by the

norm

. (Contributed by Thierry Arnoux, 21-Sep-2017.)

**Hypotheses**
Ref	Expression
tpr2rico.0
tpr2rico.1
tpr2rico.2

**Assertion**
Ref	Expression
tpr2rico	$/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

Proof of Theorem tpr2rico Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ioo 11292	. . . . . . . . . 10 $/\$
2	1	ixxf 11298	. . . . . . . . 9
3		ffn 5547	. . . . . . . . 9
4	2, 3	mp1i 12	. . . . . . . 8 $/\$ $/\$
5		elssuni 4109	. . . . . . . . . . . . . 14
6		tpr2rico.0	. . . . . . . . . . . . . . . 16
7		retop 20182	. . . . . . . . . . . . . . . 16
8	6, 7	eqeltri 2503	. . . . . . . . . . . . . . 15
9		uniretop 20183	. . . . . . . . . . . . . . . 16
10	6	unieqi 4088	. . . . . . . . . . . . . . . 16
11	9, 10	eqtr4i 2456	. . . . . . . . . . . . . . 15
12	8, 8, 11, 11	txunii 19008	. . . . . . . . . . . . . 14
13	5, 12	syl6sseqr 3391	. . . . . . . . . . . . 13
14	13	ad2antrr 718	. . . . . . . . . . . 12 $/\$ $/\$
15		simplr 747	. . . . . . . . . . . 12 $/\$ $/\$
16	14, 15	sseldd 3345	. . . . . . . . . . 11 $/\$ $/\$
17		xp1st 6595	. . . . . . . . . . 11
18	16, 17	syl 16	. . . . . . . . . 10 $/\$ $/\$
19		simpr 458	. . . . . . . . . . . 12 $/\$ $/\$
20	19	rpred 11015	. . . . . . . . . . 11 $/\$ $/\$
21	20	rehalfcld 10559	. . . . . . . . . 10 $/\$ $/\$
22	18, 21	resubcld 9764	. . . . . . . . 9 $/\$ $/\$
23	22	rexrd 9421	. . . . . . . 8 $/\$ $/\$
24	18, 21	readdcld 9401	. . . . . . . . 9 $/\$ $/\$
25	24	rexrd 9421	. . . . . . . 8 $/\$ $/\$
26		fnovrn 6227	. . . . . . . 8 $/\$ $/\$
27	4, 23, 25, 26	syl3anc 1211	. . . . . . 7 $/\$ $/\$
28		xp2nd 6596	. . . . . . . . . . 11
29	16, 28	syl 16	. . . . . . . . . 10 $/\$ $/\$
30	29, 21	resubcld 9764	. . . . . . . . 9 $/\$ $/\$
31	30	rexrd 9421	. . . . . . . 8 $/\$ $/\$
32	29, 21	readdcld 9401	. . . . . . . . 9 $/\$ $/\$
33	32	rexrd 9421	. . . . . . . 8 $/\$ $/\$
34		fnovrn 6227	. . . . . . . 8 $/\$ $/\$
35	4, 31, 33, 34	syl3anc 1211	. . . . . . 7 $/\$ $/\$
36		eqidd 2434	. . . . . . 7 $/\$ $/\$
37		xpeq1 4841	. . . . . . . . 9
38	37	eqeq2d 2444	. . . . . . . 8
39		xpeq2 4842	. . . . . . . . 9
40	39	eqeq2d 2444	. . . . . . . 8
41	38, 40	rspc2ev 3070	. . . . . . 7 $/\$ $/\$
42	27, 35, 36, 41	syl3anc 1211	. . . . . 6 $/\$ $/\$
43		eqid 2433	. . . . . . 7
44		vex 2965	. . . . . . . 8
45		vex 2965	. . . . . . . 8
46	44, 45	xpex 6497	. . . . . . 7
47	43, 46	elrnmpt2 6192	. . . . . 6
48	42, 47	sylibr 212	. . . . 5 $/\$ $/\$
49		tpr2rico.2	. . . . 5
50	48, 49	syl6eleqr 2524	. . . 4 $/\$ $/\$
51	50	ralrimiva 2789	. . 3 $/\$
52		xpss 4933	. . . . . . 7
53	52, 16	sseldi 3342	. . . . . 6 $/\$ $/\$
54	18	rexrd 9421	. . . . . . . 8 $/\$ $/\$
55	19	rphalfcld 11027	. . . . . . . . 9 $/\$ $/\$
56	18, 55	ltsubrpd 11043	. . . . . . . 8 $/\$ $/\$
57	18, 55	ltaddrpd 11044	. . . . . . . 8 $/\$ $/\$
58		elioo1 11328	. . . . . . . . 9 $/\$ $/\$ $/\$
59	23, 25, 58	syl2anc 654	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
60	54, 56, 57, 59	mpbir3and 1164	. . . . . . 7 $/\$ $/\$
61	29	rexrd 9421	. . . . . . . 8 $/\$ $/\$
62	29, 55	ltsubrpd 11043	. . . . . . . 8 $/\$ $/\$
63	29, 55	ltaddrpd 11044	. . . . . . . 8 $/\$ $/\$
64		elioo1 11328	. . . . . . . . 9 $/\$ $/\$ $/\$
65	31, 33, 64	syl2anc 654	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
66	61, 62, 63, 65	mpbir3and 1164	. . . . . . 7 $/\$ $/\$
67	60, 66	jca 529	. . . . . 6 $/\$ $/\$ $/\$
68		elxp7 6598	. . . . . 6 $/\$ $/\$
69	53, 67, 68	sylanbrc 657	. . . . 5 $/\$ $/\$
70	69	ralrimiva 2789	. . . 4 $/\$
71		mnfle 11101	. . . . . . . . . . . . . . . . . 18
72	23, 71	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
73		pnfge 11098	. . . . . . . . . . . . . . . . . 18
74	25, 73	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
75		mnfxr 11082	. . . . . . . . . . . . . . . . . 18
76		pnfxr 11080	. . . . . . . . . . . . . . . . . 18
77		ioossioo 25886	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
78	75, 76, 77	mpanl12 675	. . . . . . . . . . . . . . . . 17 $/\$
79	72, 74, 78	syl2anc 654	. . . . . . . . . . . . . . . 16 $/\$ $/\$
80		ioomax 11358	. . . . . . . . . . . . . . . 16
81	79, 80	syl6sseq 3390	. . . . . . . . . . . . . . 15 $/\$ $/\$
82		mnfle 11101	. . . . . . . . . . . . . . . . . 18
83	31, 82	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
84		pnfge 11098	. . . . . . . . . . . . . . . . . 18
85	33, 84	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
86		ioossioo 25886	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
87	75, 76, 86	mpanl12 675	. . . . . . . . . . . . . . . . 17 $/\$
88	83, 85, 87	syl2anc 654	. . . . . . . . . . . . . . . 16 $/\$ $/\$
89	88, 80	syl6sseq 3390	. . . . . . . . . . . . . . 15 $/\$ $/\$
90		xpss12 4932	. . . . . . . . . . . . . . 15 $/\$
91	81, 89, 90	syl2anc 654	. . . . . . . . . . . . . 14 $/\$ $/\$
92	91	sselda 3344	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
93	92	expcom 435	. . . . . . . . . . . 12 $/\$ $/\$
94	93	ancld 548	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
95	94	imdistanri 684	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96	13	adantr 462	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
97		simpr1 987	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
98	96, 97	sseldd 3345	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
99	98	3anassrs 1202	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
100		simpr 458	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
101		simplr 747	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
102	101	rphalfcld 11027	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
103		tpr2rico.1	. . . . . . . . . . . . . . 15
104	103	cnre2csqima 26195	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
105	99, 100, 102, 104	syl3anc 1211	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
106		eqid 2433	. . . . . . . . . . . . . . . . . . . . 21 ℂ_fld ℂ_fld
107	103, 6, 106	cnrehmeo 20367	. . . . . . . . . . . . . . . . . . . 20 ℂ_fld
108	106	cnfldtopon 20204	. . . . . . . . . . . . . . . . . . . . . 22 ℂ_fld TopOn
109	108	toponunii 18379	. . . . . . . . . . . . . . . . . . . . 21 ℂ_fld
110	12, 109	hmeof1o 19179	. . . . . . . . . . . . . . . . . . . 20 ℂ_fld
111		f1of 5629	. . . . . . . . . . . . . . . . . . . 20
112	107, 110, 111	mp2b 10	. . . . . . . . . . . . . . . . . . 19
113	112	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
114	113, 99	ffvelrnd 5832	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
115	112	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
116	115	ffvelrnda 5831	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
117		sqsscirc2 26193	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
118	114, 116, 101, 117	syl21anc 1210	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
119	118	imp 429	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
120	101	rpxrd 11016	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
121	120	adantr 462	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
122		cnxmet 20194	. . . . . . . . . . . . . . . . 17
123	121, 122	jctil 534	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
124	114	adantr 462	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
125	116	adantr 462	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
126	124, 125	jca 529	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
127		eqid 2433	. . . . . . . . . . . . . . . . . . 19
128	127	cnmetdval 20192	. . . . . . . . . . . . . . . . . 18 $/\$
129	125, 124, 128	syl2anc 654	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
130		simpr 458	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
131	129, 130	eqbrtrd 4300	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
132		elbl3 19809	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
133	132	biimpar 482	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
134	123, 126, 131, 133	syl21anc 1210	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
135	119, 134	syldan 467	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
136	135	ex 434	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
137	105, 136	syld 44	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
138		f1ocnv 5641	. . . . . . . . . . . . . . 15
139	107, 110, 138	mp2b 10	. . . . . . . . . . . . . 14
140		f1ofun 5631	. . . . . . . . . . . . . 14
141	139, 140	ax-mp 5	. . . . . . . . . . . . 13
142		f1odm 5633	. . . . . . . . . . . . . . 15
143	139, 142	ax-mp 5	. . . . . . . . . . . . . 14
144	116, 143	syl6eleqr 2524	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
145		funfvima 5939	. . . . . . . . . . . . 13 $/\$
146	141, 144, 145	sylancr 656	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
147	107, 110	mp1i 12	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
148		f1ocnvfv1 5970	. . . . . . . . . . . . . . 15 $/\$
149	147, 100, 148	syl2anc 654	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
150	149	eleq1d 2499	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
151	150	biimpd 207	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152	137, 146, 151	3syld 55	. . . . . . . . . . 11 $/\$ $/\$ $/\$
153	152	imp 429	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
154	95, 153	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
155	154	ex 434	. . . . . . . 8 $/\$ $/\$
156	155	ssrdv 3350	. . . . . . 7 $/\$ $/\$
157	156	ralrimiva 2789	. . . . . 6 $/\$
158	103	mpt2fun 6181	. . . . . . . . . 10
159	158	a1i 11	. . . . . . . . 9 $/\$
160	13	sselda 3344	. . . . . . . . . 10 $/\$
161		f1odm 5633	. . . . . . . . . . 11
162	107, 110, 161	mp2b 10	. . . . . . . . . 10
163	160, 162	syl6eleqr 2524	. . . . . . . . 9 $/\$
164		simpr 458	. . . . . . . . 9 $/\$
165		funfvima 5939	. . . . . . . . . 10 $/\$
166	165	imp 429	. . . . . . . . 9 $/\$ $/\$
167	159, 163, 164, 166	syl21anc 1210	. . . . . . . 8 $/\$
168		hmeoima 19180	. . . . . . . . . . 11 ℂ_fld $/\$ ℂ_fld
169	107, 168	mpan 663	. . . . . . . . . 10 ℂ_fld
170	106	cnfldtopn 20203	. . . . . . . . . . . . 13 ℂ_fld
171	170	elmopn2 19862	. . . . . . . . . . . 12 ℂ_fld $/\$
172	122, 171	ax-mp 5	. . . . . . . . . . 11 ℂ_fld $/\$
173	172	simprbi 461	. . . . . . . . . 10 ℂ_fld
174	169, 173	syl 16	. . . . . . . . 9
175	174	adantr 462	. . . . . . . 8 $/\$
176		oveq1 6087	. . . . . . . . . . 11
177	176	sseq1d 3371	. . . . . . . . . 10
178	177	rexbidv 2726	. . . . . . . . 9
179	178	rspcva 3060	. . . . . . . 8 $/\$
180	167, 175, 179	syl2anc 654	. . . . . . 7 $/\$
181		imass2 5192	. . . . . . . . . 10
182		f1of1 5628	. . . . . . . . . . . . 13
183	107, 110, 182	mp2b 10	. . . . . . . . . . . 12
184		f1imacnv 5645	. . . . . . . . . . . 12 $/\$
185	183, 13, 184	sylancr 656	. . . . . . . . . . 11
186	185	sseq2d 3372	. . . . . . . . . 10
187	181, 186	syl5ib 219	. . . . . . . . 9
188	187	reximdv 2817	. . . . . . . 8
189	188	adantr 462	. . . . . . 7 $/\$
190	180, 189	mpd 15	. . . . . 6 $/\$
191		r19.29 2847	. . . . . 6 $/\$ $/\$
192	157, 190, 191	syl2anc 654	. . . . 5 $/\$ $/\$
193		sstr 3352	. . . . . 6 $/\$
194	193	reximi 2813	. . . . 5 $/\$
195	192, 194	syl 16	. . . 4 $/\$
196		r19.29 2847	. . . 4 $/\$ $/\$
197	70, 195, 196	syl2anc 654	. . 3 $/\$ $/\$
198		r19.29 2847	. . 3 $/\$ $/\$ $/\$ $/\$
199	51, 197, 198	syl2anc 654	. 2 $/\$ $/\$ $/\$
200		eleq2 2494	. . . . 5
201		sseq1 3365	. . . . 5
202	200, 201	anbi12d 703	. . . 4 $/\$ $/\$
203	202	rspcev 3062	. . 3 $/\$ $/\$ $/\$
204	203	rexlimivw 2827	. 2 $/\$ $/\$ $/\$
205	199, 204	syl 16	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 958

wceq 1362

wcel 1755

wral 2705

wrex 2706

cvv 2962

wss 3316

cpw 3848

cuni 4079 class class class wbr 4280

cxp 4825

ccnv 4826

cdm 4827

crn 4828

cima 4830

ccom 4831

wfun 5400

wfn 5401

wf 5402

wf1 5403

wf1o 5405

cfv 5406 (class class class)co 6080

cmpt2 6082

c1st 6564

c2nd 6565

cc 9268

cr 9269

ci 9272

caddc 9273

cmul 9275

cpnf 9403

cmnf 9404

cxr 9405

clt 9406

cle 9407

cmin 9583

cdiv 9981

c2 10359

crp 10979

cioo 11288

cre 12570

cim 12571

cabs 12707

ctopn 14343

ctg 14359

cxmt 17645

cbl 17647 ℂ_fldccnfld 17662

ctop 18340

ctx 18975

chmeo 19168

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1594 ax-4 1605 ax-5 1669 ax-6 1707 ax-7 1727 ax-8 1757 ax-9 1759 ax-10 1774 ax-11 1779 ax-12 1791 ax-13 1942 ax-ext 2414 ax-rep 4391 ax-sep 4401 ax-nul 4409 ax-pow 4458 ax-pr 4519 ax-un 6361 ax-inf2 7835 ax-cnex 9326 ax-resscn 9327 ax-1cn 9328 ax-icn 9329 ax-addcl 9330 ax-addrcl 9331 ax-mulcl 9332 ax-mulrcl 9333 ax-mulcom 9334 ax-addass 9335 ax-mulass 9336 ax-distr 9337 ax-i2m1 9338 ax-1ne0 9339 ax-1rid 9340 ax-rnegex 9341 ax-rrecex 9342 ax-cnre 9343 ax-pre-lttri 9344 ax-pre-lttrn 9345 ax-pre-ltadd 9346 ax-pre-mulgt0 9347 ax-pre-sup 9348 ax-addf 9349 ax-mulf 9350

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 959 df-3an 960 df-tru 1365 df-ex 1590 df-nf 1593 df-sb 1700 df-eu 2258 df-mo 2259 df-clab 2420 df-cleq 2426 df-clel 2429 df-nfc 2558 df-ne 2598 df-nel 2599 df-ral 2710 df-rex 2711 df-reu 2712 df-rmo 2713 df-rab 2714 df-v 2964 df-sbc 3176 df-csb 3277 df-dif 3319 df-un 3321 df-in 3323 df-ss 3330 df-pss 3332 df-nul 3626 df-if 3780 df-pw 3850 df-sn 3866 df-pr 3868 df-tp 3870 df-op 3872 df-uni 4080 df-int 4117 df-iun 4161 df-iin 4162 df-br 4281 df-opab 4339 df-mpt 4340 df-tr 4374 df-eprel 4619 df-id 4623 df-po 4628 df-so 4629 df-fr 4666 df-se 4667 df-we 4668 df-ord 4709 df-on 4710 df-lim 4711 df-suc 4712 df-xp 4833 df-rel 4834 df-cnv 4835 df-co 4836 df-dm 4837 df-rn 4838 df-res 4839 df-ima 4840 df-iota 5369 df-fun 5408 df-fn 5409 df-f 5410 df-f1 5411 df-fo 5412 df-f1o 5413 df-fv 5414 df-isom 5415 df-riota 6039 df-ov 6083 df-oprab 6084 df-mpt2 6085 df-of 6309 df-om 6466 df-1st 6566 df-2nd 6567 df-supp 6680 df-recs 6818 df-rdg 6852 df-1o 6908 df-2o 6909 df-oadd 6912 df-er 7089 df-map 7204 df-ixp 7252 df-en 7299 df-dom 7300 df-sdom 7301 df-fin 7302 df-fsupp 7609 df-fi 7649 df-sup 7679 df-oi 7712 df-card 8097 df-cda 8325 df-pnf 9408 df-mnf 9409 df-xr 9410 df-ltxr 9411 df-le 9412 df-sub 9585 df-neg 9586 df-div 9982 df-nn 10311 df-2 10368 df-3 10369 df-4 10370 df-5 10371 df-6 10372 df-7 10373 df-8 10374 df-9 10375 df-10 10376 df-n0 10568 df-z 10635 df-dec 10744 df-uz 10850 df-q 10942 df-rp 10980 df-xneg 11077 df-xadd 11078 df-xmul 11079 df-ioo 11292 df-icc 11295 df-fz 11425 df-fzo 11533 df-seq 11791 df-exp 11850 df-hash 12088 df-cj 12572 df-re 12573 df-im 12574 df-sqr 12708 df-abs 12709 df-struct 14159 df-ndx 14160 df-slot 14161 df-base 14162 df-sets 14163 df-ress 14164 df-plusg 14234 df-mulr 14235 df-starv 14236 df-sca 14237 df-vsca 14238 df-ip 14239 df-tset 14240 df-ple 14241 df-ds 14243 df-unif 14244 df-hom 14245 df-cco 14246 df-rest 14344 df-topn 14345 df-0g 14363 df-gsum 14364 df-topgen 14365 df-pt 14366 df-prds 14369 df-xrs 14423 df-qtop 14428 df-imas 14429 df-xps 14431 df-mre 14507 df-mrc 14508 df-acs 14510 df-mnd 15398 df-submnd 15448 df-mulg 15528 df-cntz 15815 df-cmn 16259 df-psmet 17653 df-xmet 17654 df-met 17655 df-bl 17656 df-mopn 17657 df-cnfld 17663 df-top 18345 df-bases 18347 df-topon 18348 df-topsp 18349 df-cn 18673 df-cnp 18674 df-tx 18977 df-hmeo 19170 df-xms 19737 df-ms 19738 df-tms 19739 df-cncf 20296

This theorem is referenced by: dya2iocnei 26551

W3C validator