Metamath Proof Explorer


Theorem cnheibor

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)

Ref Expression
Hypotheses cnheibor.2
|- J = ( TopOpen ` CCfld )
cnheibor.3
|- T = ( J |`t X )
Assertion cnheibor
|- ( X C_ CC -> ( T e. Comp <-> ( X e. ( Clsd ` J ) /\ E. r e. RR A. x e. X ( abs ` x ) <_ r ) ) )

Proof

Step Hyp Ref Expression
1 cnheibor.2
 |-  J = ( TopOpen ` CCfld )
2 cnheibor.3
 |-  T = ( J |`t X )
3 1 cnfldhaus
 |-  J e. Haus
4 simpl
 |-  ( ( X C_ CC /\ T e. Comp ) -> X C_ CC )
5 simpr
 |-  ( ( X C_ CC /\ T e. Comp ) -> T e. Comp )
6 2 5 eqeltrrid
 |-  ( ( X C_ CC /\ T e. Comp ) -> ( J |`t X ) e. Comp )
7 1 cnfldtopon
 |-  J e. ( TopOn ` CC )
8 7 toponunii
 |-  CC = U. J
9 8 hauscmp
 |-  ( ( J e. Haus /\ X C_ CC /\ ( J |`t X ) e. Comp ) -> X e. ( Clsd ` J ) )
10 3 4 6 9 mp3an2i
 |-  ( ( X C_ CC /\ T e. Comp ) -> X e. ( Clsd ` J ) )
11 1 cnfldtop
 |-  J e. Top
12 8 restuni
 |-  ( ( J e. Top /\ X C_ CC ) -> X = U. ( J |`t X ) )
13 11 4 12 sylancr
 |-  ( ( X C_ CC /\ T e. Comp ) -> X = U. ( J |`t X ) )
14 2 unieqi
 |-  U. T = U. ( J |`t X )
15 13 14 eqtr4di
 |-  ( ( X C_ CC /\ T e. Comp ) -> X = U. T )
16 15 eleq2d
 |-  ( ( X C_ CC /\ T e. Comp ) -> ( x e. X <-> x e. U. T ) )
17 16 biimpar
 |-  ( ( ( X C_ CC /\ T e. Comp ) /\ x e. U. T ) -> x e. X )
18 cnex
 |-  CC e. _V
19 ssexg
 |-  ( ( X C_ CC /\ CC e. _V ) -> X e. _V )
20 4 18 19 sylancl
 |-  ( ( X C_ CC /\ T e. Comp ) -> X e. _V )
21 20 adantr
 |-  ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> X e. _V )
22 cnxmet
 |-  ( abs o. - ) e. ( *Met ` CC )
23 0cnd
 |-  ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> 0 e. CC )
24 4 sselda
 |-  ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> x e. CC )
25 24 abscld
 |-  ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( abs ` x ) e. RR )
26 peano2re
 |-  ( ( abs ` x ) e. RR -> ( ( abs ` x ) + 1 ) e. RR )
27 25 26 syl
 |-  ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( ( abs ` x ) + 1 ) e. RR )
28 27 rexrd
 |-  ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( ( abs ` x ) + 1 ) e. RR* )
29 1 cnfldtopn
 |-  J = ( MetOpen ` ( abs o. - ) )
30 29 blopn
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ ( ( abs ` x ) + 1 ) e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) e. J )
31 22 23 28 30 mp3an2i
 |-  ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) e. J )
32 elrestr
 |-  ( ( 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 ) )
33 11 21 31 32 mp3an2i
 |-  ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) e. ( J |`t X ) )
34 33 2 eleqtrrdi
 |-  ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) e. T )
35 0cn
 |-  0 e. CC
36 eqid
 |-  ( abs o. - ) = ( abs o. - )
37 36 cnmetdval
 |-  ( ( 0 e. CC /\ x e. CC ) -> ( 0 ( abs o. - ) x ) = ( abs ` ( 0 - x ) ) )
38 35 37 mpan
 |-  ( x e. CC -> ( 0 ( abs o. - ) x ) = ( abs ` ( 0 - x ) ) )
39 df-neg
 |-  -u x = ( 0 - x )
40 39 fveq2i
 |-  ( abs ` -u x ) = ( abs ` ( 0 - x ) )
41 absneg
 |-  ( x e. CC -> ( abs ` -u x ) = ( abs ` x ) )
42 40 41 eqtr3id
 |-  ( x e. CC -> ( abs ` ( 0 - x ) ) = ( abs ` x ) )
43 38 42 eqtrd
 |-  ( x e. CC -> ( 0 ( abs o. - ) x ) = ( abs ` x ) )
44 24 43 syl
 |-  ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( 0 ( abs o. - ) x ) = ( abs ` x ) )
45 25 ltp1d
 |-  ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( abs ` x ) < ( ( abs ` x ) + 1 ) )
46 44 45 eqbrtrd
 |-  ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( 0 ( abs o. - ) x ) < ( ( abs ` x ) + 1 ) )
