| Step | Hyp | Ref
| Expression |
| 1 | | cnheibor.2 |
. . . . 5
⊢ 𝐽 =
(TopOpen‘ℂfld) |
| 2 | 1 | cnfldhaus 24805 |
. . . 4
⊢ 𝐽 ∈ Haus |
| 3 | | simpl 482 |
. . . 4
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 ⊆
ℂ) |
| 4 | | cnheibor.3 |
. . . . 5
⊢ 𝑇 = (𝐽 ↾t 𝑋) |
| 5 | | simpr 484 |
. . . . 5
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑇 ∈ Comp) |
| 6 | 4, 5 | eqeltrrid 2846 |
. . . 4
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → (𝐽 ↾t 𝑋) ∈ Comp) |
| 7 | 1 | cnfldtopon 24803 |
. . . . . 6
⊢ 𝐽 ∈
(TopOn‘ℂ) |
| 8 | 7 | toponunii 22922 |
. . . . 5
⊢ ℂ =
∪ 𝐽 |
| 9 | 8 | hauscmp 23415 |
. . . 4
⊢ ((𝐽 ∈ Haus ∧ 𝑋 ⊆ ℂ ∧ (𝐽 ↾t 𝑋) ∈ Comp) → 𝑋 ∈ (Clsd‘𝐽)) |
| 10 | 2, 3, 6, 9 | mp3an2i 1468 |
. . 3
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 ∈ (Clsd‘𝐽)) |
| 11 | 1 | cnfldtop 24804 |
. . . . . . . . . . 11
⊢ 𝐽 ∈ Top |
| 12 | 8 | restuni 23170 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ ℂ) → 𝑋 = ∪
(𝐽 ↾t
𝑋)) |
| 13 | 11, 3, 12 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 = ∪
(𝐽 ↾t
𝑋)) |
| 14 | 4 | unieqi 4919 |
. . . . . . . . . 10
⊢ ∪ 𝑇 =
∪ (𝐽 ↾t 𝑋) |
| 15 | 13, 14 | eqtr4di 2795 |
. . . . . . . . 9
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 = ∪
𝑇) |
| 16 | 15 | eleq2d 2827 |
. . . . . . . 8
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝑇)) |
| 17 | 16 | biimpar 477 |
. . . . . . 7
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ ∪ 𝑇)
→ 𝑥 ∈ 𝑋) |
| 18 | | cnex 11236 |
. . . . . . . . . . . 12
⊢ ℂ
∈ V |
| 19 | | ssexg 5323 |
. . . . . . . . . . . 12
⊢ ((𝑋 ⊆ ℂ ∧ ℂ
∈ V) → 𝑋 ∈
V) |
| 20 | 3, 18, 19 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → 𝑋 ∈ V) |
| 21 | 20 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑋 ∈ V) |
| 22 | | cnxmet 24793 |
. . . . . . . . . . 11
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
| 23 | | 0cnd 11254 |
. . . . . . . . . . 11
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 0 ∈ ℂ) |
| 24 | 3 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ℂ) |
| 25 | 24 | abscld 15475 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (abs‘𝑥) ∈ ℝ) |
| 26 | | peano2re 11434 |
. . . . . . . . . . . . 13
⊢
((abs‘𝑥)
∈ ℝ → ((abs‘𝑥) + 1) ∈ ℝ) |
| 27 | 25, 26 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((abs‘𝑥) + 1) ∈ ℝ) |
| 28 | 27 | rexrd 11311 |
. . . . . . . . . . 11
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((abs‘𝑥) + 1) ∈
ℝ*) |
| 29 | 1 | cnfldtopn 24802 |
. . . . . . . . . . . 12
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
| 30 | 29 | blopn 24513 |
. . . . . . . . . . 11
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ ((abs‘𝑥) + 1)
∈ ℝ*) → (0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∈ 𝐽) |
| 31 | 22, 23, 28, 30 | mp3an2i 1468 |
. . . . . . . . . 10
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∈ 𝐽) |
| 32 | | elrestr 17473 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑋 ∈ V ∧
(0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∈ 𝐽) → ((0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∩ 𝑋) ∈ (𝐽 ↾t 𝑋)) |
| 33 | 11, 21, 31, 32 | mp3an2i 1468 |
. . . . . . . . 9
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∩ 𝑋) ∈ (𝐽 ↾t 𝑋)) |
| 34 | 33, 4 | eleqtrrdi 2852 |
. . . . . . . 8
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∩ 𝑋) ∈ 𝑇) |
| 35 | | 0cn 11253 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℂ |
| 36 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (abs
∘ − ) = (abs ∘ − ) |
| 37 | 36 | cnmetdval 24791 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℂ ∧ 𝑥
∈ ℂ) → (0(abs ∘ − )𝑥) = (abs‘(0 − 𝑥))) |
| 38 | 35, 37 | mpan 690 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (0(abs
∘ − )𝑥) =
(abs‘(0 − 𝑥))) |
| 39 | | df-neg 11495 |
. . . . . . . . . . . . . . 15
⊢ -𝑥 = (0 − 𝑥) |
| 40 | 39 | fveq2i 6909 |
. . . . . . . . . . . . . 14
⊢
(abs‘-𝑥) =
(abs‘(0 − 𝑥)) |
| 41 | | absneg 15316 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ →
(abs‘-𝑥) =
(abs‘𝑥)) |
| 42 | 40, 41 | eqtr3id 2791 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ →
(abs‘(0 − 𝑥)) =
(abs‘𝑥)) |
| 43 | 38, 42 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (0(abs
∘ − )𝑥) =
(abs‘𝑥)) |
| 44 | 24, 43 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (0(abs ∘ − )𝑥) = (abs‘𝑥)) |
| 45 | 25 | ltp1d 12198 |
. . . . . . . . . . 11
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (abs‘𝑥) < ((abs‘𝑥) + 1)) |
| 46 | 44, 45 | eqbrtrd 5165 |
. . . . . . . . . 10
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (0(abs ∘ − )𝑥) < ((abs‘𝑥) + 1)) |
| 47 | | elbl 24398 |
. . . . . . . . . . 11
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ ((abs‘𝑥) + 1)
∈ ℝ*) → (𝑥 ∈ (0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
↔ (𝑥 ∈ ℂ
∧ (0(abs ∘ − )𝑥) < ((abs‘𝑥) + 1)))) |
| 48 | 22, 23, 28, 47 | mp3an2i 1468 |
. . . . . . . . . 10
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ (0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
↔ (𝑥 ∈ ℂ
∧ (0(abs ∘ − )𝑥) < ((abs‘𝑥) + 1)))) |
| 49 | 24, 46, 48 | mpbir2and 713 |
. . . . . . . . 9
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ (0(ball‘(abs ∘ −
))((abs‘𝑥) +
1))) |
| 50 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
| 51 | 49, 50 | elind 4200 |
. . . . . . . 8
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ((0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∩ 𝑋)) |
| 52 | 24 | absge0d 15483 |
. . . . . . . . . 10
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → 0 ≤ (abs‘𝑥)) |
| 53 | 25, 52 | ge0p1rpd 13107 |
. . . . . . . . 9
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ((abs‘𝑥) + 1) ∈
ℝ+) |
| 54 | | eqid 2737 |
. . . . . . . . 9
⊢
((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∩ 𝑋) |
| 55 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑟 = ((abs‘𝑥) + 1) → (0(ball‘(abs
∘ − ))𝑟) =
(0(ball‘(abs ∘ − ))((abs‘𝑥) + 1))) |
| 56 | 55 | ineq1d 4219 |
. . . . . . . . . 10
⊢ (𝑟 = ((abs‘𝑥) + 1) →
((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ((0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∩ 𝑋)) |
| 57 | 56 | rspceeqv 3645 |
. . . . . . . . 9
⊢
((((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 586 |
. . . . . . . 8
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ∃𝑟 ∈ ℝ+
((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ −
))𝑟) ∩ 𝑋)) |
| 59 | | eleq2 2830 |
. . . . . . . . . 10
⊢ (𝑢 = ((0(ball‘(abs ∘
− ))((abs‘𝑥) +
1)) ∩ 𝑋) → (𝑥 ∈ 𝑢 ↔ 𝑥 ∈ ((0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∩ 𝑋))) |
| 60 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑢 = ((0(ball‘(abs ∘
− ))((abs‘𝑥) +
1)) ∩ 𝑋) → (𝑢 = ((0(ball‘(abs ∘
− ))𝑟) ∩ 𝑋) ↔ ((0(ball‘(abs
∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ −
))𝑟) ∩ 𝑋))) |
| 61 | 60 | rexbidv 3179 |
. . . . . . . . . 10
⊢ (𝑢 = ((0(ball‘(abs ∘
− ))((abs‘𝑥) +
1)) ∩ 𝑋) →
(∃𝑟 ∈
ℝ+ 𝑢 =
((0(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ↔ ∃𝑟 ∈ ℝ+
((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ −
))𝑟) ∩ 𝑋))) |
| 62 | 59, 61 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑢 = ((0(ball‘(abs ∘
− ))((abs‘𝑥) +
1)) ∩ 𝑋) → ((𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ+ 𝑢 = ((0(ball‘(abs ∘
− ))𝑟) ∩ 𝑋)) ↔ (𝑥 ∈ ((0(ball‘(abs ∘ −
))((abs‘𝑥) + 1))
∩ 𝑋) ∧ ∃𝑟 ∈ ℝ+
((0(ball‘(abs ∘ − ))((abs‘𝑥) + 1)) ∩ 𝑋) = ((0(ball‘(abs ∘ −
))𝑟) ∩ 𝑋)))) |
| 63 | 62 | rspcev 3622 |
. . . . . . . 8
⊢
((((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 837 |
. . . . . . 7
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ 𝑋) → ∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ+ 𝑢 = ((0(ball‘(abs ∘
− ))𝑟) ∩ 𝑋))) |
| 65 | 17, 64 | syldan 591 |
. . . . . 6
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑥 ∈ ∪ 𝑇)
→ ∃𝑢 ∈
𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ+ 𝑢 = ((0(ball‘(abs ∘
− ))𝑟) ∩ 𝑋))) |
| 66 | 65 | ralrimiva 3146 |
. . . . 5
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) →
∀𝑥 ∈ ∪ 𝑇∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ+ 𝑢 = ((0(ball‘(abs ∘
− ))𝑟) ∩ 𝑋))) |
| 67 | | eqid 2737 |
. . . . . 6
⊢ ∪ 𝑇 =
∪ 𝑇 |
| 68 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑟 = (𝑓‘𝑢) → (0(ball‘(abs ∘ −
))𝑟) = (0(ball‘(abs
∘ − ))(𝑓‘𝑢))) |
| 69 | 68 | ineq1d 4219 |
. . . . . . 7
⊢ (𝑟 = (𝑓‘𝑢) → ((0(ball‘(abs ∘ −
))𝑟) ∩ 𝑋) = ((0(ball‘(abs ∘
− ))(𝑓‘𝑢)) ∩ 𝑋)) |
| 70 | 69 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑟 = (𝑓‘𝑢) → (𝑢 = ((0(ball‘(abs ∘ −
))𝑟) ∩ 𝑋) ↔ 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) |
| 71 | 67, 70 | cmpcovf 23399 |
. . . . 5
⊢ ((𝑇 ∈ Comp ∧ ∀𝑥 ∈ ∪ 𝑇∃𝑢 ∈ 𝑇 (𝑥 ∈ 𝑢 ∧ ∃𝑟 ∈ ℝ+ 𝑢 = ((0(ball‘(abs ∘
− ))𝑟) ∩ 𝑋))) → ∃𝑠 ∈ (𝒫 𝑇 ∩ Fin)(∪ 𝑇 =
∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋)))) |
| 72 | 5, 66, 71 | syl2anc 584 |
. . . 4
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) →
∃𝑠 ∈ (𝒫
𝑇 ∩ Fin)(∪ 𝑇 =
∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋)))) |
| 73 | 15 | ad4antr 732 |
. . . . . . . . . . . . . 14
⊢
((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → 𝑋 = ∪ 𝑇) |
| 74 | | simpllr 776 |
. . . . . . . . . . . . . 14
⊢
((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → ∪ 𝑇 = ∪
𝑠) |
| 75 | 73, 74 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢
((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → 𝑋 = ∪ 𝑠) |
| 76 | 75 | eleq2d 2827 |
. . . . . . . . . . . 12
⊢
((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝑠)) |
| 77 | | eluni2 4911 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ∪ 𝑠
↔ ∃𝑧 ∈
𝑠 𝑥 ∈ 𝑧) |
| 78 | 76, 77 | bitrdi 287 |
. . . . . . . . . . 11
⊢
((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (𝑥 ∈ 𝑋 ↔ ∃𝑧 ∈ 𝑠 𝑥 ∈ 𝑧)) |
| 79 | | elssuni 4937 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑠 → 𝑧 ⊆ ∪ 𝑠) |
| 80 | 79 | ad2antrl 728 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ⊆ ∪ 𝑠) |
| 81 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑋 = ∪ 𝑠) |
| 82 | 80, 81 | sseqtrrd 4021 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ⊆ 𝑋) |
| 83 | | simp-6l 787 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑋 ⊆ ℂ) |
| 84 | 82, 83 | sstrd 3994 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ⊆ ℂ) |
| 85 | | simprr 773 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ 𝑧) |
| 86 | 84, 85 | sseldd 3984 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ ℂ) |
| 87 | 86 | abscld 15475 |
. . . . . . . . . . . . 13
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) ∈ ℝ) |
| 88 | | simplrl 777 |
. . . . . . . . . . . . 13
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑟 ∈ ℝ) |
| 89 | | simprl 771 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) → 𝑓:𝑠⟶ℝ+) |
| 90 | 89 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑓:𝑠⟶ℝ+) |
| 91 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ∈ 𝑠) |
| 92 | 90, 91 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ∈
ℝ+) |
| 93 | 92 | rpred 13077 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ∈ ℝ) |
| 94 | 86, 43 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (0(abs ∘ − )𝑥) = (abs‘𝑥)) |
| 95 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 = 𝑧 → 𝑢 = 𝑧) |
| 96 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 = 𝑧 → (𝑓‘𝑢) = (𝑓‘𝑧)) |
| 97 | 96 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = 𝑧 → (0(ball‘(abs ∘ −
))(𝑓‘𝑢)) = (0(ball‘(abs ∘
− ))(𝑓‘𝑧))) |
| 98 | 97 | ineq1d 4219 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 = 𝑧 → ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋) = ((0(ball‘(abs ∘ −
))(𝑓‘𝑧)) ∩ 𝑋)) |
| 99 | 95, 98 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = 𝑧 → (𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋) ↔ 𝑧 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑧)) ∩ 𝑋))) |
| 100 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) → ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋)) |
| 101 | 100 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → ∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋)) |
| 102 | 99, 101, 91 | rspcdva 3623 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑧 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑧)) ∩ 𝑋)) |
| 103 | 85, 102 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ ((0(ball‘(abs ∘ −
))(𝑓‘𝑧)) ∩ 𝑋)) |
| 104 | 103 | elin1d 4204 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ (0(ball‘(abs ∘ −
))(𝑓‘𝑧))) |
| 105 | | 0cnd 11254 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → 0 ∈ ℂ) |
| 106 | 92 | rpxrd 13078 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ∈
ℝ*) |
| 107 | | elbl 24398 |
. . . . . . . . . . . . . . . . . 18
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ (𝑓‘𝑧) ∈ ℝ*)
→ (𝑥 ∈
(0(ball‘(abs ∘ − ))(𝑓‘𝑧)) ↔ (𝑥 ∈ ℂ ∧ (0(abs ∘ −
)𝑥) < (𝑓‘𝑧)))) |
| 108 | 22, 105, 106, 107 | mp3an2i 1468 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑥 ∈ (0(ball‘(abs ∘ −
))(𝑓‘𝑧)) ↔ (𝑥 ∈ ℂ ∧ (0(abs ∘ −
)𝑥) < (𝑓‘𝑧)))) |
| 109 | 104, 108 | mpbid 232 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑥 ∈ ℂ ∧ (0(abs ∘ −
)𝑥) < (𝑓‘𝑧))) |
| 110 | 109 | simprd 495 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (0(abs ∘ − )𝑥) < (𝑓‘𝑧)) |
| 111 | 94, 110 | eqbrtrrd 5167 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) < (𝑓‘𝑧)) |
| 112 | 96 | breq1d 5153 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑧 → ((𝑓‘𝑢) ≤ 𝑟 ↔ (𝑓‘𝑧) ≤ 𝑟)) |
| 113 | | simplrr 778 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟) |
| 114 | 112, 113,
91 | rspcdva 3623 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (𝑓‘𝑧) ≤ 𝑟) |
| 115 | 87, 93, 88, 111, 114 | ltletrd 11421 |
. . . . . . . . . . . . 13
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) < 𝑟) |
| 116 | 87, 88, 115 | ltled 11409 |
. . . . . . . . . . . 12
⊢
(((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) ∧ (𝑧 ∈ 𝑠 ∧ 𝑥 ∈ 𝑧)) → (abs‘𝑥) ≤ 𝑟) |
| 117 | 116 | rexlimdvaa 3156 |
. . . . . . . . . . 11
⊢
((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (∃𝑧 ∈ 𝑠 𝑥 ∈ 𝑧 → (abs‘𝑥) ≤ 𝑟)) |
| 118 | 78, 117 | sylbid 240 |
. . . . . . . . . 10
⊢
((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → (𝑥 ∈ 𝑋 → (abs‘𝑥) ≤ 𝑟)) |
| 119 | 118 | ralrimiv 3145 |
. . . . . . . . 9
⊢
((((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) ∧ (𝑟 ∈ ℝ ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟)) → ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟) |
| 120 | | simpllr 776 |
. . . . . . . . . . 11
⊢
(((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) → 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) |
| 121 | 120 | elin2d 4205 |
. . . . . . . . . 10
⊢
(((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) → 𝑠 ∈ Fin) |
| 122 | | ffvelcdm 7101 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝑠⟶ℝ+ ∧ 𝑢 ∈ 𝑠) → (𝑓‘𝑢) ∈
ℝ+) |
| 123 | 122 | rpred 13077 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝑠⟶ℝ+ ∧ 𝑢 ∈ 𝑠) → (𝑓‘𝑢) ∈ ℝ) |
| 124 | 123 | ralrimiva 3146 |
. . . . . . . . . . 11
⊢ (𝑓:𝑠⟶ℝ+ →
∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ∈ ℝ) |
| 125 | 124 | ad2antrl 728 |
. . . . . . . . . 10
⊢
(((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) → ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ∈ ℝ) |
| 126 | | fimaxre3 12214 |
. . . . . . . . . 10
⊢ ((𝑠 ∈ Fin ∧ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ∈ ℝ) → ∃𝑟 ∈ ℝ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟) |
| 127 | 121, 125,
126 | syl2anc 584 |
. . . . . . . . 9
⊢
(((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑢 ∈ 𝑠 (𝑓‘𝑢) ≤ 𝑟) |
| 128 | 119, 127 | reximddv 3171 |
. . . . . . . 8
⊢
(((((𝑋 ⊆
ℂ ∧ 𝑇 ∈
Comp) ∧ 𝑠 ∈
(𝒫 𝑇 ∩ Fin))
∧ ∪ 𝑇 = ∪ 𝑠) ∧ (𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟) |
| 129 | 128 | ex 412 |
. . . . . . 7
⊢ ((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 =
∪ 𝑠) → ((𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋)) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) |
| 130 | 129 | exlimdv 1933 |
. . . . . 6
⊢ ((((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) ∧ ∪ 𝑇 =
∪ 𝑠) → (∃𝑓(𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋)) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) |
| 131 | 130 | expimpd 453 |
. . . . 5
⊢ (((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) ∧ 𝑠 ∈ (𝒫 𝑇 ∩ Fin)) → ((∪ 𝑇 =
∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) |
| 132 | 131 | rexlimdva 3155 |
. . . 4
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) →
(∃𝑠 ∈ (𝒫
𝑇 ∩ Fin)(∪ 𝑇 =
∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶ℝ+ ∧
∀𝑢 ∈ 𝑠 𝑢 = ((0(ball‘(abs ∘ −
))(𝑓‘𝑢)) ∩ 𝑋))) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) |
| 133 | 72, 132 | mpd 15 |
. . 3
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) →
∃𝑟 ∈ ℝ
∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟) |
| 134 | 10, 133 | jca 511 |
. 2
⊢ ((𝑋 ⊆ ℂ ∧ 𝑇 ∈ Comp) → (𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) |
| 135 | | eqid 2737 |
. . . . . 6
⊢ (𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧))) = (𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧))) |
| 136 | | eqid 2737 |
. . . . . 6
⊢ ((𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧))) “ ((-𝑟[,]𝑟) × (-𝑟[,]𝑟))) = ((𝑦 ∈ ℝ, 𝑧 ∈ ℝ ↦ (𝑦 + (i · 𝑧))) “ ((-𝑟[,]𝑟) × (-𝑟[,]𝑟))) |
| 137 | 1, 4, 135, 136 | cnheiborlem 24986 |
. . . . 5
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑟 ∈ ℝ ∧ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) → 𝑇 ∈ Comp) |
| 138 | 137 | rexlimdvaa 3156 |
. . . 4
⊢ (𝑋 ∈ (Clsd‘𝐽) → (∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟 → 𝑇 ∈ Comp)) |
| 139 | 138 | imp 406 |
. . 3
⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟) → 𝑇 ∈ Comp) |
| 140 | 139 | adantl 481 |
. 2
⊢ ((𝑋 ⊆ ℂ ∧ (𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)) → 𝑇 ∈ Comp) |
| 141 | 134, 140 | impbida 801 |
1
⊢ (𝑋 ⊆ ℂ → (𝑇 ∈ Comp ↔ (𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟))) |