tpr2rico - Mathbox for Thierry Arnoux

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

Theorem tpr2rico 28718

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 11639	. . . . . . . . . 10 $/\$
2	1	ixxf 11645	. . . . . . . . 9
3		ffn 5728	. . . . . . . . 9
4	2, 3	mp1i 13	. . . . . . . 8 $/\$ $/\$
5		elssuni 4227	. . . . . . . . . . . . . 14
6		tpr2rico.0	. . . . . . . . . . . . . . . 16
7		retop 21782	. . . . . . . . . . . . . . . 16
8	6, 7	eqeltri 2525	. . . . . . . . . . . . . . 15
9		uniretop 21783	. . . . . . . . . . . . . . . 16
10	6	unieqi 4207	. . . . . . . . . . . . . . . 16
11	9, 10	eqtr4i 2476	. . . . . . . . . . . . . . 15
12	8, 8, 11, 11	txunii 20608	. . . . . . . . . . . . . 14
13	5, 12	syl6sseqr 3479	. . . . . . . . . . . . 13
14	13	ad2antrr 732	. . . . . . . . . . . 12 $/\$ $/\$
15		simplr 762	. . . . . . . . . . . 12 $/\$ $/\$
16	14, 15	sseldd 3433	. . . . . . . . . . 11 $/\$ $/\$
17		xp1st 6823	. . . . . . . . . . 11
18	16, 17	syl 17	. . . . . . . . . 10 $/\$ $/\$
19		simpr 463	. . . . . . . . . . . 12 $/\$ $/\$
20	19	rpred 11341	. . . . . . . . . . 11 $/\$ $/\$
21	20	rehalfcld 10859	. . . . . . . . . 10 $/\$ $/\$
22	18, 21	resubcld 10047	. . . . . . . . 9 $/\$ $/\$
23	22	rexrd 9690	. . . . . . . 8 $/\$ $/\$
24	18, 21	readdcld 9670	. . . . . . . . 9 $/\$ $/\$
25	24	rexrd 9690	. . . . . . . 8 $/\$ $/\$
26		fnovrn 6444	. . . . . . . 8 $/\$ $/\$
27	4, 23, 25, 26	syl3anc 1268	. . . . . . 7 $/\$ $/\$
28		xp2nd 6824	. . . . . . . . . . 11
29	16, 28	syl 17	. . . . . . . . . 10 $/\$ $/\$
30	29, 21	resubcld 10047	. . . . . . . . 9 $/\$ $/\$
31	30	rexrd 9690	. . . . . . . 8 $/\$ $/\$
32	29, 21	readdcld 9670	. . . . . . . . 9 $/\$ $/\$
33	32	rexrd 9690	. . . . . . . 8 $/\$ $/\$
34		fnovrn 6444	. . . . . . . 8 $/\$ $/\$
35	4, 31, 33, 34	syl3anc 1268	. . . . . . 7 $/\$ $/\$
36		eqidd 2452	. . . . . . 7 $/\$ $/\$
37		xpeq1 4848	. . . . . . . . 9
38	37	eqeq2d 2461	. . . . . . . 8
39		xpeq2 4849	. . . . . . . . 9
40	39	eqeq2d 2461	. . . . . . . 8
41	38, 40	rspc2ev 3161	. . . . . . 7 $/\$ $/\$
42	27, 35, 36, 41	syl3anc 1268	. . . . . 6 $/\$ $/\$
43		eqid 2451	. . . . . . 7
44		vex 3048	. . . . . . . 8
45		vex 3048	. . . . . . . 8
46	44, 45	xpex 6595	. . . . . . 7
47	43, 46	elrnmpt2 6409	. . . . . 6
48	42, 47	sylibr 216	. . . . 5 $/\$ $/\$
49		tpr2rico.2	. . . . 5
50	48, 49	syl6eleqr 2540	. . . 4 $/\$ $/\$
51	50	ralrimiva 2802	. . 3 $/\$
52		xpss 4941	. . . . . . 7
53	52, 16	sseldi 3430	. . . . . 6 $/\$ $/\$
54	18	rexrd 9690	. . . . . . . 8 $/\$ $/\$
55	19	rphalfcld 11353	. . . . . . . . 9 $/\$ $/\$
56	18, 55	ltsubrpd 11370	. . . . . . . 8 $/\$ $/\$
57	18, 55	ltaddrpd 11371	. . . . . . . 8 $/\$ $/\$
58		elioo1 11676	. . . . . . . . 9 $/\$ $/\$ $/\$
59	23, 25, 58	syl2anc 667	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
60	54, 56, 57, 59	mpbir3and 1191	. . . . . . 7 $/\$ $/\$
61	29	rexrd 9690	. . . . . . . 8 $/\$ $/\$
62	29, 55	ltsubrpd 11370	. . . . . . . 8 $/\$ $/\$
63	29, 55	ltaddrpd 11371	. . . . . . . 8 $/\$ $/\$
64		elioo1 11676	. . . . . . . . 9 $/\$ $/\$ $/\$
65	31, 33, 64	syl2anc 667	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
66	61, 62, 63, 65	mpbir3and 1191	. . . . . . 7 $/\$ $/\$
67	60, 66	jca 535	. . . . . 6 $/\$ $/\$ $/\$
68		elxp7 6826	. . . . . 6 $/\$ $/\$
69	53, 67, 68	sylanbrc 670	. . . . 5 $/\$ $/\$
70	69	ralrimiva 2802	. . . 4 $/\$
71		mnfle 11435	. . . . . . . . . . . . . . . . . 18
72	23, 71	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
73		pnfge 11432	. . . . . . . . . . . . . . . . . 18
74	25, 73	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
75		mnfxr 11414	. . . . . . . . . . . . . . . . . 18
76		pnfxr 11412	. . . . . . . . . . . . . . . . . 18
77		ioossioo 11726	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
78	75, 76, 77	mpanl12 688	. . . . . . . . . . . . . . . . 17 $/\$
79	72, 74, 78	syl2anc 667	. . . . . . . . . . . . . . . 16 $/\$ $/\$
80		ioomax 11709	. . . . . . . . . . . . . . . 16
81	79, 80	syl6sseq 3478	. . . . . . . . . . . . . . 15 $/\$ $/\$
82		mnfle 11435	. . . . . . . . . . . . . . . . . 18
83	31, 82	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
84		pnfge 11432	. . . . . . . . . . . . . . . . . 18
85	33, 84	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
86		ioossioo 11726	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
87	75, 76, 86	mpanl12 688	. . . . . . . . . . . . . . . . 17 $/\$
88	83, 85, 87	syl2anc 667	. . . . . . . . . . . . . . . 16 $/\$ $/\$
89	88, 80	syl6sseq 3478	. . . . . . . . . . . . . . 15 $/\$ $/\$
90		xpss12 4940	. . . . . . . . . . . . . . 15 $/\$
91	81, 89, 90	syl2anc 667	. . . . . . . . . . . . . 14 $/\$ $/\$
92	91	sselda 3432	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
93	92	expcom 437	. . . . . . . . . . . 12 $/\$ $/\$
94	93	ancld 556	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
95	94	imdistanri 697	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96	13	adantr 467	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
97		simpr1 1014	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
98	96, 97	sseldd 3433	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
99	98	3anassrs 1232	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
100		simpr 463	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
101		simplr 762	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
102	101	rphalfcld 11353	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
103		tpr2rico.1	. . . . . . . . . . . . . . 15
104	103	cnre2csqima 28717	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
105	99, 100, 102, 104	syl3anc 1268	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
106		eqid 2451	. . . . . . . . . . . . . . . . . . . . 21 ℂ_fld ℂ_fld
107	103, 6, 106	cnrehmeo 21981	. . . . . . . . . . . . . . . . . . . 20 ℂ_fld
108	106	cnfldtopon 21803	. . . . . . . . . . . . . . . . . . . . . 22 ℂ_fld TopOn
109	108	toponunii 19947	. . . . . . . . . . . . . . . . . . . . 21 ℂ_fld
110	12, 109	hmeof1o 20779	. . . . . . . . . . . . . . . . . . . 20 ℂ_fld
111		f1of 5814	. . . . . . . . . . . . . . . . . . . 20
112	107, 110, 111	mp2b 10	. . . . . . . . . . . . . . . . . . 19
113	112	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
114	113, 99	ffvelrnd 6023	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
115	112	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
116	115	ffvelrnda 6022	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
117		sqsscirc2 28715	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
118	114, 116, 101, 117	syl21anc 1267	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
119	118	imp 431	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
120	101	rpxrd 11342	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
121	120	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
122		cnxmet 21793	. . . . . . . . . . . . . . . . 17
123	121, 122	jctil 540	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
124	114	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
125	116	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
126	124, 125	jca 535	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
127		eqid 2451	. . . . . . . . . . . . . . . . . . 19
128	127	cnmetdval 21791	. . . . . . . . . . . . . . . . . 18 $/\$
129	125, 124, 128	syl2anc 667	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
130		simpr 463	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
131	129, 130	eqbrtrd 4423	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
132		elbl3 21407	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
133	132	biimpar 488	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
134	123, 126, 131, 133	syl21anc 1267	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
135	119, 134	syldan 473	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
136	135	ex 436	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
137	105, 136	syld 45	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
138		f1ocnv 5826	. . . . . . . . . . . . . . 15
139	107, 110, 138	mp2b 10	. . . . . . . . . . . . . 14
140		f1ofun 5816	. . . . . . . . . . . . . 14
141	139, 140	ax-mp 5	. . . . . . . . . . . . 13
142		f1odm 5818	. . . . . . . . . . . . . . 15
143	139, 142	ax-mp 5	. . . . . . . . . . . . . 14
144	116, 143	syl6eleqr 2540	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
145		funfvima 6140	. . . . . . . . . . . . 13 $/\$
146	141, 144, 145	sylancr 669	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
147	107, 110	mp1i 13	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
148		f1ocnvfv1 6175	. . . . . . . . . . . . . . 15 $/\$
149	147, 100, 148	syl2anc 667	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
150	149	eleq1d 2513	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
151	150	biimpd 211	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152	137, 146, 151	3syld 57	. . . . . . . . . . 11 $/\$ $/\$ $/\$
153	152	imp 431	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
154	95, 153	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
155	154	ex 436	. . . . . . . 8 $/\$ $/\$
156	155	ssrdv 3438	. . . . . . 7 $/\$ $/\$
157	156	ralrimiva 2802	. . . . . 6 $/\$
158	103	mpt2fun 6398	. . . . . . . . . 10
159	158	a1i 11	. . . . . . . . 9 $/\$
160	13	sselda 3432	. . . . . . . . . 10 $/\$
161		f1odm 5818	. . . . . . . . . . 11
162	107, 110, 161	mp2b 10	. . . . . . . . . 10
163	160, 162	syl6eleqr 2540	. . . . . . . . 9 $/\$
164		simpr 463	. . . . . . . . 9 $/\$
165		funfvima 6140	. . . . . . . . . 10 $/\$
166	165	imp 431	. . . . . . . . 9 $/\$ $/\$
167	159, 163, 164, 166	syl21anc 1267	. . . . . . . 8 $/\$
168		hmeoima 20780	. . . . . . . . . . 11 ℂ_fld $/\$ ℂ_fld
169	107, 168	mpan 676	. . . . . . . . . 10 ℂ_fld
170	106	cnfldtopn 21802	. . . . . . . . . . . . 13 ℂ_fld
171	170	elmopn2 21460	. . . . . . . . . . . 12 ℂ_fld $/\$
172	122, 171	ax-mp 5	. . . . . . . . . . 11 ℂ_fld $/\$
173	172	simprbi 466	. . . . . . . . . 10 ℂ_fld
174	169, 173	syl 17	. . . . . . . . 9
175	174	adantr 467	. . . . . . . 8 $/\$
176		oveq1 6297	. . . . . . . . . . 11
177	176	sseq1d 3459	. . . . . . . . . 10
178	177	rexbidv 2901	. . . . . . . . 9
179	178	rspcva 3148	. . . . . . . 8 $/\$
180	167, 175, 179	syl2anc 667	. . . . . . 7 $/\$
181		imass2 5204	. . . . . . . . . 10
182		f1of1 5813	. . . . . . . . . . . . 13
183	107, 110, 182	mp2b 10	. . . . . . . . . . . 12
184		f1imacnv 5830	. . . . . . . . . . . 12 $/\$
185	183, 13, 184	sylancr 669	. . . . . . . . . . 11
186	185	sseq2d 3460	. . . . . . . . . 10
187	181, 186	syl5ib 223	. . . . . . . . 9
188	187	reximdv 2861	. . . . . . . 8
189	188	adantr 467	. . . . . . 7 $/\$
190	180, 189	mpd 15	. . . . . 6 $/\$
191		r19.29 2925	. . . . . 6 $/\$ $/\$
192	157, 190, 191	syl2anc 667	. . . . 5 $/\$ $/\$
193		sstr 3440	. . . . . 6 $/\$
194	193	reximi 2855	. . . . 5 $/\$
195	192, 194	syl 17	. . . 4 $/\$
196		r19.29 2925	. . . 4 $/\$ $/\$
197	70, 195, 196	syl2anc 667	. . 3 $/\$ $/\$
198		r19.29 2925	. . 3 $/\$ $/\$ $/\$ $/\$
199	51, 197, 198	syl2anc 667	. 2 $/\$ $/\$ $/\$
200		eleq2 2518	. . . . 5
201		sseq1 3453	. . . . 5
202	200, 201	anbi12d 717	. . . 4 $/\$ $/\$
203	202	rspcev 3150	. . 3 $/\$ $/\$ $/\$
204	203	rexlimivw 2876	. 2 $/\$ $/\$ $/\$
205	199, 204	syl 17	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 985