47 elbl
 |-  ( ( ( 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 ) ) ) )
48 22 23 28 47 mp3an2i
 |-  ( ( ( 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 ) ) ) )
49 24 46 48 mpbir2and
 |-  ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> x e. ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) )
50 simpr
 |-  ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> x e. X )
51 49 50 elind
 |-  ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> x e. ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) )
52 24 absge0d
 |-  ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> 0 <_ ( abs ` x ) )
53 25 52 ge0p1rpd
 |-  ( ( ( X C_ CC /\ T e. Comp ) /\ x e. X ) -> ( ( abs ` x ) + 1 ) e. RR+ )
54 eqid
 |-  ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) = ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X )
55 oveq2
 |-  ( r = ( ( abs ` x ) + 1 ) -> ( 0 ( ball ` ( abs o. - ) ) r ) = ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) )
56 55 ineq1d
 |-  ( r = ( ( abs ` x ) + 1 ) -> ( ( 0 ( ball ` ( abs o. - ) ) r ) i^i X ) = ( ( 0 ( ball ` ( abs o. - ) ) ( ( abs ` x ) + 1 ) ) i^i X ) )
57 56 rspceeqv
 |-  ( ( ( ( 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 ) )
58 53 54 57 sylancl
 |-  ( ( ( 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 ) )
59 eleq2
 |-  ( 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 ) ) )
60 eqeq1
 |-  ( 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 ) ) )
61 60 rexbidv
 |-  ( 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 ) ) )
62 59 61 anbi12d
 |-  ( 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 ) ) ) )
63 62 rspcev
 |-  ( ( ( ( 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 ) ) )
64 34 51 58 63 syl12anc
 |-  ( ( ( 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 ) ) )
65 17 64 syldan
 |-  ( ( ( 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 ) ) )
66 65 ralrimiva
 |-  ( ( 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 ) ) )
67 eqid
 |-  U. T = U. T
68 oveq2
 |-  ( r = ( f ` u ) -> ( 0 ( ball ` ( abs o. - ) ) r ) = ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) )
69 68 ineq1d
 |-  ( r = ( f ` u ) -> ( ( 0 ( ball ` ( abs o. - ) ) r ) i^i X ) = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) )
70 69 eqeq2d
 |-  ( r = ( f ` u ) -> ( u = ( ( 0 ( ball ` ( abs o. - ) ) r ) i^i X ) <-> u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) ) )
71 67 70 cmpcovf
 |-  ( ( 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 ) ) ) )
72 5 66 71 syl2anc
 |-  ( ( 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 ) ) ) )
