Step | Hyp | Ref
| Expression |
1 | | sstotbnd.2 |
. . . . 5
⊢ 𝑁 = (𝑀 ↾ (𝑌 × 𝑌)) |
2 | | metres2 22388 |
. . . . 5
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑀 ↾ (𝑌 × 𝑌)) ∈ (Met‘𝑌)) |
3 | 1, 2 | syl5eqel 2854 |
. . . 4
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → 𝑁 ∈ (Met‘𝑌)) |
4 | | istotbnd3 33902 |
. . . . 5
⊢ (𝑁 ∈ (TotBnd‘𝑌) ↔ (𝑁 ∈ (Met‘𝑌) ∧ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) |
5 | 4 | baib 525 |
. . . 4
⊢ (𝑁 ∈ (Met‘𝑌) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) |
6 | 3, 5 | syl 17 |
. . 3
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) |
7 | | simpllr 760 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑌 ⊆ 𝑋) |
8 | | sspwb 5045 |
. . . . . . . . . 10
⊢ (𝑌 ⊆ 𝑋 ↔ 𝒫 𝑌 ⊆ 𝒫 𝑋) |
9 | 7, 8 | sylib 208 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝒫 𝑌 ⊆ 𝒫 𝑋) |
10 | 9 | ssrind 3988 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → (𝒫 𝑌 ∩ Fin) ⊆ (𝒫 𝑋 ∩ Fin)) |
11 | | simprl 754 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) |
12 | 10, 11 | sseldd 3753 |
. . . . . . 7
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) |
13 | | simprr 756 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌) |
14 | | metxmet 22359 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀 ∈ (∞Met‘𝑋)) |
15 | 14 | ad4antr 712 |
. . . . . . . . . . . . 13
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑀 ∈ (∞Met‘𝑋)) |
16 | | elfpw 8424 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ↔ (𝑣 ⊆ 𝑌 ∧ 𝑣 ∈ Fin)) |
17 | 16 | simplbi 485 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) → 𝑣 ⊆ 𝑌) |
18 | 17 | adantl 467 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) → 𝑣 ⊆ 𝑌) |
19 | 18 | sselda 3752 |
. . . . . . . . . . . . . 14
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ 𝑌) |
20 | | simp-4r 770 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑌 ⊆ 𝑋) |
21 | | sseqin2 3968 |
. . . . . . . . . . . . . . 15
⊢ (𝑌 ⊆ 𝑋 ↔ (𝑋 ∩ 𝑌) = 𝑌) |
22 | 20, 21 | sylib 208 |
. . . . . . . . . . . . . 14
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → (𝑋 ∩ 𝑌) = 𝑌) |
23 | 19, 22 | eleqtrrd 2853 |
. . . . . . . . . . . . 13
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ (𝑋 ∩ 𝑌)) |
24 | | simpllr 760 |
. . . . . . . . . . . . . 14
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑑 ∈ ℝ+) |
25 | 24 | rpxrd 12076 |
. . . . . . . . . . . . 13
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑑 ∈ ℝ*) |
26 | 1 | blres 22456 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ (𝑋 ∩ 𝑌) ∧ 𝑑 ∈ ℝ*) → (𝑥(ball‘𝑁)𝑑) = ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌)) |
27 | 15, 23, 25, 26 | syl3anc 1476 |
. . . . . . . . . . . 12
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → (𝑥(ball‘𝑁)𝑑) = ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌)) |
28 | | inss1 3981 |
. . . . . . . . . . . 12
⊢ ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌) ⊆ (𝑥(ball‘𝑀)𝑑) |
29 | 27, 28 | syl6eqss 3804 |
. . . . . . . . . . 11
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑)) |
30 | 29 | ralrimiva 3115 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) →
∀𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑)) |
31 | | ss2iun 4670 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑) → ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)) |
32 | 30, 31 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)) |
33 | 32 | adantrr 696 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)) |
34 | 13, 33 | eqsstr3d 3789 |
. . . . . . 7
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)) |
35 | 12, 34 | jca 501 |
. . . . . 6
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))) |
36 | 35 | ex 397 |
. . . . 5
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) → ((𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌) → (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)))) |
37 | 36 | reximdv2 3162 |
. . . 4
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) →
(∃𝑣 ∈ (𝒫
𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌 → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))) |
38 | 37 | ralimdva 3111 |
. . 3
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌 → ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))) |
39 | 6, 38 | sylbid 230 |
. 2
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) → ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))) |
40 | | simpr 471 |
. . . . . . 7
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) → 𝑐 ∈
ℝ+) |
41 | 40 | rphalfcld 12087 |
. . . . . 6
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) → (𝑐 / 2) ∈
ℝ+) |
42 | | oveq2 6801 |
. . . . . . . . . 10
⊢ (𝑑 = (𝑐 / 2) → (𝑥(ball‘𝑀)𝑑) = (𝑥(ball‘𝑀)(𝑐 / 2))) |
43 | 42 | iuneq2d 4681 |
. . . . . . . . 9
⊢ (𝑑 = (𝑐 / 2) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))) |
44 | 43 | sseq2d 3782 |
. . . . . . . 8
⊢ (𝑑 = (𝑐 / 2) → (𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) ↔ 𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) |
45 | 44 | rexbidv 3200 |
. . . . . . 7
⊢ (𝑑 = (𝑐 / 2) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) ↔ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) |
46 | 45 | rspcv 3456 |
. . . . . 6
⊢ ((𝑐 / 2) ∈ ℝ+
→ (∀𝑑 ∈
ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) |
47 | 41, 46 | syl 17 |
. . . . 5
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) →
(∀𝑑 ∈
ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) |
48 | | elfpw 8424 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ↔ (𝑣 ⊆ 𝑋 ∧ 𝑣 ∈ Fin)) |
49 | 48 | simprbi 484 |
. . . . . . . . . 10
⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ∈ Fin) |
50 | 49 | ad2antrl 707 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → 𝑣 ∈ Fin) |
51 | | ssrab2 3836 |
. . . . . . . . 9
⊢ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ⊆ 𝑣 |
52 | | ssfi 8336 |
. . . . . . . . 9
⊢ ((𝑣 ∈ Fin ∧ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ⊆ 𝑣) → {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin) |
53 | 50, 51, 52 | sylancl 574 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin) |
54 | | oveq1 6800 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝑥(ball‘𝑀)(𝑐 / 2)) = (𝑦(ball‘𝑀)(𝑐 / 2))) |
55 | 54 | ineq1d 3964 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌)) |
56 | | incom 3956 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2))) |
57 | 55, 56 | syl6eq 2821 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2)))) |
58 | | dfin5 3731 |
. . . . . . . . . . . . . 14
⊢ (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2))) = {𝑧 ∈ 𝑌 ∣ 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))} |
59 | 57, 58 | syl6eq 2821 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = {𝑧 ∈ 𝑌 ∣ 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))}) |
60 | 59 | neeq1d 3002 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ {𝑧 ∈ 𝑌 ∣ 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))} ≠ ∅)) |
61 | | rabn0 4104 |
. . . . . . . . . . . 12
⊢ ({𝑧 ∈ 𝑌 ∣ 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))} ≠ ∅ ↔ ∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) |
62 | 60, 61 | syl6bb 276 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ ∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) |
63 | 62 | elrab 3515 |
. . . . . . . . . 10
⊢ (𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ↔ (𝑦 ∈ 𝑣 ∧ ∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) |
64 | 63 | simprbi 484 |
. . . . . . . . 9
⊢ (𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} → ∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) |
65 | 64 | rgen 3071 |
. . . . . . . 8
⊢
∀𝑦 ∈
{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)) |
66 | | eleq1 2838 |
. . . . . . . . 9
⊢ (𝑧 = (𝑓‘𝑦) → (𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)) ↔ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) |
67 | 66 | ac6sfi 8360 |
. . . . . . . 8
⊢ (({𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin ∧
∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → ∃𝑓(𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) |
68 | 53, 65, 67 | sylancl 574 |
. . . . . . 7
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ∃𝑓(𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) |
69 | | fdm 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → dom 𝑓 = {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}) |
70 | 69 | ad2antrl 707 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → dom 𝑓 = {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}) |
71 | 70, 51 | syl6eqss 3804 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → dom 𝑓 ⊆ 𝑣) |
72 | | simprl 754 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌) |
73 | 70 | feq2d 6171 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓:dom 𝑓⟶𝑌 ↔ 𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌)) |
74 | 72, 73 | mpbird 247 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑓:dom 𝑓⟶𝑌) |
75 | | simprr 756 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) |
76 | | ffn 6185 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → 𝑓 Fn {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}) |
77 | | elpreima 6480 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 Fn {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} → (𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∧ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → (𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∧ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))) |
79 | 78 | baibd 529 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ 𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}) → (𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) |
80 | 79 | ralbidva 3134 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → (∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) |
81 | 80 | ad2antrl 707 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) |
82 | 75, 81 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) |
83 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑥 → 𝑦 = 𝑥) |
84 | | oveq1 6800 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → (𝑦(ball‘𝑀)(𝑐 / 2)) = (𝑥(ball‘𝑀)(𝑐 / 2))) |
85 | 84 | imaeq2d 5607 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑥 → (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) = (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))) |
86 | 83, 85 | eleq12d 2844 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → (𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))) |
87 | 86 | ralrab2 3524 |
. . . . . . . . . . . . 13
⊢
(∀𝑦 ∈
{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))) |
88 | 82, 87 | sylib 208 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))) |
89 | 71, 74, 88 | 3jca 1122 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) |
90 | 89 | ex 397 |
. . . . . . . . . 10
⊢ (𝑣 ∈ Fin → ((𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))))) |
91 | 50, 90 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ((𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))))) |
92 | | simpr2 1235 |
. . . . . . . . . . . . 13
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓:dom 𝑓⟶𝑌) |
93 | | frn 6193 |
. . . . . . . . . . . . 13
⊢ (𝑓:dom 𝑓⟶𝑌 → ran 𝑓 ⊆ 𝑌) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . 12
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓 ⊆ 𝑌) |
95 | | ffn 6185 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:dom 𝑓⟶𝑌 → 𝑓 Fn dom 𝑓) |
96 | 92, 95 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓 Fn dom 𝑓) |
97 | 50 | adantr 466 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑣 ∈ Fin) |
98 | | simpr1 1233 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓 ⊆ 𝑣) |
99 | | ssfi 8336 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∈ Fin ∧ dom 𝑓 ⊆ 𝑣) → dom 𝑓 ∈ Fin) |
100 | 97, 98, 99 | syl2anc 573 |
. . . . . . . . . . . . . 14
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓 ∈ Fin) |
101 | | fnfi 8394 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 Fn dom 𝑓 ∧ dom 𝑓 ∈ Fin) → 𝑓 ∈ Fin) |
102 | 96, 100, 101 | syl2anc 573 |
. . . . . . . . . . . . 13
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓 ∈ Fin) |
103 | | rnfi 8405 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ Fin → ran 𝑓 ∈ Fin) |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . 12
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓 ∈ Fin) |
105 | | elfpw 8424 |
. . . . . . . . . . . 12
⊢ (ran
𝑓 ∈ (𝒫 𝑌 ∩ Fin) ↔ (ran 𝑓 ⊆ 𝑌 ∧ ran 𝑓 ∈ Fin)) |
106 | 94, 104, 105 | sylanbrc 572 |
. . . . . . . . . . 11
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓 ∈ (𝒫 𝑌 ∩ Fin)) |
107 | | oveq1 6800 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (𝑥(ball‘𝑁)𝑐) = (𝑧(ball‘𝑁)𝑐)) |
108 | 107 | cbviunv 4693 |
. . . . . . . . . . . 12
⊢ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) |
109 | 3 | ad4antr 712 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑁 ∈ (Met‘𝑌)) |
110 | | metxmet 22359 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ (Met‘𝑌) → 𝑁 ∈ (∞Met‘𝑌)) |
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑁 ∈ (∞Met‘𝑌)) |
112 | 94 | sselda 3752 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ 𝑌) |
113 | | rpxr 12043 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 ∈ ℝ+
→ 𝑐 ∈
ℝ*) |
114 | 113 | ad4antlr 714 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑐 ∈ ℝ*) |
115 | | blssm 22443 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝑧 ∈ 𝑌 ∧ 𝑐 ∈ ℝ*) → (𝑧(ball‘𝑁)𝑐) ⊆ 𝑌) |
116 | 111, 112,
114, 115 | syl3anc 1476 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → (𝑧(ball‘𝑁)𝑐) ⊆ 𝑌) |
117 | 116 | ralrimiva 3115 |
. . . . . . . . . . . . . 14
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌) |
118 | | iunss 4695 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌 ↔ ∀𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌) |
119 | 117, 118 | sylibr 224 |
. . . . . . . . . . . . 13
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌) |
120 | | iunin1 4719 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = (∪
𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) |
121 | | simplrr 763 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))) |
122 | 54 | cbviunv 4693 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)) = ∪
𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) |
123 | 121, 122 | syl6sseq 3800 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 ⊆ ∪
𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2))) |
124 | | sseqin2 3968 |
. . . . . . . . . . . . . . . 16
⊢ (𝑌 ⊆ ∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ↔ (∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌) |
125 | 123, 124 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → (∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌) |
126 | 120, 125 | syl5eq 2817 |
. . . . . . . . . . . . . 14
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌) |
127 | | 0ss 4116 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∅
⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) |
128 | | sseq1 3775 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ∅ → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ↔ ∅ ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))) |
129 | 127, 128 | mpbiri 248 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ∅ → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)) |
130 | 129 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ∅ → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))) |
131 | | simpr3 1237 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))) |
132 | 55 | neeq1d 3002 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅)) |
133 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
134 | 54 | imaeq2d 5607 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑦 → (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))) = (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) |
135 | 133, 134 | eleq12d 2844 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑦 → (𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))) ↔ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))) |
136 | 132, 135 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑦 → ((((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))) ↔ (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))))) |
137 | 136 | rspccva 3459 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑥 ∈
𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ 𝑦 ∈ 𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))) |
138 | 131, 137 | sylan 569 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))) |
139 | 14 | ad5antr 716 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑀 ∈ (∞Met‘𝑋)) |
140 | | cnvimass 5626 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ⊆ dom 𝑓 |
141 | 48 | simplbi 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ⊆ 𝑋) |
142 | 141 | ad2antrl 707 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → 𝑣 ⊆ 𝑋) |
143 | 142 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑣 ⊆ 𝑋) |
144 | 98, 143 | sstrd 3762 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓 ⊆ 𝑋) |
145 | 140, 144 | syl5ss 3763 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ⊆ 𝑋) |
146 | 145 | sselda 3752 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑦 ∈ 𝑋) |
147 | | simp-4r 770 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ+) |
148 | 147 | rpred 12075 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ) |
149 | | elpreima 6480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 Fn dom 𝑓 → (𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑦 ∈ dom 𝑓 ∧ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))) |
150 | 149 | simplbda 487 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓 Fn dom 𝑓 ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) |
151 | 96, 150 | sylan 569 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) |
152 | | blhalf 22430 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑐 ∈ ℝ ∧ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑦(ball‘𝑀)(𝑐 / 2)) ⊆ ((𝑓‘𝑦)(ball‘𝑀)𝑐)) |
153 | 139, 146,
148, 151, 152 | syl22anc 1477 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑦(ball‘𝑀)(𝑐 / 2)) ⊆ ((𝑓‘𝑦)(ball‘𝑀)𝑐)) |
154 | 153 | ssrind 3988 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ (((𝑓‘𝑦)(ball‘𝑀)𝑐) ∩ 𝑌)) |
155 | 140 | sseli 3748 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) → 𝑦 ∈ dom 𝑓) |
156 | | ffvelrn 6500 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓:dom 𝑓⟶𝑌 ∧ 𝑦 ∈ dom 𝑓) → (𝑓‘𝑦) ∈ 𝑌) |
157 | 92, 155, 156 | syl2an 583 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ 𝑌) |
158 | | simp-5r 774 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑌 ⊆ 𝑋) |
159 | 158, 21 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑋 ∩ 𝑌) = 𝑌) |
160 | 157, 159 | eleqtrrd 2853 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ (𝑋 ∩ 𝑌)) |
161 | 113 | ad4antlr 714 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ*) |
162 | 1 | blres 22456 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ (𝑓‘𝑦) ∈ (𝑋 ∩ 𝑌) ∧ 𝑐 ∈ ℝ*) → ((𝑓‘𝑦)(ball‘𝑁)𝑐) = (((𝑓‘𝑦)(ball‘𝑀)𝑐) ∩ 𝑌)) |
163 | 139, 160,
161, 162 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑓‘𝑦)(ball‘𝑁)𝑐) = (((𝑓‘𝑦)(ball‘𝑀)𝑐) ∩ 𝑌)) |
164 | 154, 163 | sseqtr4d 3791 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ((𝑓‘𝑦)(ball‘𝑁)𝑐)) |
165 | | fnfvelrn 6499 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓 Fn dom 𝑓 ∧ 𝑦 ∈ dom 𝑓) → (𝑓‘𝑦) ∈ ran 𝑓) |
166 | 96, 155, 165 | syl2an 583 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ ran 𝑓) |
167 | | oveq1 6800 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = (𝑓‘𝑦) → (𝑧(ball‘𝑁)𝑐) = ((𝑓‘𝑦)(ball‘𝑁)𝑐)) |
168 | 167 | ssiun2s 4698 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓‘𝑦) ∈ ran 𝑓 → ((𝑓‘𝑦)(ball‘𝑁)𝑐) ⊆ ∪
𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)) |
169 | 166, 168 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑓‘𝑦)(ball‘𝑁)𝑐) ⊆ ∪
𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)) |
170 | 164, 169 | sstrd 3762 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)) |
171 | 170 | adantlr 694 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)) |
172 | 171 | ex 397 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) → (𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))) |
173 | 138, 172 | syld 47 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))) |
174 | 130, 173 | pm2.61dne 3029 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)) |
175 | 174 | ralrimiva 3115 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)) |
176 | | iunss 4695 |
. . . . . . . . . . . . . . 15
⊢ (∪ 𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ↔ ∀𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)) |
177 | 175, 176 | sylibr 224 |
. . . . . . . . . . . . . 14
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)) |
178 | 126, 177 | eqsstr3d 3789 |
. . . . . . . . . . . . 13
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 ⊆ ∪
𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)) |
179 | 119, 178 | eqssd 3769 |
. . . . . . . . . . . 12
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) = 𝑌) |
180 | 108, 179 | syl5eq 2817 |
. . . . . . . . . . 11
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌) |
181 | | iuneq1 4668 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ran 𝑓 → ∪
𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐)) |
182 | 181 | eqeq1d 2773 |
. . . . . . . . . . . 12
⊢ (𝑤 = ran 𝑓 → (∪
𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌 ↔ ∪
𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌)) |
183 | 182 | rspcev 3460 |
. . . . . . . . . . 11
⊢ ((ran
𝑓 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌) |
184 | 106, 180,
183 | syl2anc 573 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌) |
185 | 184 | ex 397 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ((dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)) |
186 | 91, 185 | syld 47 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ((𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)) |
187 | 186 | exlimdv 2013 |
. . . . . . 7
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → (∃𝑓(𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)) |
188 | 68, 187 | mpd 15 |
. . . . . 6
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌) |
189 | 188 | rexlimdvaa 3180 |
. . . . 5
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) →
(∃𝑣 ∈ (𝒫
𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)) |
190 | 47, 189 | syld 47 |
. . . 4
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) →
(∀𝑑 ∈
ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)) |
191 | 190 | ralrimdva 3118 |
. . 3
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → ∀𝑐 ∈ ℝ+ ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)) |
192 | | istotbnd3 33902 |
. . . . 5
⊢ (𝑁 ∈ (TotBnd‘𝑌) ↔ (𝑁 ∈ (Met‘𝑌) ∧ ∀𝑐 ∈ ℝ+ ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)) |
193 | 192 | baib 525 |
. . . 4
⊢ (𝑁 ∈ (Met‘𝑌) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑐 ∈ ℝ+ ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)) |
194 | 3, 193 | syl 17 |
. . 3
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑐 ∈ ℝ+ ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)) |
195 | 191, 194 | sylibrd 249 |
. 2
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → 𝑁 ∈ (TotBnd‘𝑌))) |
196 | 39, 195 | impbid 202 |
1
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))) |