This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
cnheibor.3 ⊢ 𝑇 = ( 𝐽 ↾t 𝑋 )
Assertion cnheibor ( 𝑋 ⊆ ℂ → ( 𝑇 ∈ Comp ↔ ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ∃ 𝑟 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ( abs ‘ 𝑥 ) ≤ 𝑟 ) ) )

Proof

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 eqtr3id ⊢ ( 𝑥 ∈ ℂ → ( 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 ffvelcdmd ⊢ ( ( ( ( ( ( ( 𝑋 ⊆ ℂ ∧ 𝑇 ∈ 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 ffvelcdm ⊢ ( ( 𝑓 : 𝑠 ⟶ ℝ+ ∧ 𝑢 ∈ 𝑠 ) → ( 𝑓 ‘ 𝑢 ) ∈ ℝ+ )
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 ‘ 𝑥 ) ≤ 𝑟 ) ) )