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 β€˜ π‘₯ ) ≀ π‘Ÿ ) ) )