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
|
syl5eqr |
|- ( 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 ) ) ) |