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