# 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 ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
cnheibor.3 ${⊢}{T}={J}{↾}_{𝑡}{X}$
Assertion cnheibor ${⊢}{X}\subseteq ℂ\to \left({T}\in \mathrm{Comp}↔\left({X}\in \mathrm{Clsd}\left({J}\right)\wedge \exists {r}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left|{x}\right|\le {r}\right)\right)$

### Proof

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