Step | Hyp | Ref
| Expression |
1 | | sstotbnd.2 |
. . . . 5
⊢ 𝑁 = (𝑀 ↾ (𝑌 × 𝑌)) |
2 | | metres2 22691 |
. . . . 5
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑀 ↾ (𝑌 × 𝑌)) ∈ (Met‘𝑌)) |
3 | 1, 2 | syl5eqel 2863 |
. . . 4
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → 𝑁 ∈ (Met‘𝑌)) |
4 | | istotbnd3 34528 |
. . . . 5
⊢ (𝑁 ∈ (TotBnd‘𝑌) ↔ (𝑁 ∈ (Met‘𝑌) ∧ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) |
5 | 4 | baib 528 |
. . . 4
⊢ (𝑁 ∈ (Met‘𝑌) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) |
6 | 3, 5 | syl 17 |
. . 3
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) |
7 | | simpllr 764 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑌 ⊆ 𝑋) |
8 | | sspwb 5194 |
. . . . . . . . . 10
⊢ (𝑌 ⊆ 𝑋 ↔ 𝒫 𝑌 ⊆ 𝒫 𝑋) |
9 | 7, 8 | sylib 210 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝒫 𝑌 ⊆ 𝒫 𝑋) |
10 | 9 | ssrind 4093 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → (𝒫 𝑌 ∩ Fin) ⊆ (𝒫 𝑋 ∩ Fin)) |
11 | | simprl 759 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) |
12 | 10, 11 | sseldd 3852 |
. . . . . . 7
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) |
13 | | simprr 761 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌) |
14 | | metxmet 22662 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀 ∈ (∞Met‘𝑋)) |
15 | 14 | ad4antr 720 |
. . . . . . . . . . . . 13
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑀 ∈ (∞Met‘𝑋)) |
16 | | elfpw 8619 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ↔ (𝑣 ⊆ 𝑌 ∧ 𝑣 ∈ Fin)) |
17 | 16 | simplbi 490 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) → 𝑣 ⊆ 𝑌) |
18 | 17 | adantl 474 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) → 𝑣 ⊆ 𝑌) |
19 | 18 | sselda 3851 |
. . . . . . . . . . . . . 14
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ 𝑌) |
20 | | simp-4r 772 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑌 ⊆ 𝑋) |
21 | | sseqin2 4073 |
. . . . . . . . . . . . . . 15
⊢ (𝑌 ⊆ 𝑋 ↔ (𝑋 ∩ 𝑌) = 𝑌) |
22 | 20, 21 | sylib 210 |
. . . . . . . . . . . . . 14
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → (𝑋 ∩ 𝑌) = 𝑌) |
23 | 19, 22 | eleqtrrd 2862 |
. . . . . . . . . . . . 13
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ (𝑋 ∩ 𝑌)) |
24 | | simpllr 764 |
. . . . . . . . . . . . . 14
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑑 ∈ ℝ+) |
25 | 24 | rpxrd 12247 |
. . . . . . . . . . . . 13
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑑 ∈ ℝ*) |
26 | 1 | blres 22759 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ (𝑋 ∩ 𝑌) ∧ 𝑑 ∈ ℝ*) → (𝑥(ball‘𝑁)𝑑) = ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌)) |
27 | 15, 23, 25, 26 | syl3anc 1352 |
. . . . . . . . . . . 12
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → (𝑥(ball‘𝑁)𝑑) = ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌)) |
28 | | inss1 4086 |
. . . . . . . . . . . 12
⊢ ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌) ⊆ (𝑥(ball‘𝑀)𝑑) |
29 | 27, 28 | syl6eqss 3904 |
. . . . . . . . . . 11
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑)) |
30 | 29 | ralrimiva 3125 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) →
∀𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑)) |
31 | | ss2iun 4805 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑) → ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)) |
32 | 30, 31 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)) |
33 | 32 | adantrr 705 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)) |
34 | 13, 33 | eqsstr3d 3889 |
. . . . . . 7
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)) |
35 | 12, 34 | jca 504 |
. . . . . 6
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))) |
36 | 35 | ex 405 |
. . . . 5
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) → ((𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌) → (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)))) |
37 | 36 | reximdv2 3209 |
. . . 4
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ+) →
(∃𝑣 ∈ (𝒫
𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌 → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))) |
38 | 37 | ralimdva 3120 |
. . 3
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌 → ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))) |
39 | 6, 38 | sylbid 232 |
. 2
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) → ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))) |
40 | | simpr 477 |
. . . . . . 7
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) → 𝑐 ∈
ℝ+) |
41 | 40 | rphalfcld 12258 |
. . . . . 6
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) → (𝑐 / 2) ∈
ℝ+) |
42 | | oveq2 6982 |
. . . . . . . . . 10
⊢ (𝑑 = (𝑐 / 2) → (𝑥(ball‘𝑀)𝑑) = (𝑥(ball‘𝑀)(𝑐 / 2))) |
43 | 42 | iuneq2d 4816 |
. . . . . . . . 9
⊢ (𝑑 = (𝑐 / 2) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))) |
44 | 43 | sseq2d 3882 |
. . . . . . . 8
⊢ (𝑑 = (𝑐 / 2) → (𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) ↔ 𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) |
45 | 44 | rexbidv 3235 |
. . . . . . 7
⊢ (𝑑 = (𝑐 / 2) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) ↔ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) |
46 | 45 | rspcv 3524 |
. . . . . 6
⊢ ((𝑐 / 2) ∈ ℝ+
→ (∀𝑑 ∈
ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) |
47 | 41, 46 | syl 17 |
. . . . 5
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) →
(∀𝑑 ∈
ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) |
48 | | elfpw 8619 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ↔ (𝑣 ⊆ 𝑋 ∧ 𝑣 ∈ Fin)) |
49 | 48 | simprbi 489 |
. . . . . . . . . 10
⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ∈ Fin) |
50 | 49 | ad2antrl 716 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → 𝑣 ∈ Fin) |
51 | | ssrab2 3939 |
. . . . . . . . 9
⊢ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ⊆ 𝑣 |
52 | | ssfi 8531 |
. . . . . . . . 9
⊢ ((𝑣 ∈ Fin ∧ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ⊆ 𝑣) → {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin) |
53 | 50, 51, 52 | sylancl 578 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin) |
54 | | oveq1 6981 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝑥(ball‘𝑀)(𝑐 / 2)) = (𝑦(ball‘𝑀)(𝑐 / 2))) |
55 | 54 | ineq1d 4069 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌)) |
56 | | incom 4060 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2))) |
57 | 55, 56 | syl6eq 2823 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2)))) |
58 | | dfin5 3830 |
. . . . . . . . . . . . . 14
⊢ (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2))) = {𝑧 ∈ 𝑌 ∣ 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))} |
59 | 57, 58 | syl6eq 2823 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = {𝑧 ∈ 𝑌 ∣ 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))}) |
60 | 59 | neeq1d 3019 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ {𝑧 ∈ 𝑌 ∣ 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))} ≠ ∅)) |
61 | | rabn0 4219 |
. . . . . . . . . . . 12
⊢ ({𝑧 ∈ 𝑌 ∣ 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))} ≠ ∅ ↔ ∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) |
62 | 60, 61 | syl6bb 279 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ ∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) |
63 | 62 | elrab 3588 |
. . . . . . . . . 10
⊢ (𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ↔ (𝑦 ∈ 𝑣 ∧ ∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) |
64 | 63 | simprbi 489 |
. . . . . . . . 9
⊢ (𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} → ∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) |
65 | 64 | rgen 3091 |
. . . . . . . 8
⊢
∀𝑦 ∈
{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)) |
66 | | eleq1 2846 |
. . . . . . . . 9
⊢ (𝑧 = (𝑓‘𝑦) → (𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)) ↔ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) |
67 | 66 | ac6sfi 8555 |
. . . . . . . 8
⊢ (({𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin ∧
∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → ∃𝑓(𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) |
68 | 53, 65, 67 | sylancl 578 |
. . . . . . 7
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ∃𝑓(𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) |
69 | | fdm 6349 |
. . . . . . . . . . . . . 14
⊢ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → dom 𝑓 = {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}) |
70 | 69 | ad2antrl 716 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → dom 𝑓 = {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}) |
71 | 70, 51 | syl6eqss 3904 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → dom 𝑓 ⊆ 𝑣) |
72 | | simprl 759 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌) |
73 | 70 | feq2d 6327 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓:dom 𝑓⟶𝑌 ↔ 𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌)) |
74 | 72, 73 | mpbird 249 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑓:dom 𝑓⟶𝑌) |
75 | | simprr 761 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) |
76 | | ffn 6341 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → 𝑓 Fn {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}) |
77 | | elpreima 6651 |
. . . . . . . . . . . . . . . . . 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 532 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ 𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}) → (𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) |
80 | 79 | ralbidva 3139 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → (∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) |
81 | 80 | ad2antrl 716 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) |
82 | 75, 81 | mpbird 249 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) |
83 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑥 → 𝑦 = 𝑥) |
84 | | oveq1 6981 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → (𝑦(ball‘𝑀)(𝑐 / 2)) = (𝑥(ball‘𝑀)(𝑐 / 2))) |
85 | 84 | imaeq2d 5767 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑥 → (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) = (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))) |
86 | 83, 85 | eleq12d 2853 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → (𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))) |
87 | 86 | ralrab2 3598 |
. . . . . . . . . . . . 13
⊢
(∀𝑦 ∈
{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))) |
88 | 82, 87 | sylib 210 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))) |
89 | 71, 74, 88 | 3jca 1109 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) |
90 | 89 | ex 405 |
. . . . . . . . . 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 1176 |
. . . . . . . . . . . . 13
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓:dom 𝑓⟶𝑌) |
93 | 92 | frnd 6348 |
. . . . . . . . . . . 12
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓 ⊆ 𝑌) |
94 | 92 | ffnd 6342 |
. . . . . . . . . . . . . 14
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓 Fn dom 𝑓) |
95 | 50 | adantr 473 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑣 ∈ Fin) |
96 | | simpr1 1175 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓 ⊆ 𝑣) |
97 | | ssfi 8531 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∈ Fin ∧ dom 𝑓 ⊆ 𝑣) → dom 𝑓 ∈ Fin) |
98 | 95, 96, 97 | syl2anc 576 |
. . . . . . . . . . . . . 14
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓 ∈ Fin) |
99 | | fnfi 8589 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 Fn dom 𝑓 ∧ dom 𝑓 ∈ Fin) → 𝑓 ∈ Fin) |
100 | 94, 98, 99 | syl2anc 576 |
. . . . . . . . . . . . 13
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓 ∈ Fin) |
101 | | rnfi 8600 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ Fin → ran 𝑓 ∈ Fin) |
102 | 100, 101 | syl 17 |
. . . . . . . . . . . 12
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓 ∈ Fin) |
103 | | elfpw 8619 |
. . . . . . . . . . . 12
⊢ (ran
𝑓 ∈ (𝒫 𝑌 ∩ Fin) ↔ (ran 𝑓 ⊆ 𝑌 ∧ ran 𝑓 ∈ Fin)) |
104 | 93, 102, 103 | sylanbrc 575 |
. . . . . . . . . . 11
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓 ∈ (𝒫 𝑌 ∩ Fin)) |
105 | | oveq1 6981 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (𝑥(ball‘𝑁)𝑐) = (𝑧(ball‘𝑁)𝑐)) |
106 | 105 | cbviunv 4829 |
. . . . . . . . . . . 12
⊢ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) |
107 | 3 | ad4antr 720 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑁 ∈ (Met‘𝑌)) |
108 | | metxmet 22662 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ (Met‘𝑌) → 𝑁 ∈ (∞Met‘𝑌)) |
109 | 107, 108 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑁 ∈ (∞Met‘𝑌)) |
110 | 93 | sselda 3851 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ 𝑌) |
111 | | rpxr 12213 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 ∈ ℝ+
→ 𝑐 ∈
ℝ*) |
112 | 111 | ad4antlr 721 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑐 ∈ ℝ*) |
113 | | blssm 22746 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝑧 ∈ 𝑌 ∧ 𝑐 ∈ ℝ*) → (𝑧(ball‘𝑁)𝑐) ⊆ 𝑌) |
114 | 109, 110,
112, 113 | syl3anc 1352 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → (𝑧(ball‘𝑁)𝑐) ⊆ 𝑌) |
115 | 114 | ralrimiva 3125 |
. . . . . . . . . . . . . 14
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌) |
116 | | iunss 4831 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌 ↔ ∀𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌) |
117 | 115, 116 | sylibr 226 |
. . . . . . . . . . . . 13
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌) |
118 | | iunin1 4856 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = (∪
𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) |
119 | | simplrr 766 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))) |
120 | 54 | cbviunv 4829 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)) = ∪
𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) |
121 | 119, 120 | syl6sseq 3900 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 ⊆ ∪
𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2))) |
122 | | sseqin2 4073 |
. . . . . . . . . . . . . . . 16
⊢ (𝑌 ⊆ ∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ↔ (∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌) |
123 | 121, 122 | sylib 210 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → (∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌) |
124 | 118, 123 | syl5eq 2819 |
. . . . . . . . . . . . . 14
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌) |
125 | | 0ss 4230 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∅
⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) |
126 | | sseq1 3875 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ∅ → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ↔ ∅ ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))) |
127 | 125, 126 | mpbiri 250 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ∅ → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)) |
128 | 127 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ∅ → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))) |
129 | | simpr3 1177 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))) |
130 | 55 | neeq1d 3019 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅)) |
131 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
132 | 54 | imaeq2d 5767 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑦 → (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))) = (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) |
133 | 131, 132 | eleq12d 2853 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑦 → (𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))) ↔ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))) |
134 | 130, 133 | imbi12d 337 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑦 → ((((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))) ↔ (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))))) |
135 | 134 | rspccva 3527 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑥 ∈
𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ 𝑦 ∈ 𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))) |
136 | 129, 135 | sylan 572 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))) |
137 | 14 | ad5antr 722 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑀 ∈ (∞Met‘𝑋)) |
138 | | cnvimass 5786 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ⊆ dom 𝑓 |
139 | 48 | simplbi 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ⊆ 𝑋) |
140 | 139 | ad2antrl 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → 𝑣 ⊆ 𝑋) |
141 | 140 | adantr 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑣 ⊆ 𝑋) |
142 | 96, 141 | sstrd 3861 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓 ⊆ 𝑋) |
143 | 138, 142 | syl5ss 3862 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ⊆ 𝑋) |
144 | 143 | sselda 3851 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑦 ∈ 𝑋) |
145 | | simp-4r 772 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ+) |
146 | 145 | rpred 12246 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ) |
147 | | elpreima 6651 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 Fn dom 𝑓 → (𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑦 ∈ dom 𝑓 ∧ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))) |
148 | 147 | simplbda 492 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓 Fn dom 𝑓 ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) |
149 | 94, 148 | sylan 572 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) |
150 | | blhalf 22733 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑐 ∈ ℝ ∧ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑦(ball‘𝑀)(𝑐 / 2)) ⊆ ((𝑓‘𝑦)(ball‘𝑀)𝑐)) |
151 | 137, 144,
146, 149, 150 | syl22anc 827 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑦(ball‘𝑀)(𝑐 / 2)) ⊆ ((𝑓‘𝑦)(ball‘𝑀)𝑐)) |
152 | 151 | ssrind 4093 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ (((𝑓‘𝑦)(ball‘𝑀)𝑐) ∩ 𝑌)) |
153 | 138 | sseli 3847 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) → 𝑦 ∈ dom 𝑓) |
154 | | ffvelrn 6672 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓:dom 𝑓⟶𝑌 ∧ 𝑦 ∈ dom 𝑓) → (𝑓‘𝑦) ∈ 𝑌) |
155 | 92, 153, 154 | syl2an 587 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ 𝑌) |
156 | | simp-5r 774 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑌 ⊆ 𝑋) |
157 | 156, 21 | sylib 210 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑋 ∩ 𝑌) = 𝑌) |
158 | 155, 157 | eleqtrrd 2862 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ (𝑋 ∩ 𝑌)) |
159 | 111 | ad4antlr 721 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ*) |
160 | 1 | blres 22759 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ (𝑓‘𝑦) ∈ (𝑋 ∩ 𝑌) ∧ 𝑐 ∈ ℝ*) → ((𝑓‘𝑦)(ball‘𝑁)𝑐) = (((𝑓‘𝑦)(ball‘𝑀)𝑐) ∩ 𝑌)) |
161 | 137, 158,
159, 160 | syl3anc 1352 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑓‘𝑦)(ball‘𝑁)𝑐) = (((𝑓‘𝑦)(ball‘𝑀)𝑐) ∩ 𝑌)) |
162 | 152, 161 | sseqtr4d 3891 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ((𝑓‘𝑦)(ball‘𝑁)𝑐)) |
163 | | fnfvelrn 6671 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓 Fn dom 𝑓 ∧ 𝑦 ∈ dom 𝑓) → (𝑓‘𝑦) ∈ ran 𝑓) |
164 | 94, 153, 163 | syl2an 587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ ran 𝑓) |
165 | | oveq1 6981 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = (𝑓‘𝑦) → (𝑧(ball‘𝑁)𝑐) = ((𝑓‘𝑦)(ball‘𝑁)𝑐)) |
166 | 165 | ssiun2s 4834 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓‘𝑦) ∈ ran 𝑓 → ((𝑓‘𝑦)(ball‘𝑁)𝑐) ⊆ ∪
𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)) |
167 | 164, 166 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑓‘𝑦)(ball‘𝑁)𝑐) ⊆ ∪
𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)) |
168 | 162, 167 | sstrd 3861 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)) |
169 | 168 | adantlr 703 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) ∧ 𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)) |
170 | 169 | ex 405 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) → (𝑦 ∈ (◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))) |
171 | 136, 170 | syld 47 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))) |
172 | 128, 171 | pm2.61dne 3047 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)) |
173 | 172 | ralrimiva 3125 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)) |
174 | | iunss 4831 |
. . . . . . . . . . . . . . 15
⊢ (∪ 𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ↔ ∀𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)) |
175 | 173, 174 | sylibr 226 |
. . . . . . . . . . . . . 14
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)) |
176 | 124, 175 | eqsstr3d 3889 |
. . . . . . . . . . . . 13
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 ⊆ ∪
𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)) |
177 | 117, 176 | eqssd 3868 |
. . . . . . . . . . . 12
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) = 𝑌) |
178 | 106, 177 | syl5eq 2819 |
. . . . . . . . . . 11
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌) |
179 | | iuneq1 4803 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ran 𝑓 → ∪
𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐)) |
180 | 179 | eqeq1d 2773 |
. . . . . . . . . . . 12
⊢ (𝑤 = ran 𝑓 → (∪
𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌 ↔ ∪
𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌)) |
181 | 180 | rspcev 3528 |
. . . . . . . . . . 11
⊢ ((ran
𝑓 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌) |
182 | 104, 178,
181 | syl2anc 576 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌) |
183 | 182 | ex 405 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ((dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)) |
184 | 91, 183 | syld 47 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ((𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)) |
185 | 184 | exlimdv 1893 |
. . . . . . 7
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → (∃𝑓(𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)) |
186 | 68, 185 | mpd 15 |
. . . . . 6
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌) |
187 | 186 | rexlimdvaa 3223 |
. . . . 5
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) →
(∃𝑣 ∈ (𝒫
𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)) |
188 | 47, 187 | syld 47 |
. . . 4
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ+) →
(∀𝑑 ∈
ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)) |
189 | 188 | ralrimdva 3132 |
. . 3
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → ∀𝑐 ∈ ℝ+ ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)) |
190 | | istotbnd3 34528 |
. . . . 5
⊢ (𝑁 ∈ (TotBnd‘𝑌) ↔ (𝑁 ∈ (Met‘𝑌) ∧ ∀𝑐 ∈ ℝ+ ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)) |
191 | 190 | baib 528 |
. . . 4
⊢ (𝑁 ∈ (Met‘𝑌) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑐 ∈ ℝ+ ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)) |
192 | 3, 191 | syl 17 |
. . 3
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑐 ∈ ℝ+ ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)) |
193 | 189, 192 | sylibrd 251 |
. 2
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → 𝑁 ∈ (TotBnd‘𝑌))) |
194 | 39, 193 | impbid 204 |
1
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))) |