wceq 1444

wcel 1887

wral 2737

wrex 2738

cvv 3045

wss 3404

cpw 3951

cuni 4198 class class class wbr 4402

cxp 4832

ccnv 4833

cdm 4834

crn 4835

cima 4837

ccom 4838

wfun 5576

wfn 5577

wf 5578

wf1 5579

wf1o 5581

cfv 5582 (class class class)co 6290

cmpt2 6292

c1st 6791

c2nd 6792

cc 9537

cr 9538

ci 9541

caddc 9542

cmul 9544

cpnf 9672

cmnf 9673

cxr 9674

clt 9675

cle 9676

cmin 9860

cdiv 10269

c2 10659

crp 11302

cioo 11635

cre 13160

cim 13161

cabs 13297

ctopn 15320

ctg 15336

cxmt 18955

cbl 18957 ℂ_fldccnfld 18970

ctop 19917

ctx 20575

chmeo 20768

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-inf2 8146 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-pre-sup 9617 ax-addf 9618 ax-mulf 9619

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-iin 4281 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-se 4794 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-isom 5591 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-of 6531 df-om 6693 df-1st 6793 df-2nd 6794 df-supp 6915 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-2o 7183 df-oadd 7186 df-er 7363 df-map 7474 df-ixp 7523 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-fsupp 7884 df-fi 7925 df-sup 7956 df-inf 7957 df-oi 8025 df-card 8373 df-cda 8598 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-nn 10610 df-2 10668 df-3 10669 df-4 10670 df-5 10671 df-6 10672 df-7 10673 df-8 10674 df-9 10675 df-10 10676 df-n0 10870 df-z 10938 df-dec 11052 df-uz 11160 df-q 11265 df-rp 11303 df-xneg 11409 df-xadd 11410 df-xmul 11411 df-ioo 11639 df-icc 11642 df-fz 11785 df-fzo 11916 df-seq 12214 df-exp 12273 df-hash 12516 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs 13299 df-struct 15123 df-ndx 15124 df-slot 15125 df-base 15126 df-sets 15127 df-ress 15128 df-plusg 15203 df-mulr 15204 df-starv 15205 df-sca 15206 df-vsca 15207 df-ip 15208 df-tset 15209 df-ple 15210 df-ds 15212 df-unif 15213 df-hom 15214 df-cco 15215 df-rest 15321 df-topn 15322 df-0g 15340 df-gsum 15341 df-topgen 15342 df-pt 15343 df-prds 15346 df-xrs 15400 df-qtop 15406 df-imas 15407 df-xps 15410 df-mre 15492 df-mrc 15493 df-acs 15495 df-mgm 16488 df-sgrp 16527 df-mnd 16537 df-submnd 16583 df-mulg 16676 df-cntz 16971 df-cmn 17432 df-psmet 18962 df-xmet 18963 df-met 18964 df-bl 18965 df-mopn 18966 df-cnfld 18971 df-top 19921 df-bases 19922 df-topon 19923 df-topsp 19924 df-cn 20243 df-cnp 20244 df-tx 20577 df-hmeo 20770 df-xms 21335 df-ms 21336 df-tms 21337 df-cncf 21910

This theorem is referenced by: dya2iocnei 29104

W3C validator