73 15 ad4antr
 |-  ( ( ( ( ( ( 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 )
74 simpllr
 |-  ( ( ( ( ( ( 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 )
75 73 74 eqtrd
 |-  ( ( ( ( ( ( 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 )
76 75 eleq2d
 |-  ( ( ( ( ( ( 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 ) )
77 eluni2
 |-  ( x e. U. s <-> E. z e. s x e. z )
78 76 77 bitrdi
 |-  ( ( ( ( ( ( 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 ) )
79 elssuni
 |-  ( z e. s -> z C_ U. s )
80 79 ad2antrl
 |-  ( ( ( ( ( ( ( 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 )
81 75 adantr
 |-  ( ( ( ( ( ( ( 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 )
82 80 81 sseqtrrd
 |-  ( ( ( ( ( ( ( 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 )
83 simp-6l
 |-  ( ( ( ( ( ( ( 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 )
84 82 83 sstrd
 |-  ( ( ( ( ( ( ( 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 )
85 simprr
 |-  ( ( ( ( ( ( ( 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 )
86 84 85 sseldd
 |-  ( ( ( ( ( ( ( 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 )
87 86 abscld
 |-  ( ( ( ( ( ( ( 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 )
88 simplrl
 |-  ( ( ( ( ( ( ( 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 )
89 simprl
 |-  ( ( ( ( ( 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+ )
90 89 ad2antrr
 |-  ( ( ( ( ( ( ( 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+ )
91 simprl
 |-  ( ( ( ( ( ( ( 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 )
92 90 91 ffvelrnd
 |-  ( ( ( ( ( ( ( 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+ )
93 92 rpred
 |-  ( ( ( ( ( ( ( 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 )
94 86 43 syl
 |-  ( ( ( ( ( ( ( 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 ) )
95 id
 |-  ( u = z -> u = z )
96 fveq2
 |-  ( u = z -> ( f ` u ) = ( f ` z ) )
97 96 oveq2d
 |-  ( u = z -> ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) = ( 0 ( ball ` ( abs o. - ) ) ( f ` z ) ) )
98 97 ineq1d
 |-  ( u = z -> ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` z ) ) i^i X ) )
99 95 98 eqeq12d
 |-  ( u = z -> ( u = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` u ) ) i^i X ) <-> z = ( ( 0 ( ball ` ( abs o. - ) ) ( f ` z ) ) i^i X ) ) )
100 simprr
 |-  ( ( ( ( ( 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
 |-  ( ( ( ( ( ( ( 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 99 101 91 rspcdva
 |-  ( ( ( ( ( ( ( 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 ) )
103 85 102 eleqtrd
 |-  ( ( ( ( ( ( ( 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 ) )
104 103 elin1d
 |-  ( ( ( ( ( ( ( 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 ) ) )
105 0cnd
 |-  ( ( ( ( ( ( ( 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 )
106 92 rpxrd
 |-  ( ( ( ( ( ( ( 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 elbl
 |-  ( ( ( 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 ) ) ) )
108 22 105 106 107 mp3an2i
 |-  ( ( ( ( ( ( ( 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 ) ) ) )
109 104 108 mpbid
 |-  ( ( ( ( ( ( ( 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 ) ) )
110 109 simprd
 |-  ( ( ( ( ( ( ( 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 ) )
111 94 110 eqbrtrrd
 |-  ( ( ( ( ( ( ( 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 ) )
112 96 breq1d
 |-  ( u = z -> ( ( f ` u ) <_ r <-> ( f ` z ) <_ r ) )
113 simplrr
 |-  ( ( ( ( ( ( ( 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 )
114 112 113 91 rspcdva
 |-  ( ( ( ( ( ( ( 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 )
115 87 93 88 111 114 ltletrd
 |-  ( ( ( ( ( ( ( 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 )
116 87 88 115 ltled
 |-  ( ( ( ( ( ( ( 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 )
117 116 rexlimdvaa
 |-  ( ( ( ( ( ( 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 ) )
118 78 117 sylbid
 |-  ( ( ( ( ( ( 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 ) )
119 118 ralrimiv
 |-  ( ( ( ( ( ( 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 )
120 simpllr
 |-  ( ( ( ( ( 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 ) )
121 120 elin2d
 |-  ( ( ( ( ( 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 )
122 ffvelrn
 |-  ( ( f : s --> RR+ /\ u e. s ) -> ( f ` u ) e. RR+ )
123 122 rpred
 |-  ( ( f : s --> RR+ /\ u e. s ) -> ( f ` u ) e. RR )
124 123 ralrimiva
 |-  ( f : s --> RR+ -> A. u e. s ( f ` u ) e. RR )
125 124 ad2antrl
 |-  ( ( ( ( ( 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 )
126 fimaxre3
 |-  ( ( s e. Fin /\ A. u e. s ( f ` u ) e. RR ) -> E. r e. RR A. u e. s ( f ` u ) <_ r )
127 121 125 126 syl2anc
 |-  ( ( ( ( ( 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 )
128 119 127 reximddv
 |-  ( ( ( ( ( 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 )
129 128 ex
 |-  ( ( ( ( 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 ) )
130 129 exlimdv
 |-  ( ( ( ( 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 ) )
131 130 expimpd
 |-  ( ( ( 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 ) )
132 131 rexlimdva
 |-  ( ( 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 ) )
133 72 132 mpd
 |-  ( ( X C_ CC /\ T e. Comp ) -> E. r e. RR A. x e. X ( abs ` x ) <_ r )
134 10 133 jca
 |-  ( ( X C_ CC /\ T e. Comp ) -> ( X e. ( Clsd ` J ) /\ E. r e. RR A. x e. X ( abs ` x ) <_ r ) )
135 eqid
 |-  ( y e. RR , z e. RR |-> ( y + ( _i x. z ) ) ) = ( y e. RR , z e. RR |-> ( y + ( _i x. z ) ) )
136 eqid
 |-  ( ( 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 ) ) )
137 1 2 135 136 cnheiborlem
 |-  ( ( X e. ( Clsd ` J ) /\ ( r e. RR /\ A. x e. X ( abs ` x ) <_ r ) ) -> T e. Comp )
138 137 rexlimdvaa
 |-  ( X e. ( Clsd ` J ) -> ( E. r e. RR A. x e. X ( abs ` x ) <_ r -> T e. Comp ) )
139 138 imp
 |-  ( ( X e. ( Clsd ` J ) /\ E. r e. RR A. x e. X ( abs ` x ) <_ r ) -> T e. Comp )
140 139 adantl
 |-  ( ( X C_ CC /\ ( X e. ( Clsd ` J ) /\ E. r e. RR A. x e. X ( abs ` x ) <_ r ) ) -> T e. Comp )
141 134 140 impbida
 |-  ( X C_ CC -> ( T e. Comp <-> ( X e. ( Clsd ` J ) /\ E. r e. RR A. x e. X ( abs ` x ) <_ r ) ) )