Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sstotbnd2 Structured version   Visualization version   GIF version

Theorem sstotbnd2 36233
Description: Condition for a subset of a metric space to be totally bounded. (Contributed by Mario Carneiro, 12-Sep-2015.)
Hypothesis
Ref Expression
sstotbnd.2 𝑁 = (𝑀 ↾ (𝑌 × 𝑌))
Assertion
Ref Expression
sstotbnd2 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑)))
Distinct variable groups:   𝑣,𝑑,𝑥,𝑀   𝑋,𝑑,𝑣,𝑥   𝑁,𝑑,𝑣,𝑥   𝑌,𝑑,𝑣,𝑥

Proof of Theorem sstotbnd2
Dummy variables 𝑐 𝑓 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sstotbnd.2 . . . . 5 𝑁 = (𝑀 ↾ (𝑌 × 𝑌))
2 metres2 23716 . . . . 5 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → (𝑀 ↾ (𝑌 × 𝑌)) ∈ (Met‘𝑌))
31, 2eqeltrid 2842 . . . 4 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → 𝑁 ∈ (Met‘𝑌))
4 istotbnd3 36230 . . . . 5 (𝑁 ∈ (TotBnd‘𝑌) ↔ (𝑁 ∈ (Met‘𝑌) ∧ ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌))
54baib 536 . . . 4 (𝑁 ∈ (Met‘𝑌) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌))
63, 5syl 17 . . 3 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌))
7 simpllr 774 . . . . . . . . . 10 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑌𝑋)
87sspwd 4573 . . . . . . . . 9 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝒫 𝑌 ⊆ 𝒫 𝑋)
98ssrind 4195 . . . . . . . 8 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → (𝒫 𝑌 ∩ Fin) ⊆ (𝒫 𝑋 ∩ Fin))
10 simprl 769 . . . . . . . 8 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑣 ∈ (𝒫 𝑌 ∩ Fin))
119, 10sseldd 3945 . . . . . . 7 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑣 ∈ (𝒫 𝑋 ∩ Fin))
12 simprr 771 . . . . . . . 8 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)
13 metxmet 23687 . . . . . . . . . . . . . 14 (𝑀 ∈ (Met‘𝑋) → 𝑀 ∈ (∞Met‘𝑋))
1413ad4antr 730 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → 𝑀 ∈ (∞Met‘𝑋))
15 elfpw 9298 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ↔ (𝑣𝑌𝑣 ∈ Fin))
1615simplbi 498 . . . . . . . . . . . . . . . 16 (𝑣 ∈ (𝒫 𝑌 ∩ Fin) → 𝑣𝑌)
1716adantl 482 . . . . . . . . . . . . . . 15 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) → 𝑣𝑌)
1817sselda 3944 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → 𝑥𝑌)
19 simp-4r 782 . . . . . . . . . . . . . . 15 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → 𝑌𝑋)
20 sseqin2 4175 . . . . . . . . . . . . . . 15 (𝑌𝑋 ↔ (𝑋𝑌) = 𝑌)
2119, 20sylib 217 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → (𝑋𝑌) = 𝑌)
2218, 21eleqtrrd 2841 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → 𝑥 ∈ (𝑋𝑌))
23 simpllr 774 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → 𝑑 ∈ ℝ+)
2423rpxrd 12958 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → 𝑑 ∈ ℝ*)
251blres 23784 . . . . . . . . . . . . 13 ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ (𝑋𝑌) ∧ 𝑑 ∈ ℝ*) → (𝑥(ball‘𝑁)𝑑) = ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌))
2614, 22, 24, 25syl3anc 1371 . . . . . . . . . . . 12 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → (𝑥(ball‘𝑁)𝑑) = ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌))
27 inss1 4188 . . . . . . . . . . . 12 ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌) ⊆ (𝑥(ball‘𝑀)𝑑)
2826, 27eqsstrdi 3998 . . . . . . . . . . 11 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑))
2928ralrimiva 3143 . . . . . . . . . 10 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) → ∀𝑥𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑))
30 ss2iun 4972 . . . . . . . . . 10 (∀𝑥𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑) → 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑))
3129, 30syl 17 . . . . . . . . 9 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) → 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑))
3231adantrr 715 . . . . . . . 8 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑))
3312, 32eqsstrrd 3983 . . . . . . 7 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑))
3411, 33jca 512 . . . . . 6 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑)))
3534ex 413 . . . . 5 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) → ((𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌) → (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑))))
3635reximdv2 3161 . . . 4 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) → (∃𝑣 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌 → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑)))
3736ralimdva 3164 . . 3 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → (∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌 → ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑)))
386, 37sylbid 239 . 2 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → (𝑁 ∈ (TotBnd‘𝑌) → ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑)))
39 simpr 485 . . . . . . 7 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) → 𝑐 ∈ ℝ+)
4039rphalfcld 12969 . . . . . 6 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) → (𝑐 / 2) ∈ ℝ+)
41 oveq2 7365 . . . . . . . . . 10 (𝑑 = (𝑐 / 2) → (𝑥(ball‘𝑀)𝑑) = (𝑥(ball‘𝑀)(𝑐 / 2)))
4241iuneq2d 4983 . . . . . . . . 9 (𝑑 = (𝑐 / 2) → 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))
4342sseq2d 3976 . . . . . . . 8 (𝑑 = (𝑐 / 2) → (𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) ↔ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
4443rexbidv 3175 . . . . . . 7 (𝑑 = (𝑐 / 2) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) ↔ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
4544rspcv 3577 . . . . . 6 ((𝑐 / 2) ∈ ℝ+ → (∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
4640, 45syl 17 . . . . 5 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) → (∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
47 elfpw 9298 . . . . . . . . . . 11 (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ↔ (𝑣𝑋𝑣 ∈ Fin))
4847simprbi 497 . . . . . . . . . 10 (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ∈ Fin)
4948ad2antrl 726 . . . . . . . . 9 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → 𝑣 ∈ Fin)
50 ssrab2 4037 . . . . . . . . 9 {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ⊆ 𝑣
51 ssfi 9117 . . . . . . . . 9 ((𝑣 ∈ Fin ∧ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ⊆ 𝑣) → {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin)
5249, 50, 51sylancl 586 . . . . . . . 8 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin)
53 oveq1 7364 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑥(ball‘𝑀)(𝑐 / 2)) = (𝑦(ball‘𝑀)(𝑐 / 2)))
5453ineq1d 4171 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌))
55 incom 4161 . . . . . . . . . . . . . . 15 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2)))
5654, 55eqtrdi 2792 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2))))
57 dfin5 3918 . . . . . . . . . . . . . 14 (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2))) = {𝑧𝑌𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))}
5856, 57eqtrdi 2792 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = {𝑧𝑌𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))})
5958neeq1d 3003 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ {𝑧𝑌𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))} ≠ ∅))
60 rabn0 4345 . . . . . . . . . . . 12 ({𝑧𝑌𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))} ≠ ∅ ↔ ∃𝑧𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
6159, 60bitrdi 286 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ ∃𝑧𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
6261elrab 3645 . . . . . . . . . 10 (𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ↔ (𝑦𝑣 ∧ ∃𝑧𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
6362simprbi 497 . . . . . . . . 9 (𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} → ∃𝑧𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
6463rgen 3066 . . . . . . . 8 𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}∃𝑧𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))
65 eleq1 2825 . . . . . . . . 9 (𝑧 = (𝑓𝑦) → (𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)) ↔ (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
6665ac6sfi 9231 . . . . . . . 8 (({𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}∃𝑧𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → ∃𝑓(𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
6752, 64, 66sylancl 586 . . . . . . 7 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ∃𝑓(𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
68 fdm 6677 . . . . . . . . . . . . . 14 (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → dom 𝑓 = {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅})
6968ad2antrl 726 . . . . . . . . . . . . 13 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → dom 𝑓 = {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅})
7069, 50eqsstrdi 3998 . . . . . . . . . . . 12 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → dom 𝑓𝑣)
71 simprl 769 . . . . . . . . . . . . 13 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌)
7269feq2d 6654 . . . . . . . . . . . . 13 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓:dom 𝑓𝑌𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌))
7371, 72mpbird 256 . . . . . . . . . . . 12 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑓:dom 𝑓𝑌)
74 simprr 771 . . . . . . . . . . . . . 14 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
75 ffn 6668 . . . . . . . . . . . . . . . . . 18 (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌𝑓 Fn {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅})
76 elpreima 7008 . . . . . . . . . . . . . . . . . 18 (𝑓 Fn {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} → (𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∧ (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))))
7775, 76syl 17 . . . . . . . . . . . . . . . . 17 (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → (𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∧ (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))))
7877baibd 540 . . . . . . . . . . . . . . . 16 ((𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}) → (𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
7978ralbidva 3172 . . . . . . . . . . . . . . 15 (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → (∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
8079ad2antrl 726 . . . . . . . . . . . . . 14 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
8174, 80mpbird 256 . . . . . . . . . . . . 13 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))
82 id 22 . . . . . . . . . . . . . . 15 (𝑦 = 𝑥𝑦 = 𝑥)
83 oveq1 7364 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑥 → (𝑦(ball‘𝑀)(𝑐 / 2)) = (𝑥(ball‘𝑀)(𝑐 / 2)))
8483imaeq2d 6013 . . . . . . . . . . . . . . 15 (𝑦 = 𝑥 → (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) = (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))
8582, 84eleq12d 2832 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))
8685ralrab2 3656 . . . . . . . . . . . . 13 (∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))
8781, 86sylib 217 . . . . . . . . . . . 12 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))
8870, 73, 873jca 1128 . . . . . . . . . . 11 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))))
8988ex 413 . . . . . . . . . 10 (𝑣 ∈ Fin → ((𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))))
9049, 89syl 17 . . . . . . . . 9 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ((𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))))
91 simpr2 1195 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓:dom 𝑓𝑌)
9291frnd 6676 . . . . . . . . . . . 12 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓𝑌)
9391ffnd 6669 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓 Fn dom 𝑓)
9449adantr 481 . . . . . . . . . . . . . . 15 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑣 ∈ Fin)
95 simpr1 1194 . . . . . . . . . . . . . . 15 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓𝑣)
96 ssfi 9117 . . . . . . . . . . . . . . 15 ((𝑣 ∈ Fin ∧ dom 𝑓𝑣) → dom 𝑓 ∈ Fin)
9794, 95, 96syl2anc 584 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓 ∈ Fin)
98 fnfi 9125 . . . . . . . . . . . . . 14 ((𝑓 Fn dom 𝑓 ∧ dom 𝑓 ∈ Fin) → 𝑓 ∈ Fin)
9993, 97, 98syl2anc 584 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓 ∈ Fin)
100 rnfi 9279 . . . . . . . . . . . . 13 (𝑓 ∈ Fin → ran 𝑓 ∈ Fin)
10199, 100syl 17 . . . . . . . . . . . 12 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓 ∈ Fin)
102 elfpw 9298 . . . . . . . . . . . 12 (ran 𝑓 ∈ (𝒫 𝑌 ∩ Fin) ↔ (ran 𝑓𝑌 ∧ ran 𝑓 ∈ Fin))
10392, 101, 102sylanbrc 583 . . . . . . . . . . 11 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓 ∈ (𝒫 𝑌 ∩ Fin))
104 oveq1 7364 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑥(ball‘𝑁)𝑐) = (𝑧(ball‘𝑁)𝑐))
105104cbviunv 5000 . . . . . . . . . . . 12 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)
1063ad4antr 730 . . . . . . . . . . . . . . . . 17 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑁 ∈ (Met‘𝑌))
107 metxmet 23687 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (Met‘𝑌) → 𝑁 ∈ (∞Met‘𝑌))
108106, 107syl 17 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑁 ∈ (∞Met‘𝑌))
10992sselda 3944 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑧𝑌)
110 rpxr 12924 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ ℝ+𝑐 ∈ ℝ*)
111110ad4antlr 731 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑐 ∈ ℝ*)
112 blssm 23771 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝑧𝑌𝑐 ∈ ℝ*) → (𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
113108, 109, 111, 112syl3anc 1371 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → (𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
114113ralrimiva 3143 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
115 iunss 5005 . . . . . . . . . . . . . 14 ( 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌 ↔ ∀𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
116114, 115sylibr 233 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
117 iunin1 5032 . . . . . . . . . . . . . . 15 𝑦𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ( 𝑦𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌)
118 simplrr 776 . . . . . . . . . . . . . . . . 17 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))
11953cbviunv 5000 . . . . . . . . . . . . . . . . 17 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)) = 𝑦𝑣 (𝑦(ball‘𝑀)(𝑐 / 2))
120118, 119sseqtrdi 3994 . . . . . . . . . . . . . . . 16 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 𝑦𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)))
121 sseqin2 4175 . . . . . . . . . . . . . . . 16 (𝑌 𝑦𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ↔ ( 𝑦𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌)
122120, 121sylib 217 . . . . . . . . . . . . . . 15 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ( 𝑦𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌)
123117, 122eqtrid 2788 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑦𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌)
124 0ss 4356 . . . . . . . . . . . . . . . . . . 19 ∅ ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)
125 sseq1 3969 . . . . . . . . . . . . . . . . . . 19 (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ∅ → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ↔ ∅ ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)))
126124, 125mpbiri 257 . . . . . . . . . . . . . . . . . 18 (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ∅ → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
127126a1i 11 . . . . . . . . . . . . . . . . 17 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ∅ → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)))
128 simpr3 1196 . . . . . . . . . . . . . . . . . . 19 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))
12954neeq1d 3003 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅))
130 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦𝑥 = 𝑦)
13153imaeq2d 6013 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))) = (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))
132130, 131eleq12d 2832 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → (𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))) ↔ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))))
133129, 132imbi12d 344 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → ((((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))) ↔ (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))))
134133rspccva 3580 . . . . . . . . . . . . . . . . . . 19 ((∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ 𝑦𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))))
135128, 134sylan 580 . . . . . . . . . . . . . . . . . 18 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))))
13613ad5antr 732 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑀 ∈ (∞Met‘𝑋))
137 cnvimass 6033 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ⊆ dom 𝑓
13847simplbi 498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣𝑋)
139138ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → 𝑣𝑋)
140139adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑣𝑋)
14195, 140sstrd 3954 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓𝑋)
142137, 141sstrid 3955 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ⊆ 𝑋)
143142sselda 3944 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑦𝑋)
144 simp-4r 782 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ+)
145144rpred 12957 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ)
146 elpreima 7008 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 Fn dom 𝑓 → (𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑦 ∈ dom 𝑓 ∧ (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))))
147146simplbda 500 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 Fn dom 𝑓𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
14893, 147sylan 580 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
149 blhalf 23758 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋) ∧ (𝑐 ∈ ℝ ∧ (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑦(ball‘𝑀)(𝑐 / 2)) ⊆ ((𝑓𝑦)(ball‘𝑀)𝑐))
150136, 143, 145, 148, 149syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑦(ball‘𝑀)(𝑐 / 2)) ⊆ ((𝑓𝑦)(ball‘𝑀)𝑐))
151150ssrind 4195 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ (((𝑓𝑦)(ball‘𝑀)𝑐) ∩ 𝑌))
152137sseli 3940 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) → 𝑦 ∈ dom 𝑓)
153 ffvelcdm 7032 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓:dom 𝑓𝑌𝑦 ∈ dom 𝑓) → (𝑓𝑦) ∈ 𝑌)
15491, 152, 153syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓𝑦) ∈ 𝑌)
155 simp-5r 784 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑌𝑋)
156155, 20sylib 217 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑋𝑌) = 𝑌)
157154, 156eleqtrrd 2841 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓𝑦) ∈ (𝑋𝑌))
158110ad4antlr 731 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ*)
1591blres 23784 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀 ∈ (∞Met‘𝑋) ∧ (𝑓𝑦) ∈ (𝑋𝑌) ∧ 𝑐 ∈ ℝ*) → ((𝑓𝑦)(ball‘𝑁)𝑐) = (((𝑓𝑦)(ball‘𝑀)𝑐) ∩ 𝑌))
160136, 157, 158, 159syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑓𝑦)(ball‘𝑁)𝑐) = (((𝑓𝑦)(ball‘𝑀)𝑐) ∩ 𝑌))
161151, 160sseqtrrd 3985 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ((𝑓𝑦)(ball‘𝑁)𝑐))
162 fnfvelrn 7031 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓 Fn dom 𝑓𝑦 ∈ dom 𝑓) → (𝑓𝑦) ∈ ran 𝑓)
16393, 152, 162syl2an 596 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓𝑦) ∈ ran 𝑓)
164 oveq1 7364 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (𝑓𝑦) → (𝑧(ball‘𝑁)𝑐) = ((𝑓𝑦)(ball‘𝑁)𝑐))
165164ssiun2s 5008 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑦) ∈ ran 𝑓 → ((𝑓𝑦)(ball‘𝑁)𝑐) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
166163, 165syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑓𝑦)(ball‘𝑁)𝑐) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
167161, 166sstrd 3954 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
168167adantlr 713 . . . . . . . . . . . . . . . . . . 19 (((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦𝑣) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
169168ex 413 . . . . . . . . . . . . . . . . . 18 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦𝑣) → (𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)))
170135, 169syld 47 . . . . . . . . . . . . . . . . 17 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)))
171127, 170pm2.61dne 3031 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦𝑣) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
172171ralrimiva 3143 . . . . . . . . . . . . . . 15 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑦𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
173 iunss 5005 . . . . . . . . . . . . . . 15 ( 𝑦𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ↔ ∀𝑦𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
174172, 173sylibr 233 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑦𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
175123, 174eqsstrrd 3983 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
176116, 175eqssd 3961 . . . . . . . . . . . 12 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) = 𝑌)
177105, 176eqtrid 2788 . . . . . . . . . . 11 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌)
178 iuneq1 4970 . . . . . . . . . . . . 13 (𝑤 = ran 𝑓 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐))
179178eqeq1d 2738 . . . . . . . . . . . 12 (𝑤 = ran 𝑓 → ( 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌))
180179rspcev 3581 . . . . . . . . . . 11 ((ran 𝑓 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)
181103, 177, 180syl2anc 584 . . . . . . . . . 10 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)
182181ex 413 . . . . . . . . 9 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ((dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
18390, 182syld 47 . . . . . . . 8 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ((𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
184183exlimdv 1936 . . . . . . 7 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → (∃𝑓(𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
18567, 184mpd 15 . . . . . 6 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)
186185rexlimdvaa 3153 . . . . 5 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
18746, 186syld 47 . . . 4 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) → (∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
188187ralrimdva 3151 . . 3 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → (∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) → ∀𝑐 ∈ ℝ+𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
189 istotbnd3 36230 . . . . 5 (𝑁 ∈ (TotBnd‘𝑌) ↔ (𝑁 ∈ (Met‘𝑌) ∧ ∀𝑐 ∈ ℝ+𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
190189baib 536 . . . 4 (𝑁 ∈ (Met‘𝑌) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑐 ∈ ℝ+𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
1913, 190syl 17 . . 3 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑐 ∈ ℝ+𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
192188, 191sylibrd 258 . 2 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → (∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) → 𝑁 ∈ (TotBnd‘𝑌)))
19338, 192impbid 211 1 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wex 1781  wcel 2106  wne 2943  wral 3064  wrex 3073  {crab 3407  cin 3909  wss 3910  c0 4282  𝒫 cpw 4560   ciun 4954   × cxp 5631  ccnv 5632  dom cdm 5633  ran crn 5634  cres 5635  cima 5636   Fn wfn 6491  wf 6492  cfv 6496  (class class class)co 7357  Fincfn 8883  cr 11050  *cxr 11188   / cdiv 11812  2c2 12208  +crp 12915  ∞Metcxmet 20781  Metcmet 20782  ballcbl 20783  TotBndctotbnd 36225
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-1o 8412  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-2 12216  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-totbnd 36227
This theorem is referenced by:  sstotbnd  36234  sstotbnd3  36235
  Copyright terms: Public domain W3C validator