Theorem cnheibor 21540

Description: Heine-Borel theorem for complex numbers. A subset of CC is compact iff it is closed and bounded. (Contributed by Mario Carneiro, 14-Sep-2014.)

Hypotheses

Ref	Expression
cnheibor.2	|- J = ( TopOpen ` ℂfld )
cnheibor.3	|- T = ( J ↾t X )

Assertion

Ref	Expression
cnheibor	|- ( X C_ CC -> ( T e. Comp <-> ( X e. ( Clsd ` J ) /\ E. r e. RR A. x e. X ( abs ` x ) <_ r ) ) )

Distinct variable groups:   x, r, T   J, r, x   X, r, x

Proof of Theorem cnheibor

Dummy variables f s u y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnheibor.2	. . . . . 6 |- J = ( TopOpen ` ℂfld )
2	1	cnfldhaus 21377	. . . . 5 |- J e. Haus
3	2	a1i 11	. . . 4 |- ( ( X C_ CC /\ T e. Comp ) -> J e. Haus )
4		simpl 455	. . . 4 |- ( ( X C_ CC /\ T e. Comp ) -> X C_ CC )
5		cnheibor.3	. . . . 5 |- T = ( J ↾t X )
6		simpr 459	. . . . 5 |- ( ( X C_ CC /\ T e. Comp ) -> T e. Comp )
7	5, 6	syl5eqelr 2475	. . . 4 |- ( ( X C_ CC /\ T e. Comp ) -> ( J ↾t X ) e. Comp )
8	1	cnfldtopon 21375	. . . . . 6 |- J e. (TopOn ` CC )
9	8	toponunii 19518	. . . . 5 |- CC = U. J
10	9	hauscmp 19993	. . . 4 |- ( ( J e. Haus /\ X C_ CC /\ ( J ↾t X ) e. Comp ) -> X e. ( Clsd ` J ) )
11	3, 4, 7, 10	syl3anc 1226	. . 3 |- ( ( X C_ CC /\ T e. Comp ) -> X e. ( Clsd ` J ) )
12	1	cnfldtop 21376	. . . . . . . . . . 11 |- J e. Top
13	9	restuni 19749	. . . . . . . . . . 11 |- ( ( J e. Top /\ X C_ CC ) -> X = U. ( J ↾t X ) )
14	12, 4, 13	sylancr 661	. . . . . . . . . 10 |- ( ( X C_ CC /\ T e. Comp ) -> X = U. ( J ↾t X ) )
15	5	unieqi 4172	. . . . . . . . . 10 |- U. T = U. ( J ↾t X )
16	14, 15	syl6eqr 2441	. . . . . . . . 9 |- ( ( X C_ CC /\ T e. Comp ) -> X = U. T )
17	16	eleq2d 2452	. . . . . . . 8 |- ( ( X C_ CC /\ T e. Comp ) -> ( x e. X <-> x e. U. T ) )
18	17	biimpar 483	. . . . . . 7 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. U. T ) -> x e. X )
19	12	a1i 11	. . . . . . . . . 10 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> J e. Top )
20		cnex 9484	. . . . . . . . . . . 12 |- CC e. _V
21		ssexg 4511	. . . . . . . . . . . 12 |- ( ( X C_ CC /\ CC e. _V ) -> X e. _V )
22	4, 20, 21	sylancl 660	. . . . . . . . . . 11 |- ( ( X C_ CC /\ T e. Comp ) -> X e. _V )
23	22	adantr 463	. . . . . . . . . 10 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> X e. _V )
24		cnxmet 21365	. . . . . . . . . . . 12 |- ( abs o. - ) e. ( *Met ` CC )
25	24	a1i 11	. . . . . . . . . . 11 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( abs o. - ) e. ( *Met ` CC ) )
26		0cnd 9500	. . . . . . . . . . 11 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> 0 e. CC )
27	4	sselda 3417	. . . . . . . . . . . . . 14 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> x e. CC )
28	27	abscld 13269	. . . . . . . . . . . . 13 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( abs ` x ) e. RR )
29		peano2re 9664	. . . . . . . . . . . . 13 |- ( ( abs ` x ) e. RR -> ( ( abs ` x ) + 1 ) e. RR )
30	28, 29	syl 16	. . . . . . . . . . . 12 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( ( abs ` x ) + 1 ) e. RR )
31	30	rexrd 9554	. . . . . . . . . . 11 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( ( abs ` x ) + 1 ) e. RR* )
32	1	cnfldtopn 21374	. . . . . . . . . . . 12 |- J = ( MetOpen ` ( abs o. - ) )
33	32	blopn 21088	. . . . . . . . . . 11 |- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ ( ( abs ` x ) + 1 ) e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) e. J )
34	25, 26, 31, 33	syl3anc 1226	. . . . . . . . . 10 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) e. J )
35		elrestr 14836	. . . . . . . . . 10 |- ( ( J e. Top /\ X e. _V /\ ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) e. J ) -> ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) e. ( J ↾t X ) )
36	19, 23, 34, 35	syl3anc 1226	. . . . . . . . 9 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) e. ( J ↾t X ) )
37	36, 5	syl6eleqr 2481	. . . . . . . 8 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) e. T )
38		0cn 9499	. . . . . . . . . . . . . 14 |- 0 e. CC
39		eqid 2382	. . . . . . . . . . . . . . 15 |- ( abs o. - ) = ( abs o. - )
40	39	cnmetdval 21363	. . . . . . . . . . . . . 14 |- ( ( 0 e. CC /\ x e. CC ) -> ( 0 ( abs o. - ) x ) = ( abs ` ( 0 - x ) ) )
41	38, 40	mpan 668	. . . . . . . . . . . . 13 |- ( x e. CC -> ( 0 ( abs o. - ) x ) = ( abs ` ( 0 - x ) ) )
42		df-neg 9721	. . . . . . . . . . . . . . 15 |- -u x = ( 0 - x )
43	42	fveq2i 5777	. . . . . . . . . . . . . 14 |- ( abs ` -u x ) = ( abs ` ( 0 - x ) )
44		absneg 13112	. . . . . . . . . . . . . 14 |- ( x e. CC -> ( abs ` -u x ) = ( abs ` x ) )
45	43, 44	syl5eqr 2437	. . . . . . . . . . . . 13 |- ( x e. CC -> ( abs ` ( 0 - x ) ) = ( abs ` x ) )
46	41, 45	eqtrd 2423	. . . . . . . . . . . 12 |- ( x e. CC -> ( 0 ( abs o. - ) x ) = ( abs ` x ) )
47	27, 46	syl 16	. . . . . . . . . . 11 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( 0 ( abs o. - ) x ) = ( abs ` x ) )
48	28	ltp1d 10392	. . . . . . . . . . 11 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( abs ` x ) < ( ( abs ` x ) + 1 ) )
49	47, 48	eqbrtrd 4387	. . . . . . . . . 10 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( 0 ( abs o. - ) x ) < ( ( abs ` x ) + 1 ) )
50		elbl 20976	. . . . . . . . . . 11 |- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ ( ( abs ` x ) + 1 ) e. RR* ) -> ( x e. ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) <-> ( x e. CC /\ ( 0 ( abs o. - ) x ) < ( ( abs ` x ) + 1 ) ) ) )
51	25, 26, 31, 50	syl3anc 1226	. . . . . . . . . 10 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( x e. ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) <-> ( x e. CC /\ ( 0 ( abs o. - ) x ) < ( ( abs ` x ) + 1 ) ) ) )
52	27, 49, 51	mpbir2and 920	. . . . . . . . 9 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> x e. ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) )
53		simpr 459	. . . . . . . . 9 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> x e. X )
54	52, 53	elind 3602	. . . . . . . 8 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> x e. ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) )
55	27	absge0d 13277	. . . . . . . . . 10 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> 0 <_ ( abs ` x ) )
56	28, 55	ge0p1rpd 11203	. . . . . . . . 9 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( ( abs ` x ) + 1 ) e. RR+ )
57		eqid 2382	. . . . . . . . 9 |- ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) = ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X )
58		oveq2 6204	. . . . . . . . . . . 12 |- ( r = ( ( abs ` x ) + 1 ) -> ( 0 ( ball ` ( abs o. - ) ) r ) = ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) )
59	58	ineq1d 3613	. . . . . . . . . . 11 |- ( r = ( ( abs ` x ) + 1 ) -> ( ( 0 ( ball ` ( abs o. - ) ) r ) i^i X ) = ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) )
60	59	eqeq2d 2396	. . . . . . . . . 10 |- ( r = ( ( abs ` x ) + 1 ) -> ( ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) = ( ( 0 ( ball ` ( abs o. - ) ) r ) i^i X ) <-> ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) = ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) ) )
61	60	rspcev 3135	. . . . . . . . 9 |- ( ( ( ( abs ` x ) + 1 ) e. RR+ /\ ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) = ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) ) -> E. r e. RR+ ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) = ( ( 0 ( ball ` ( abs o. - ) ) r ) i^i X ) )
62	56, 57, 61	sylancl 660	. . . . . . . 8 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> E. r e. RR+ ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) = ( ( 0 ( ball ` ( abs o. - ) ) r ) i^i X ) )
63		eleq2 2455	. . . . . . . . . 10 |- ( u = ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) -> ( x e. u <-> x e. ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) ) )
64		eqeq1 2386	. . . . . . . . . . 11 |- ( u = ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) -> ( u = ( ( 0 ( ball ` ( abs o. - ) ) r ) i^i X ) <-> ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) = ( ( 0 ( ball ` ( abs o. - ) ) r ) i^i X ) ) )
65	64	rexbidv 2893	. . . . . . . . . 10 |- ( u = ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) -> ( E. r e. RR+ u = ( ( 0 ( ball ` ( abs o. - ) ) r ) i^i X ) <-> E. r e. RR+ ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) = ( ( 0 ( ball ` ( abs o. - ) ) r ) i^i X ) ) )
66	63, 65	anbi12d 708	. . . . . . . . 9 |- ( u = ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) -> ( ( x e. u /\ E. r e. RR+ u = ( ( 0 ( ball ` ( abs o. - ) ) r ) i^i X ) ) <-> ( x e. ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) /\ E. r e. RR+ ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) = ( ( 0 ( ball ` ( abs o. - ) ) r ) i^i X ) ) ) )
67	66	rspcev 3135	. . . . . . . 8 |- ( ( ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) e. T /\ ( x e. ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) /\ E. r e. RR+ ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) = ( ( 0 ( ball ` ( abs o. - ) ) r ) i^i X ) ) ) -> E. u e. T ( x e. u /\ E. r e. RR+ u = ( ( 0 ( ball ` ( abs o. - ) ) r ) i^i X ) ) )
68	37, 54, 62, 67	syl12anc 1224	. . . . . . 7 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> E. u e. T ( x e. u /\ E. r e. RR+ u = ( ( 0 ( ball ` ( abs o. - ) ) r ) i^i X ) ) )
69	18, 68	syldan 468	. . . . . 6 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. U. T ) -> E. u e. T ( x e. u /\ E. r e. RR+ u = ( ( 0 ( ball ` ( abs o. - ) ) r ) i^i X ) ) )
70	69	ralrimiva 2796	. . . . 5 |- ( ( X C_ CC /\ T e. Comp ) -> A. x e. U. T E. u e. T ( x e. u /\ E. r e. RR+ u = ( ( 0 ( ball ` ( abs o. - ) ) r ) i^i X ) ) )
71		eqid 2382	. . . . . 6 |- U. T = U. T
72		oveq2 6204	. . . . . . . 8 |- ( r = ( f ` u ) -> ( 0 ( ball ` ( abs o. - ) ) r ) = ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) )
73	72	ineq1d 3613	. . . . . . 7 |- ( r = ( f ` u ) -> ( ( 0 ( ball ` ( abs o. - ) ) r ) i^i X ) = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) )
74	73	eqeq2d 2396	. . . . . 6 |- ( r = ( f ` u ) -> ( u = ( ( 0 ( ball ` ( abs o. - ) ) r ) i^i X ) <-> u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) )
75	71, 74	cmpcovf 19977	. . . . 5 |- ( ( T e. Comp /\ A. x e. U. T E. u e. T ( x e. u /\ E. r e. RR+ u = ( ( 0 ( ball ` ( abs o. - ) ) r ) i^i X ) ) ) -> E. s e. ( ~P T i^i Fin ) ( U. T = U. s /\ E. f ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) )
76	6, 70, 75	syl2anc 659	. . . 4 |- ( ( X C_ CC /\ T e. Comp ) -> E. s e. ( ~P T i^i Fin ) ( U. T = U. s /\ E. f ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) )
77	16	ad4antr 729	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) -> X = U. T )
78		simpllr 758	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) -> U. T = U. s )
79	77, 78	eqtrd 2423	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) -> X = U. s )
80	79	eleq2d 2452	. . . . . . . . . . . 12 |- ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) -> ( x e. X <-> x e. U. s ) )
81		eluni2 4167	. . . . . . . . . . . 12 |- ( x e. U. s <-> E. z e. s x e. z )
82	80, 81	syl6bb 261	. . . . . . . . . . 11 |- ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) -> ( x e. X <-> E. z e. s x e. z ) )
83		elssuni 4192	. . . . . . . . . . . . . . . . . 18 |- ( z e. s -> z C_ U. s )
84	83	ad2antrl 725	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> z C_ U. s )
85	79	adantr 463	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> X = U. s )
86	84, 85	sseqtr4d 3454	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> z C_ X )
87		simp-6l 769	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> X C_ CC )
88	86, 87	sstrd 3427	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> z C_ CC )
89		simprr 755	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> x e. z )
90	88, 89	sseldd 3418	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> x e. CC )
91	90	abscld 13269	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> ( abs ` x ) e. RR )
92		simplrl 759	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> r e. RR )
93		simprl 754	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) -> f : s --> RR+ )
94	93	ad2antrr 723	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> f : s --> RR+ )
95		simprl 754	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> z e. s )
96	94, 95	ffvelrnd 5934	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> ( f ` z ) e. RR+ )
97	96	rpred 11177	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> ( f ` z ) e. RR )
98	90, 46	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> ( 0 ( abs o. - ) x ) = ( abs ` x ) )
99		inss1 3632	. . . . . . . . . . . . . . . . . 18 |- ( ( 0 ( ball ` ( abs o. - ) ) ( f ` z ) ) i^i X ) C_ ( 0 ( ball ` ( abs o. - ) ) ( f ` z ) )
100		simprr 755	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) -> A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) )
101	100	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) )
102		id 22	. . . . . . . . . . . . . . . . . . . . . 22 |- ( u = z -> u = z )
103		fveq2 5774	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( u = z -> ( f ` u ) = ( f ` z ) )
104	103	oveq2d 6212	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( u = z -> ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) = ( 0 ( ball ` ( abs o. - ) ) ( f ` z ) ) )
105	104	ineq1d 3613	. . . . . . . . . . . . . . . . . . . . . 22 |- ( u = z -> ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` z ) ) i^i X ) )
106	102, 105	eqeq12d 2404	. . . . . . . . . . . . . . . . . . . . 21 |- ( u = z -> ( u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) <-> z = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` z ) ) i^i X ) ) )
107	106	rspcv 3131	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. s -> ( A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) -> z = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` z ) ) i^i X ) ) )
108	95, 101, 107	sylc 60	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> z = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` z ) ) i^i X ) )
109	89, 108	eleqtrd 2472	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> x e. ( ( 0 ( ball ` ( abs o. - ) ) ( f ` z ) ) i^i X ) )
110	99, 109	sseldi 3415	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> x e. ( 0 ( ball ` ( abs o. - ) ) ( f ` z ) ) )
111	24	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> ( abs o. - ) e. ( *Met ` CC ) )
112		0cnd 9500	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> 0 e. CC )
113	96	rpxrd 11178	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> ( f ` z ) e. RR* )
114		elbl 20976	. . . . . . . . . . . . . . . . . 18 |- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ ( f ` z ) e. RR* ) -> ( x e. ( 0 ( ball ` ( abs o. - ) ) ( f ` z ) ) <-> ( x e. CC /\ ( 0 ( abs o. - ) x ) < ( f ` z ) ) ) )
115	111, 112, 113, 114	syl3anc 1226	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> ( x e. ( 0 ( ball ` ( abs o. - ) ) ( f ` z ) ) <-> ( x e. CC /\ ( 0 ( abs o. - ) x ) < ( f ` z ) ) ) )
116	110, 115	mpbid 210	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> ( x e. CC /\ ( 0 ( abs o. - ) x ) < ( f ` z ) ) )
117	116	simprd 461	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> ( 0 ( abs o. - ) x ) < ( f ` z ) )
118	98, 117	eqbrtrrd 4389	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> ( abs ` x ) < ( f ` z ) )
119		simplrr 760	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> A. u e. s ( f ` u ) <_ r )
120	103	breq1d 4377	. . . . . . . . . . . . . . . 16 |- ( u = z -> ( ( f ` u ) <_ r <-> ( f ` z ) <_ r ) )
121	120	rspcv 3131	. . . . . . . . . . . . . . 15 |- ( z e. s -> ( A. u e. s ( f ` u ) <_ r -> ( f ` z ) <_ r ) )
122	95, 119, 121	sylc 60	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> ( f ` z ) <_ r )
123	91, 97, 92, 118, 122	ltletrd 9653	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> ( abs ` x ) < r )
124	91, 92, 123	ltled 9644	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) /\ ( z e. s /\ x e. z ) ) -> ( abs ` x ) <_ r )
125	124	rexlimdvaa 2875	. . . . . . . . . . 11 |- ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) -> ( E. z e. s x e. z -> ( abs ` x ) <_ r ) )
126	82, 125	sylbid 215	. . . . . . . . . 10 |- ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) -> ( x e. X -> ( abs ` x ) <_ r ) )
127	126	ralrimiv 2794	. . . . . . . . 9 |- ( ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) /\ ( r e. RR /\ A. u e. s ( f ` u ) <_ r ) ) -> A. x e. X ( abs ` x ) <_ r )
128		inss2 3633	. . . . . . . . . . 11 |- ( ~P T i^i Fin ) C_ Fin
129		simpllr 758	. . . . . . . . . . 11 |- ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) -> s e. ( ~P T i^i Fin ) )
130	128, 129	sseldi 3415	. . . . . . . . . 10 |- ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) -> s e. Fin )
131		ffvelrn 5931	. . . . . . . . . . . . 13 |- ( ( f : s --> RR+ /\ u e. s ) -> ( f ` u ) e. RR+ )
132	131	rpred 11177	. . . . . . . . . . . 12 |- ( ( f : s --> RR+ /\ u e. s ) -> ( f ` u ) e. RR )
133	132	ralrimiva 2796	. . . . . . . . . . 11 |- ( f : s --> RR+ -> A. u e. s ( f ` u ) e. RR )
134	133	ad2antrl 725	. . . . . . . . . 10 |- ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) -> A. u e. s ( f ` u ) e. RR )
135		fimaxre3 10408	. . . . . . . . . 10 |- ( ( s e. Fin /\ A. u e. s ( f ` u ) e. RR ) -> E. r e. RR A. u e. s ( f ` u ) <_ r )
136	130, 134, 135	syl2anc 659	. . . . . . . . 9 |- ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) -> E. r e. RR A. u e. s ( f ` u ) <_ r )
137	127, 136	reximddv 2858	. . . . . . . 8 |- ( ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) /\ ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) -> E. r e. RR A. x e. X ( abs ` x ) <_ r )
138	137	ex 432	. . . . . . 7 |- ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) -> ( ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) -> E. r e. RR A. x e. X ( abs ` x ) <_ r ) )
139	138	exlimdv 1732	. . . . . 6 |- ( ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) /\ U. T = U. s ) -> ( E. f ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) -> E. r e. RR A. x e. X ( abs ` x ) <_ r ) )
140	139	expimpd 601	. . . . 5 |- ( ( ( X C_ CC /\ T e. Comp ) /\ s e. ( ~P T i^i Fin ) ) -> ( ( U. T = U. s /\ E. f ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) -> E. r e. RR A. x e. X ( abs ` x ) <_ r ) )
141	140	rexlimdva 2874	. . . 4 |- ( ( X C_ CC /\ T e. Comp ) -> ( E. s e. ( ~P T i^i Fin ) ( U. T = U. s /\ E. f ( f : s --> RR+ /\ A. u e. s u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) ) -> E. r e. RR A. x e. X ( abs ` x ) <_ r ) )
142	76, 141	mpd 15	. . 3 |- ( ( X C_ CC /\ T e. Comp ) -> E. r e. RR A. x e. X ( abs ` x ) <_ r )
143	11, 142	jca 530	. 2 |- ( ( X C_ CC /\ T e. Comp ) -> ( X e. ( Clsd ` J ) /\ E. r e. RR A. x e. X ( abs ` x ) <_ r ) )
144		eqid 2382	. . . . . 6 |- ( y e. RR , z e. RR |-> ( y + ( _i x. z ) ) ) = ( y e. RR , z e. RR |-> ( y + ( _i x. z ) ) )
145		eqid 2382	. . . . . 6 |- ( ( y e. RR , z e. RR |-> ( y + ( _i x. z ) ) ) " ( ( -u r [,] r ) X. ( -u r [,] r ) ) ) = ( ( y e. RR , z e. RR |-> ( y + ( _i x. z ) ) ) " ( ( -u r [,] r ) X. ( -u r [,] r ) ) )
146	1, 5, 144, 145	cnheiborlem 21539	. . . . 5 |- ( ( X e. ( Clsd ` J ) /\ ( r e. RR /\ A. x e. X ( abs ` x ) <_ r ) ) -> T e. Comp )
147	146	rexlimdvaa 2875	. . . 4 |- ( X e. ( Clsd ` J ) -> ( E. r e. RR A. x e. X ( abs ` x ) <_ r -> T e. Comp ) )
148	147	imp 427	. . 3 |- ( ( X e. ( Clsd ` J ) /\ E. r e. RR A. x e. X ( abs ` x ) <_ r ) -> T e. Comp )
149	148	adantl 464	. 2 |- ( ( X C_ CC /\ ( X e. ( Clsd ` J ) /\ E. r e. RR A. x e. X ( abs ` x ) <_ r ) ) -> T e. Comp )
150	143, 149	impbida 830	1 |- ( X C_ CC -> ( T e. Comp <-> ( X e. ( Clsd ` J ) /\ E. r e. RR A. x e. X ( abs ` x ) <_ r ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 367   = wceq 1399   E.wex 1620   e. wcel 1826   A.wral 2732   E.wrex 2733   _Vcvv 3034   i^i cin 3388   C_ wss 3389   ~Pcpw 3927   U.cuni 4163   class class class wbr 4367   X. cxp 4911   "cima 4916   o. ccom 4917   -->wf 5492   ` cfv 5496  (class class class)co 6196   |-> cmpt2 6198   Fincfn 7435   CCcc 9401   RRcr 9402   0cc0 9403   1c1 9404   _ici 9405   + caddc 9406   x. cmul 9408   RR*cxr 9538   < clt 9539   <_ cle 9540   - cmin 9718   -ucneg 9719   RR+crp 11139   [,]cicc 11453   abscabs 13069   ↾_t crest 14828   TopOpenctopn 14829   *Metcxmt 18516   ballcbl 18518  ℂ_fldccnfld 18533   Topctop 19479   Clsdccld 19602   Hauscha 19895   Compccmp 19972

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-rep 4478  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491  ax-inf2 7972  ax-cnex 9459  ax-resscn 9460  ax-1cn 9461  ax-icn 9462  ax-addcl 9463  ax-addrcl 9464  ax-mulcl 9465  ax-mulrcl 9466  ax-mulcom 9467  ax-addass 9468  ax-mulass 9469  ax-distr 9470  ax-i2m1 9471  ax-1ne0 9472  ax-1rid 9473  ax-rnegex 9474  ax-rrecex 9475  ax-cnre 9476  ax-pre-lttri 9477  ax-pre-lttrn 9478  ax-pre-ltadd 9479  ax-pre-mulgt0 9480  ax-pre-sup 9481  ax-addf 9482  ax-mulf 9483

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-nel 2580  df-ral 2737  df-rex 2738  df-reu 2739  df-rmo 2740  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-pss 3405  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-tp 3949  df-op 3951  df-uni 4164  df-int 4200  df-iun 4245  df-iin 4246  df-br 4368  df-opab 4426  df-mpt 4427  df-tr 4461  df-eprel 4705  df-id 4709  df-po 4714  df-so 4715  df-fr 4752  df-se 4753  df-we 4754  df-ord 4795  df-on 4796  df-lim 4797  df-suc 4798  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-isom 5505  df-riota 6158  df-ov 6199  df-oprab 6200  df-mpt2 6201  df-of 6439  df-om 6600  df-1st 6699  df-2nd 6700  df-supp 6818  df-recs 6960  df-rdg 6994  df-1o 7048  df-2o 7049  df-oadd 7052  df-er 7229  df-map 7340  df-ixp 7389  df-en 7436  df-dom 7437  df-sdom 7438  df-fin 7439  df-fsupp 7745  df-fi 7786  df-sup 7816  df-oi 7850  df-card 8233  df-cda 8461  df-pnf 9541  df-mnf 9542  df-xr 9543  df-ltxr 9544  df-le 9545  df-sub 9720  df-neg 9721  df-div 10124  df-nn 10453  df-2 10511  df-3 10512  df-4 10513  df-5 10514  df-6 10515  df-7 10516  df-8 10517  df-9 10518  df-10 10519  df-n0 10713  df-z 10782  df-dec 10896  df-uz 11002  df-q 11102  df-rp 11140  df-xneg 11239  df-xadd 11240  df-xmul 11241  df-ioo 11454  df-icc 11457  df-fz 11594  df-fzo 11718  df-seq 12011  df-exp 12070  df-hash 12308  df-cj 12934  df-re 12935  df-im 12936  df-sqrt 13070  df-abs 13071  df-struct 14636  df-ndx 14637  df-slot 14638  df-base 14639  df-sets 14640  df-ress 14641  df-plusg 14715  df-mulr 14716  df-starv 14717  df-sca 14718  df-vsca 14719  df-ip 14720  df-tset 14721  df-ple 14722  df-ds 14724  df-unif 14725  df-hom 14726  df-cco 14727  df-rest 14830  df-topn 14831  df-0g 14849  df-gsum 14850  df-topgen 14851  df-pt 14852  df-prds 14855  df-xrs 14909  df-qtop 14914  df-imas 14915  df-xps 14917  df-mre 14993  df-mrc 14994  df-acs 14996  df-mgm 15989  df-sgrp 16028  df-mnd 16038  df-submnd 16084  df-mulg 16177  df-cntz 16472  df-cmn 16917  df-psmet 18524  df-xmet 18525  df-met 18526  df-bl 18527  df-mopn 18528  df-cnfld 18534  df-top 19484  df-bases 19486  df-topon 19487  df-topsp 19488  df-cld 19605  df-cls 19607  df-cn 19814  df-cnp 19815  df-haus 19902  df-cmp 19973  df-tx 20148  df-hmeo 20341  df-xms 20908  df-ms 20909  df-tms 20910  df-cncf 21467

This theorem is referenced by:  cnllycmp  21541  cncmet  21846  ftalem3  23465