Step | Hyp | Ref
| Expression |
1 | | cnheibor.2 |
. . . . . 6
⊢ 𝐽 =
(TopOpen‘ℂfld) |
2 | 1 | cnfldhaus 22398 |
. . . . 5
⊢ 𝐽 ∈ Haus |
3 | 2 | a1i 11 |
. . . 4
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝐽 ∈ Haus) |
4 | | simpl 472 |
. . . 4
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 ⊆
ℂ) |
5 | | cnheibor.3 |
. . . . 5
⊢ 𝑇 = (𝐽 ↾t 𝑋) |
6 | | simpr 476 |
. . . . 5
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑇 ∈ Comp) |
7 | 5, 6 | syl5eqelr 2693 |
. . . 4
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → (𝐽 ↾t 𝑋) ∈ Comp) |
8 | 1 | cnfldtopon 22396 |
. . . . . 6
⊢ 𝐽 ∈
(TopOn‘ℂ) |
9 | 8 | toponunii 20547 |
. . . . 5
⊢ ℂ =
∪ 𝐽 |
10 | 9 | hauscmp 21020 |
. . . 4
⊢ ((𝐽 ∈ Haus ∧ 𝑋 ⊆ ℂ ∧ (𝐽 ↾t 𝑋) ∈ Comp) → 𝑋 ∈ (Clsd‘𝐽)) |
11 | 3, 4, 7, 10 | syl3anc 1318 |
. . 3
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 ∈ (Clsd‘𝐽)) |
12 | 1 | cnfldtop 22397 |
. . . . . . . . . . 11
⊢ 𝐽 ∈ Top |
13 | 9 | restuni 20776 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ ℂ) → 𝑋 = ∪
(𝐽 ↾t
𝑋)) |
14 | 12, 4, 13 | sylancr 694 |
. . . . . . . . . 10
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 = ∪
(𝐽 ↾t
𝑋)) |
15 | 5 | unieqi 4381 |
. . . . . . . . . 10
⊢ ∪ 𝑇 =
∪ (𝐽 ↾t 𝑋) |
16 | 14, 15 | syl6eqr 2662 |
. . . . . . . . 9
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 = ∪
𝑇) |
17 | 16 | eleq2d 2673 |
. . . . . . . 8
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝑇)) |
18 | 17 | biimpar 501 |
. . . . . . 7
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ ∪ 𝑇)
→ 𝑥 ∈ 𝑋) |
19 | 12 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝐽 ∈ Top) |
20 | | cnex 9896 |
. . . . . . . . . . . 12
⊢ ℂ
∈ V |
21 | | ssexg 4732 |
. . . . . . . . . . . 12
⊢ ((𝑋 ⊆ ℂ ∧ ℂ
∈ V) → 𝑋 ∈
V) |
22 | 4, 20, 21 | sylancl 693 |
. . . . . . . . . . 11
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 ∈ V) |
23 | 22 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑋 ∈ V) |
24 | | cnxmet 22386 |
. . . . . . . . . . . 12
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
25 | 24 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
26 | | 0cnd 9912 |
. . . . . . . . . . 11
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 0 ∈ ℂ) |
27 | 4 | sselda 3568 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ℂ) |
28 | 27 | abscld 14023 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (abs‘𝑥) ∈ ℝ) |
29 | | peano2re 10088 |
. . . . . . . . . . . . 13
⊢
((abs‘𝑥)
∈ ℝ → ((abs‘𝑥) + 1) ∈ ℝ) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((abs‘𝑥) + 1) ∈ ℝ) |
31 | 30 | rexrd 9968 |
. . . . . . . . . . 11
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((abs‘𝑥) + 1) ∈
ℝ*) |
32 | 1 | cnfldtopn 22395 |
. . . . . . . . . . . 12
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
33 | 32 | blopn 22115 |
. . . . . . . . . . 11
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ ((abs‘𝑥) + 1)
∈ ℝ*) → (0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∈ 𝐽) |
34 | 25, 26, 31, 33 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∈ 𝐽) |
35 | | elrestr 15912 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑋 ∈ V ∧
(0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∈ 𝐽) → ((0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∩ 𝑋) ∈ (𝐽 ↾t 𝑋)) |
36 | 19, 23, 34, 35 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∩ 𝑋) ∈ (𝐽 ↾t 𝑋)) |
37 | 36, 5 | syl6eleqr 2699 |
. . . . . . . 8
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∩ 𝑋) ∈ 𝑇) |
38 | | 0cn 9911 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℂ |
39 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (abs
∘ − ) = (abs ∘ − ) |
40 | 39 | cnmetdval 22384 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℂ ∧ 𝑥
∈ ℂ) → (0(abs ∘ − )𝑥) = (abs‘(0 − 𝑥))) |
41 | 38, 40 | mpan 702 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (0(abs
∘ − )𝑥) =
(abs‘(0 − 𝑥))) |
42 | | df-neg 10148 |
. . . . . . . . . . . . . . 15
⊢ -𝑥 = (0 − 𝑥) |
43 | 42 | fveq2i 6106 |
. . . . . . . . . . . . . 14
⊢
(abs‘-𝑥) =
(abs‘(0 − 𝑥)) |
44 | | absneg 13865 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ →
(abs‘-𝑥) =
(abs‘𝑥)) |
45 | 43, 44 | syl5eqr 2658 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ →
(abs‘(0 − 𝑥)) =
(abs‘𝑥)) |
46 | 41, 45 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (0(abs
∘ − )𝑥) =
(abs‘𝑥)) |
47 | 27, 46 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (0(abs ∘ − )𝑥) = (abs‘𝑥)) |
48 | 28 | ltp1d 10833 |
. . . . . . . . . . 11
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (abs‘𝑥) < ((abs‘𝑥) + 1)) |
49 | 47, 48 | eqbrtrd 4605 |
. . . . . . . . . 10
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (0(abs ∘ − )𝑥) < ((abs‘𝑥) + 1)) |
50 | | elbl 22003 |
. . . . . . . . . . 11
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ ((abs‘𝑥) + 1)
∈ ℝ*) → (𝑥 ∈ (0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
↔ (𝑥 ∈ ℂ
∧ (0(abs ∘ − )𝑥) < ((abs‘𝑥) + 1)))) |
51 | 25, 26, 31, 50 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ (0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
↔ (𝑥 ∈ ℂ
∧ (0(abs ∘ − )𝑥) < ((abs‘𝑥) + 1)))) |
52 | 27, 49, 51 | mpbir2and 959 |
. . . . . . . . 9
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ (0(ball‘(abs ∘ −
))((abs‘𝑥) +
1))) |
53 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
54 | 52, 53 | elind 3760 |
. . . . . . . 8
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ((0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∩ 𝑋)) |
55 | 27 | absge0d 14031 |
. . . . . . . . . 10
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 0 ≤ (abs‘𝑥)) |
56 | 28, 55 | ge0p1rpd 11778 |
. . . . . . . . 9
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((abs‘𝑥) + 1) ∈
ℝ+) |
57 | | eqid 2610 |
. . . . . . . . 9
⊢
((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∩ 𝑋) |
58 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑟 = ((abs‘𝑥) + 1) → (0(ball‘(abs
∘ − ))𝑟) =
(0(ball‘(abs ∘ − ))((abs‘𝑥) + 1))) |
59 | 58 | ineq1d 3775 |
. . . . . . . . . . 11
⊢ (𝑟 = ((abs‘𝑥) + 1) →
((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ((0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∩ 𝑋)) |
60 | 59 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑟 = ((abs‘𝑥) + 1) →
(((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ −
))𝑟) ∩ 𝑋) ↔ ((0(ball‘(abs
∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∩ 𝑋))) |
61 | 60 | rspcev 3282 |
. . . . . . . . 9
⊢
((((abs‘𝑥) +
1) ∈ ℝ+ ∧ ((0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∩ 𝑋) =
((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋)) → ∃𝑟 ∈ ℝ+
((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ −
))𝑟) ∩ 𝑋)) |
62 | 56, 57, 61 | sylancl 693 |
. . . . . . . 8
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ∃𝑟 ∈ ℝ+
((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ −
))𝑟) ∩ 𝑋)) |
63 | | eleq2 2677 |
. . . . . . . . . 10
⊢ (𝑢 = ((0(ball‘(abs ∘
− ))((abs‘𝑥) +
1)) ∩ 𝑋) → (𝑥 ∈ 𝑢 ↔ 𝑥 ∈ ((0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∩ 𝑋))) |
64 | | eqeq1 2614 |
. . . . . . . . . . 11
⊢ (𝑢 = ((0(ball‘(abs ∘
− ))((abs‘𝑥) +
1)) ∩ 𝑋) → (𝑢 = ((0(ball‘(abs ∘
− ))𝑟) ∩ 𝑋) ↔ ((0(ball‘(abs
∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ −
))𝑟) ∩ 𝑋))) |
65 | 64 | rexbidv 3034 |
. . . . . . . . . 10
⊢ (𝑢 = ((0(ball‘(abs ∘
− ))((abs‘𝑥) +
1)) ∩ 𝑋) →
(∃𝑟 ∈
ℝ+ 𝑢 =
((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ↔ ∃𝑟 ∈ ℝ+
((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ −
))𝑟) ∩ 𝑋))) |
66 | 63, 65 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑢 = ((0(ball‘(abs ∘
− ))((abs‘𝑥) +
1)) ∩ 𝑋) → ((𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ+ 𝑢 = ((0(ball‘(abs ∘
− ))𝑟) ∩ 𝑋)) ↔ (𝑥 ∈ ((0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∩ 𝑋) ∧ ∃𝑟 ∈ ℝ+
((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ −
))𝑟) ∩ 𝑋)))) |
67 | 66 | rspcev 3282 |
. . . . . . . 8
⊢
((((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) ∈ 𝑇 ∧ (𝑥 ∈ ((0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∩ 𝑋) ∧ ∃𝑟 ∈ ℝ+
((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ −
))𝑟) ∩ 𝑋))) → ∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ+ 𝑢 = ((0(ball‘(abs ∘
− ))𝑟) ∩ 𝑋))) |
68 | 37, 54, 62, 67 | syl12anc 1316 |
. . . . . . 7
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ+ 𝑢 = ((0(ball‘(abs ∘
− ))𝑟) ∩ 𝑋))) |
69 | 18, 68 | syldan 486 |
. . . . . 6
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ ∪ 𝑇)
→ ∃𝑢 ∈
𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ+ 𝑢 = ((0(ball‘(abs ∘
− ))𝑟) ∩ 𝑋))) |
70 | 69 | ralrimiva 2949 |
. . . . 5
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) →
∀𝑥 ∈ ∪ 𝑇∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ+ 𝑢 = ((0(ball‘(abs ∘
− ))𝑟) ∩ 𝑋))) |
71 | | eqid 2610 |
. . . . . 6
⊢ ∪ 𝑇 =
∪ 𝑇 |
72 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑟 = (𝑓‘𝑢) → (0(ball‘(abs ∘ −
))𝑟) = (0(ball‘(abs
∘ − ))(𝑓‘𝑢))) |
73 | 72 | ineq1d 3775 |
. . . . . . 7
⊢ (𝑟 = (𝑓‘𝑢) → ((0(ball‘(abs ∘ −
))𝑟) ∩ 𝑋) = ((0(ball‘(abs ∘
− ))(𝑓‘𝑢)) ∩ 𝑋)) |
74 | 73 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑟 = (𝑓‘𝑢) → (𝑢 = ((0(ball‘(abs ∘ −
))𝑟) ∩ 𝑋) ↔ 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) |
75 | 71, 74 | cmpcovf 21004 |
. . . . 5
⊢ ((𝑇 ∈ Comp ∧ ∀𝑥 ∈ ∪ 𝑇∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ+ 𝑢 = ((0(ball‘(abs ∘
− ))𝑟) ∩ 𝑋))) → ∃𝑠 ∈ (𝒫 𝑇 ∩ Fin)(∪ 𝑇 =
∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋)))) |
76 | 6, 70, 75 | syl2anc 691 |
. . . 4
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) →
∃𝑠 ∈ (𝒫
𝑇 ∩ Fin)(∪ 𝑇 =
∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋)))) |
77 | 16 | ad4antr 764 |
. . . . . . . . . . . . . 14
⊢
((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → 𝑋 = ∪ 𝑇) |
78 | | simpllr 795 |
. . . . . . . . . . . . . 14
⊢
((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → ∪ 𝑇 = ∪
𝑠) |
79 | 77, 78 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢
((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → 𝑋 = ∪ 𝑠) |
80 | 79 | eleq2d 2673 |
. . . . . . . . . . . 12
⊢
((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝑠)) |
81 | | eluni2 4376 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ∪ 𝑠
↔ ∃𝑧 ∈
𝑠 𝑥 ∈ 𝑧) |
82 | 80, 81 | syl6bb 275 |
. . . . . . . . . . 11
⊢
((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (𝑥 ∈ 𝑋 ↔ ∃𝑧 ∈ 𝑠 𝑥 ∈ 𝑧)) |
83 | | elssuni 4403 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑠 → 𝑧 ⊆ ∪ 𝑠) |
84 | 83 | ad2antrl 760 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ⊆ ∪ 𝑠) |
85 | 79 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑋 = ∪ 𝑠) |
86 | 84, 85 | sseqtr4d 3605 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ⊆ 𝑋) |
87 | | simp-6l 806 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑋 ⊆ ℂ) |
88 | 86, 87 | sstrd 3578 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ⊆ ℂ) |
89 | | simprr 792 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ 𝑧) |
90 | 88, 89 | sseldd 3569 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ ℂ) |
91 | 90 | abscld 14023 |
. . . . . . . . . . . . 13
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) ∈ ℝ) |
92 | | simplrl 796 |
. . . . . . . . . . . . 13
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑟 ∈ ℝ) |
93 | | simprl 790 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) → 𝑓:𝑠⟶ℝ+) |
94 | 93 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑓:𝑠⟶ℝ+) |
95 | | simprl 790 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ∈ 𝑠) |
96 | 94, 95 | ffvelrnd 6268 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ∈
ℝ+) |
97 | 96 | rpred 11748 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ∈ ℝ) |
98 | 90, 46 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (0(abs ∘ − )𝑥) = (abs‘𝑥)) |
99 | | inss1 3795 |
. . . . . . . . . . . . . . . . . 18
⊢
((0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ∩ 𝑋) ⊆ (0(ball‘(abs ∘ −
))(𝑓‘𝑧)) |
100 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) → ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋)) |
101 | 100 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋)) |
102 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = 𝑧 → 𝑢 = 𝑧) |
103 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑢 = 𝑧 → (𝑓‘𝑢) = (𝑓‘𝑧)) |
104 | 103 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 = 𝑧 → (0(ball‘(abs ∘ −
))(𝑓‘𝑢)) = (0(ball‘(abs ∘
− ))(𝑓‘𝑧))) |
105 | 104 | ineq1d 3775 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = 𝑧 → ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋) = ((0(ball‘(abs ∘ −
))(𝑓‘𝑧)) ∩ 𝑋)) |
106 | 102, 105 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 = 𝑧 → (𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋) ↔ 𝑧 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑧)) ∩ 𝑋))) |
107 | 106 | rspcv 3278 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ 𝑠 → (∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋) → 𝑧 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑧)) ∩ 𝑋))) |
108 | 95, 101, 107 | sylc 63 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑧)) ∩ 𝑋)) |
109 | 89, 108 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ ((0(ball‘(abs ∘ −
))(𝑓‘𝑧)) ∩ 𝑋)) |
110 | 99, 109 | sseldi 3566 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ (0(ball‘(abs ∘ −
))(𝑓‘𝑧))) |
111 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
112 | | 0cnd 9912 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 0 ∈ ℂ) |
113 | 96 | rpxrd 11749 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ∈
ℝ*) |
114 | | elbl 22003 |
. . . . . . . . . . . . . . . . . 18
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ (𝑓‘𝑧) ∈ ℝ*)
→ (𝑥 ∈
(0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ↔ (𝑥 ∈ ℂ ∧ (0(abs ∘ −
)𝑥) < (𝑓‘𝑧)))) |
115 | 111, 112,
113, 114 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑥 ∈ (0(ball‘(abs ∘ −
))(𝑓‘𝑧)) ↔ (𝑥 ∈ ℂ ∧ (0(abs ∘ −
)𝑥) < (𝑓‘𝑧)))) |
116 | 110, 115 | mpbid 221 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑥 ∈ ℂ ∧ (0(abs ∘ −
)𝑥) < (𝑓‘𝑧))) |
117 | 116 | simprd 478 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (0(abs ∘ − )𝑥) < (𝑓‘𝑧)) |
118 | 98, 117 | eqbrtrrd 4607 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) < (𝑓‘𝑧)) |
119 | | simplrr 797 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟) |
120 | 103 | breq1d 4593 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑧 → ((𝑓‘𝑢) ≤ 𝑟 ↔ (𝑓‘𝑧) ≤ 𝑟)) |
121 | 120 | rspcv 3278 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑠 → (∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟 → (𝑓‘𝑧) ≤ 𝑟)) |
122 | 95, 119, 121 | sylc 63 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ≤ 𝑟) |
123 | 91, 97, 92, 118, 122 | ltletrd 10076 |
. . . . . . . . . . . . 13
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) < 𝑟) |
124 | 91, 92, 123 | ltled 10064 |
. . . . . . . . . . . 12
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) ≤ 𝑟) |
125 | 124 | rexlimdvaa 3014 |
. . . . . . . . . . 11
⊢
((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (∃𝑧 ∈ 𝑠 𝑥 ∈ 𝑧 → (abs‘𝑥) ≤ 𝑟)) |
126 | 82, 125 | sylbid 229 |
. . . . . . . . . 10
⊢
((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (𝑥 ∈ 𝑋 → (abs‘𝑥) ≤ 𝑟)) |
127 | 126 | ralrimiv 2948 |
. . . . . . . . 9
⊢
((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟) |
128 | | inss2 3796 |
. . . . . . . . . . 11
⊢
(𝒫 𝑇 ∩
Fin) ⊆ Fin |
129 | | simpllr 795 |
. . . . . . . . . . 11
⊢
(((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) → 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) |
130 | 128, 129 | sseldi 3566 |
. . . . . . . . . 10
⊢
(((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) → 𝑠 ∈ Fin) |
131 | | ffvelrn 6265 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝑠⟶ℝ+ ∧ 𝑢 ∈ 𝑠) → (𝑓‘𝑢) ∈
ℝ+) |
132 | 131 | rpred 11748 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝑠⟶ℝ+ ∧ 𝑢 ∈ 𝑠) → (𝑓‘𝑢) ∈ ℝ) |
133 | 132 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ (𝑓:𝑠⟶ℝ+ →
∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ∈ ℝ) |
134 | 133 | ad2antrl 760 |
. . . . . . . . . 10
⊢
(((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) → ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ∈ ℝ) |
135 | | fimaxre3 10849 |
. . . . . . . . . 10
⊢ ((𝑠 ∈ Fin ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ∈ ℝ) → ∃𝑟 ∈ ℝ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟) |
136 | 130, 134,
135 | syl2anc 691 |
. . . . . . . . 9
⊢
(((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟) |
137 | 127, 136 | reximddv 3001 |
. . . . . . . 8
⊢
(((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟) |
138 | 137 | ex 449 |
. . . . . . 7
⊢ ((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 =
∪ 𝑠) → ((𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋)) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) |
139 | 138 | exlimdv 1848 |
. . . . . 6
⊢ ((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 =
∪ 𝑠) → (∃𝑓(𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋)) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) |
140 | 139 | expimpd 627 |
. . . . 5
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) → ((∪ 𝑇 =
∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) |
141 | 140 | rexlimdva 3013 |
. . . 4
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) →
(∃𝑠 ∈ (𝒫
𝑇 ∩ Fin)(∪ 𝑇 =
∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) |
142 | 76, 141 | mpd 15 |
. . 3
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) →
∃𝑟 ∈ ℝ
∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟) |
143 | 11, 142 | jca 553 |
. 2
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → (𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) |
144 | | eqid 2610 |
. . . . . 6
⊢ (𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧))) = (𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧))) |
145 | | eqid 2610 |
. . . . . 6
⊢ ((𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧))) “ ((-𝑟[,]𝑟) × (-𝑟[,]𝑟))) = ((𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧))) “ ((-𝑟[,]𝑟) × (-𝑟[,]𝑟))) |
146 | 1, 5, 144, 145 | cnheiborlem 22561 |
. . . . 5
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑟 ∈ ℝ ∧ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) → 𝑇 ∈ Comp) |
147 | 146 | rexlimdvaa 3014 |
. . . 4
⊢ (𝑋 ∈ (Clsd‘𝐽) → (∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟 → 𝑇 ∈ Comp)) |
148 | 147 | imp 444 |
. . 3
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟) → 𝑇 ∈ Comp) |
149 | 148 | adantl 481 |
. 2
⊢ ((𝑋 ⊆ ℂ ∧ (𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) → 𝑇 ∈ Comp) |
150 | 143, 149 | impbida 873 |
1
⊢ (𝑋 ⊆ ℂ → (𝑇 ∈ Comp ↔ (𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟))) |