Theorem cnheibor 20658

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 20495	. . . . 5 |- J e. Haus
3	2	a1i 11	. . . 4 |- ( ( X C_ CC /\ T e. Comp ) -> J e. Haus )
4		simpl 457	. . . 4 |- ( ( X C_ CC /\ T e. Comp ) -> X C_ CC )
5		cnheibor.3	. . . . 5 |- T = ( J ↾t X )
6		simpr 461	. . . . 5 |- ( ( X C_ CC /\ T e. Comp ) -> T e. Comp )
7	5, 6	syl5eqelr 2547	. . . 4 |- ( ( X C_ CC /\ T e. Comp ) -> ( J ↾t X ) e. Comp )
8	1	cnfldtopon 20493	. . . . . 6 |- J e. (TopOn ` CC )
9	8	toponunii 18668	. . . . 5 |- CC = U. J
10	9	hauscmp 19141	. . . 4 |- ( ( J e. Haus /\ X C_ CC /\ ( J ↾t X ) e. Comp ) -> X e. ( Clsd ` J ) )
11	3, 4, 7, 10	syl3anc 1219	. . 3 |- ( ( X C_ CC /\ T e. Comp ) -> X e. ( Clsd ` J ) )
12	1	cnfldtop 20494	. . . . . . . . . . 11 |- J e. Top
13	9	restuni 18897	. . . . . . . . . . 11 |- ( ( J e. Top /\ X C_ CC ) -> X = U. ( J ↾t X ) )
14	12, 4, 13	sylancr 663	. . . . . . . . . 10 |- ( ( X C_ CC /\ T e. Comp ) -> X = U. ( J ↾t X ) )
15	5	unieqi 4207	. . . . . . . . . 10 |- U. T = U. ( J ↾t X )
16	14, 15	syl6eqr 2513	. . . . . . . . 9 |- ( ( X C_ CC /\ T e. Comp ) -> X = U. T )
17	16	eleq2d 2524	. . . . . . . 8 |- ( ( X C_ CC /\ T e. Comp ) -> ( x e. X <-> x e. U. T ) )
18	17	biimpar 485	. . . . . . 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 9473	. . . . . . . . . . . 12 |- CC e. _V
21		ssexg 4545	. . . . . . . . . . . 12 |- ( ( X C_ CC /\ CC e. _V ) -> X e. _V )
22	4, 20, 21	sylancl 662	. . . . . . . . . . 11 |- ( ( X C_ CC /\ T e. Comp ) -> X e. _V )
23	22	adantr 465	. . . . . . . . . 10 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> X e. _V )
24		cnxmet 20483	. . . . . . . . . . . 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 9489	. . . . . . . . . . 11 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> 0 e. CC )
27	4	sselda 3463	. . . . . . . . . . . . . 14 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> x e. CC )
28	27	abscld 13039	. . . . . . . . . . . . 13 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( abs ` x ) e. RR )
29		peano2re 9652	. . . . . . . . . . . . 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 9543	. . . . . . . . . . 11 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( ( abs ` x ) + 1 ) e. RR* )
32	1	cnfldtopn 20492	. . . . . . . . . . . 12 |- J = ( MetOpen ` ( abs o. - ) )
33	32	blopn 20206	. . . . . . . . . . 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 1219	. . . . . . . . . 10 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) e. J )
35		elrestr 14485	. . . . . . . . . 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 1219	. . . . . . . . 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 2553	. . . . . . . 8 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) e. T )
38		0cn 9488	. . . . . . . . . . . . . 14 |- 0 e. CC
39		eqid 2454	. . . . . . . . . . . . . . 15 |- ( abs o. - ) = ( abs o. - )
40	39	cnmetdval 20481	. . . . . . . . . . . . . 14 |- ( ( 0 e. CC /\ x e. CC ) -> ( 0 ( abs o. - ) x ) = ( abs ` ( 0 - x ) ) )
41	38, 40	mpan 670	. . . . . . . . . . . . 13 |- ( x e. CC -> ( 0 ( abs o. - ) x ) = ( abs ` ( 0 - x ) ) )
42		df-neg 9708	. . . . . . . . . . . . . . 15 |- -u x = ( 0 - x )
43	42	fveq2i 5801	. . . . . . . . . . . . . 14 |- ( abs ` -u x ) = ( abs ` ( 0 - x ) )
44		absneg 12883	. . . . . . . . . . . . . 14 |- ( x e. CC -> ( abs ` -u x ) = ( abs ` x ) )
45	43, 44	syl5eqr 2509	. . . . . . . . . . . . 13 |- ( x e. CC -> ( abs ` ( 0 - x ) ) = ( abs ` x ) )
46	41, 45	eqtrd 2495	. . . . . . . . . . . 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 10373	. . . . . . . . . . 11 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( abs ` x ) < ( ( abs ` x ) + 1 ) )
49	47, 48	eqbrtrd 4419	. . . . . . . . . 10 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( 0 ( abs o. - ) x ) < ( ( abs ` x ) + 1 ) )
50		elbl 20094	. . . . . . . . . . 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 1219	. . . . . . . . . 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 913	. . . . . . . . 9 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> x e. ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) )
53		simpr 461	. . . . . . . . 9 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> x e. X )
54	52, 53	elind 3647	. . . . . . . 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 13047	. . . . . . . . . 10 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> 0 <_ ( abs ` x ) )
56	28, 55	ge0p1rpd 11163	. . . . . . . . 9 |- ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( ( abs ` x ) + 1 ) e. RR+ )
57		eqid 2454	. . . . . . . . 9 |- ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) = ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X )
58		oveq2 6207	. . . . . . . . . . . 12 |- ( r = ( ( abs ` x ) + 1 ) -> ( 0 ( ball ` ( abs o. - ) ) r ) = ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) )
59	58	ineq1d 3658	. . . . . . . . . . 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 2468	. . . . . . . . . 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 3177	. . . . . . . . 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 662	. . . . . . . 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 2527	. . . . . . . . . 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 2458	. . . . . . . . . . 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 2864	. . . . . . . . . 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 710	. . . . . . . . 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 3177	. . . . . . . 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 1217	. . . . . . 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 470	. . . . . 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 2829	. . . . 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 2454	. . . . . 6 |- U. T = U. T
72		oveq2 6207	. . . . . . . 8 |- ( r = ( f ` u ) -> ( 0 ( ball ` ( abs o. - ) ) r ) = ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) )
73	72	ineq1d 3658	. . . . . . 7 |- ( r = ( f ` u ) -> ( ( 0 ( ball ` ( abs o. - ) ) r ) i^i X ) = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) )
74	73	eqeq2d 2468	. . . . . 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 19125	. . . . 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 661	. . . 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		inss2 3678	. . . . . . . . . . 11 |- ( ~P T i^i Fin ) C_ Fin
78		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 ) )
79	77, 78	sseldi 3461	. . . . . . . . . 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 )
80		ffvelrn 5949	. . . . . . . . . . . . 13 |- ( ( f : s --> RR+ /\ u e. s ) -> ( f ` u ) e. RR+ )
81	80	rpred 11137	. . . . . . . . . . . 12 |- ( ( f : s --> RR+ /\ u e. s ) -> ( f ` u ) e. RR )
82	81	ralrimiva 2829	. . . . . . . . . . 11 |- ( f : s --> RR+ -> A. u e. s ( f ` u ) e. RR )
83	82	ad2antrl 727	. . . . . . . . . 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 )
84		fimaxre3 10389	. . . . . . . . . 10 |- ( ( s e. Fin /\ A. u e. s ( f ` u ) e. RR ) -> E. r e. RR A. u e. s ( f ` u ) <_ r )
85	79, 83, 84	syl2anc 661	. . . . . . . . 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 )
86	16	ad4antr 731	. . . . . . . . . . . . . . . 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 ) ) -> X = U. T )
87		simpllr 758	. . . . . . . . . . . . . . . 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 ) ) -> U. T = U. s )
88	86, 87	eqtrd 2495	. . . . . . . . . . . . . . 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 ) ) -> X = U. s )
89	88	eleq2d 2524	. . . . . . . . . . . . . 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 e. X <-> x e. U. s ) )
90		eluni2 4202	. . . . . . . . . . . . . 14 |- ( x e. U. s <-> E. z e. s x e. z )
91	89, 90	syl6bb 261	. . . . . . . . . . . . 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 e. X <-> E. z e. s x e. z ) )
92		elssuni 4228	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. s -> z C_ U. s )
93	92	ad2antrl 727	. . . . . . . . . . . . . . . . . . 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 C_ U. s )
94	88	adantr 465	. . . . . . . . . . . . . . . . . . 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 ) ) -> X = U. s )
95	93, 94	sseqtr4d 3500	. . . . . . . . . . . . . . . . . 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 ) ) -> z C_ X )
96		simp-6l 769	. . . . . . . . . . . . . . . . . 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 C_ CC )
97	95, 96	sstrd 3473	. . . . . . . . . . . . . . . . 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_ CC )
98		simprr 756	. . . . . . . . . . . . . . . . 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. z )
99	97, 98	sseldd 3464	. . . . . . . . . . . . . . . 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 )
100	99	abscld 13039	. . . . . . . . . . . . . . 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 ) ) -> ( abs ` x ) e. RR )
101		simplrl 759	. . . . . . . . . . . . . . 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 ) ) -> r e. RR )
102		simprl 755	. . . . . . . . . . . . . . . . . . 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 ) ) ) -> f : s --> RR+ )
103	102	ad2antrr 725	. . . . . . . . . . . . . . . . . 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 : s --> RR+ )
104		simprl 755	. . . . . . . . . . . . . . . . . 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 ) ) -> z e. s )
105	103, 104	ffvelrnd 5952	. . . . . . . . . . . . . . . . 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 ) ) -> ( f ` z ) e. RR+ )
106	105	rpred 11137	. . . . . . . . . . . . . . . 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 ` z ) e. RR )
107	99, 46	syl 16	. . . . . . . . . . . . . . . . 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 ) ) -> ( 0 ( abs o. - ) x ) = ( abs ` x ) )
108		inss1 3677	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 0 ( ball ` ( abs o. - ) ) ( f ` z ) ) i^i X ) C_ ( 0 ( ball ` ( abs o. - ) ) ( f ` z ) )
109		simprr 756	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( 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 ) )
110	109	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( 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 ) )
111		id 22	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( u = z -> u = z )
112		fveq2 5798	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( u = z -> ( f ` u ) = ( f ` z ) )
113	112	oveq2d 6215	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( u = z -> ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) = ( 0 ( ball ` ( abs o. - ) ) ( f ` z ) ) )
114	113	ineq1d 3658	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( u = z -> ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` z ) ) i^i X ) )
115	111, 114	eqeq12d 2476	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( u = z -> ( u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) <-> z = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` z ) ) i^i X ) ) )
116	115	rspcv 3173	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 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 ) ) )
117	104, 110, 116	sylc 60	. . . . . . . . . . . . . . . . . . . . 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 ) ) ) /\ ( 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 ) )
118	98, 117	eleqtrd 2544	. . . . . . . . . . . . . . . . . . . 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 ) ) -> x e. ( ( 0 ( ball ` ( abs o. - ) ) ( f ` z ) ) i^i X ) )
119	108, 118	sseldi 3461	. . . . . . . . . . . . . . . . . . 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 ) ) -> x e. ( 0 ( ball ` ( abs o. - ) ) ( f ` z ) ) )
120	24	a1i 11	. . . . . . . . . . . . . . . . . . . 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 ) ) -> ( abs o. - ) e. ( *Met ` CC ) )
121		0cnd 9489	. . . . . . . . . . . . . . . . . . . 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 ) ) -> 0 e. CC )
122	105	rpxrd 11138	. . . . . . . . . . . . . . . . . . . 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 ) ) -> ( f ` z ) e. RR* )
123		elbl 20094	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 ) ) ) )
124	120, 121, 122, 123	syl3anc 1219	. . . . . . . . . . . . . . . . . . 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 ) ) -> ( x e. ( 0 ( ball ` ( abs o. - ) ) ( f ` z ) ) <-> ( x e. CC /\ ( 0 ( abs o. - ) x ) < ( f ` z ) ) ) )
125	119, 124	mpbid 210	. . . . . . . . . . . . . . . . . 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. CC /\ ( 0 ( abs o. - ) x ) < ( f ` z ) ) )
126	125	simprd 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 ) ) -> ( 0 ( abs o. - ) x ) < ( f ` z ) )
127	107, 126	eqbrtrrd 4421	. . . . . . . . . . . . . . . 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 ) ) -> ( abs ` x ) < ( f ` z ) )
128		simplrr 760	. . . . . . . . . . . . . . . . 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 ) ) -> A. u e. s ( f ` u ) <_ r )
129	112	breq1d 4409	. . . . . . . . . . . . . . . . . 18 |- ( u = z -> ( ( f ` u ) <_ r <-> ( f ` z ) <_ r ) )
130	129	rspcv 3173	. . . . . . . . . . . . . . . . 17 |- ( z e. s -> ( A. u e. s ( f ` u ) <_ r -> ( f ` z ) <_ r ) )
131	104, 128, 130	sylc 60	. . . . . . . . . . . . . . . 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 ` z ) <_ r )
132	100, 106, 101, 127, 131	ltletrd 9641	. . . . . . . . . . . . . . 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 ) ) -> ( abs ` x ) < r )
133	100, 101, 132	ltled 9632	. . . . . . . . . . . . . 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 ) <_ r )
134	133	rexlimdvaa 2946	. . . . . . . . . . . . 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 ) ) -> ( E. z e. s x e. z -> ( abs ` x ) <_ r ) )
135	91, 134	sylbid 215	. . . . . . . . . . . 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 -> ( abs ` x ) <_ r ) )
136	135	ralrimiv 2827	. . . . . . . . . . 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 ) ) -> A. x e. X ( abs ` x ) <_ r )
137	136	expr 615	. . . . . . . . . 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 -> A. x e. X ( abs ` x ) <_ r ) )
138	137	reximdva 2932	. . . . . . . . 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 -> E. r e. RR A. x e. X ( abs ` x ) <_ r ) )
139	85, 138	mpd 15	. . . . . . . 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 )
140	139	ex 434	. . . . . . 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 ) )
141	140	exlimdv 1691	. . . . . 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 ) )
142	141	expimpd 603	. . . . 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 ) )
143	142	rexlimdva 2945	. . . 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 ) )
144	76, 143	mpd 15	. . 3 |- ( ( X C_ CC /\ T e. Comp ) -> E. r e. RR A. x e. X ( abs ` x ) <_ r )
145	11, 144	jca 532	. 2 |- ( ( X C_ CC /\ T e. Comp ) -> ( X e. ( Clsd ` J ) /\ E. r e. RR A. x e. X ( abs ` x ) <_ r ) )
146		eqid 2454	. . . . . 6 |- ( y e. RR , z e. RR |-> ( y + ( _i x. z ) ) ) = ( y e. RR , z e. RR |-> ( y + ( _i x. z ) ) )
147		eqid 2454	. . . . . 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 ) ) )
148	1, 5, 146, 147	cnheiborlem 20657	. . . . 5 |- ( ( X e. ( Clsd ` J ) /\ ( r e. RR /\ A. x e. X ( abs ` x ) <_ r ) ) -> T e. Comp )
149	148	rexlimdvaa 2946	. . . 4 |- ( X e. ( Clsd ` J ) -> ( E. r e. RR A. x e. X ( abs ` x ) <_ r -> T e. Comp ) )
150	149	imp 429	. . 3 |- ( ( X e. ( Clsd ` J ) /\ E. r e. RR A. x e. X ( abs ` x ) <_ r ) -> T e. Comp )
151	150	adantl 466	. 2 |- ( ( X C_ CC /\ ( X e. ( Clsd ` J ) /\ E. r e. RR A. x e. X ( abs ` x ) <_ r ) ) -> T e. Comp )
152	145, 151	impbida 828	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 369   = wceq 1370   E.wex 1587   e. wcel 1758   A.wral 2798   E.wrex 2799   _Vcvv 3076   i^i cin 3434   C_ wss 3435   ~Pcpw 3967   U.cuni 4198   class class class wbr 4399   X. cxp 4945   "cima 4950   o. ccom 4951   -->wf 5521   ` cfv 5525  (class class class)co 6199   |-> cmpt2 6201   Fincfn 7419   CCcc 9390   RRcr 9391   0cc0 9392   1c1 9393   _ici 9394   + caddc 9395   x. cmul 9397   RR*cxr 9527   < clt 9528   <_ cle 9529   - cmin 9705   -ucneg 9706   RR+crp 11101   [,]cicc 11413   abscabs 12840   ↾_t crest 14477   TopOpenctopn 14478   *Metcxmt 17925   ballcbl 17927  ℂ_fldccnfld 17942   Topctop 18629   Clsdccld 18751   Hauscha 19043   Compccmp 19120

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4510  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481  ax-inf2 7957  ax-cnex 9448  ax-resscn 9449  ax-1cn 9450  ax-icn 9451  ax-addcl 9452  ax-addrcl 9453  ax-mulcl 9454  ax-mulrcl 9455  ax-mulcom 9456  ax-addass 9457  ax-mulass 9458  ax-distr 9459  ax-i2m1 9460  ax-1ne0 9461  ax-1rid 9462  ax-rnegex 9463  ax-rrecex 9464  ax-cnre 9465  ax-pre-lttri 9466  ax-pre-lttrn 9467  ax-pre-ltadd 9468  ax-pre-mulgt0 9469  ax-pre-sup 9470  ax-addf 9471  ax-mulf 9472

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-nel 2650  df-ral 2803  df-rex 2804  df-reu 2805  df-rmo 2806  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-pss 3451  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-tp 3989  df-op 3991  df-uni 4199  df-int 4236  df-iun 4280  df-iin 4281  df-br 4400  df-opab 4458  df-mpt 4459  df-tr 4493  df-eprel 4739  df-id 4743  df-po 4748  df-so 4749  df-fr 4786  df-se 4787  df-we 4788  df-ord 4829  df-on 4830  df-lim 4831  df-suc 4832  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-isom 5534  df-riota 6160  df-ov 6202  df-oprab 6203  df-mpt2 6204  df-of 6429  df-om 6586  df-1st 6686  df-2nd 6687  df-supp 6800  df-recs 6941  df-rdg 6975  df-1o 7029  df-2o 7030  df-oadd 7033  df-er 7210  df-map 7325  df-ixp 7373  df-en 7420  df-dom 7421  df-sdom 7422  df-fin 7423  df-fsupp 7731  df-fi 7771  df-sup 7801  df-oi 7834  df-card 8219  df-cda 8447  df-pnf 9530  df-mnf 9531  df-xr 9532  df-ltxr 9533  df-le 9534  df-sub 9707  df-neg 9708  df-div 10104  df-nn 10433  df-2 10490  df-3 10491  df-4 10492  df-5 10493  df-6 10494  df-7 10495  df-8 10496  df-9 10497  df-10 10498  df-n0 10690  df-z 10757  df-dec 10866  df-uz 10972  df-q 11064  df-rp 11102  df-xneg 11199  df-xadd 11200  df-xmul 11201  df-ioo 11414  df-icc 11417  df-fz 11554  df-fzo 11665  df-seq 11923  df-exp 11982  df-hash 12220  df-cj 12705  df-re 12706  df-im 12707  df-sqr 12841  df-abs 12842  df-struct 14293  df-ndx 14294  df-slot 14295  df-base 14296  df-sets 14297  df-ress 14298  df-plusg 14369  df-mulr 14370  df-starv 14371  df-sca 14372  df-vsca 14373  df-ip 14374  df-tset 14375  df-ple 14376  df-ds 14378  df-unif 14379  df-hom 14380  df-cco 14381  df-rest 14479  df-topn 14480  df-0g 14498  df-gsum 14499  df-topgen 14500  df-pt 14501  df-prds 14504  df-xrs 14558  df-qtop 14563  df-imas 14564  df-xps 14566  df-mre 14642  df-mrc 14643  df-acs 14645  df-mnd 15533  df-submnd 15583  df-mulg 15666  df-cntz 15953  df-cmn 16399  df-psmet 17933  df-xmet 17934  df-met 17935  df-bl 17936  df-mopn 17937  df-cnfld 17943  df-top 18634  df-bases 18636  df-topon 18637  df-topsp 18638  df-cld 18754  df-cls 18756  df-cn 18962  df-cnp 18963  df-haus 19050  df-cmp 19121  df-tx 19266  df-hmeo 19459  df-xms 20026  df-ms 20027  df-tms 20028  df-cncf 20585

This theorem is referenced by:  cnllycmp  20659  cncmet  20964  ftalem3  22544