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 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 ‘ 𝑥 ) ≤ 𝑟 ) ) )