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

Theorem sstotbnd2 35231
 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 22980 . . . . 5 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → (𝑀 ↾ (𝑌 × 𝑌)) ∈ (Met‘𝑌))
31, 2eqeltrid 2894 . . . 4 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → 𝑁 ∈ (Met‘𝑌))
4 istotbnd3 35228 . . . . 5 (𝑁 ∈ (TotBnd‘𝑌) ↔ (𝑁 ∈ (Met‘𝑌) ∧ ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌))
54baib 539 . . . 4 (𝑁 ∈ (Met‘𝑌) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌))
63, 5syl 17 . . 3 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌))
7 simpllr 775 . . . . . . . . . 10 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑌𝑋)
87sspwd 4512 . . . . . . . . 9 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝒫 𝑌 ⊆ 𝒫 𝑋)
98ssrind 4162 . . . . . . . 8 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → (𝒫 𝑌 ∩ Fin) ⊆ (𝒫 𝑋 ∩ Fin))
10 simprl 770 . . . . . . . 8 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑣 ∈ (𝒫 𝑌 ∩ Fin))
119, 10sseldd 3916 . . . . . . 7 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑣 ∈ (𝒫 𝑋 ∩ Fin))
12 simprr 772 . . . . . . . 8 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)
13 metxmet 22951 . . . . . . . . . . . . . 14 (𝑀 ∈ (Met‘𝑋) → 𝑀 ∈ (∞Met‘𝑋))
1413ad4antr 731 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → 𝑀 ∈ (∞Met‘𝑋))
15 elfpw 8813 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ↔ (𝑣𝑌𝑣 ∈ Fin))
1615simplbi 501 . . . . . . . . . . . . . . . 16 (𝑣 ∈ (𝒫 𝑌 ∩ Fin) → 𝑣𝑌)
1716adantl 485 . . . . . . . . . . . . . . 15 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) → 𝑣𝑌)
1817sselda 3915 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → 𝑥𝑌)
19 simp-4r 783 . . . . . . . . . . . . . . 15 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → 𝑌𝑋)
20 sseqin2 4142 . . . . . . . . . . . . . . 15 (𝑌𝑋 ↔ (𝑋𝑌) = 𝑌)
2119, 20sylib 221 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → (𝑋𝑌) = 𝑌)
2218, 21eleqtrrd 2893 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → 𝑥 ∈ (𝑋𝑌))
23 simpllr 775 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → 𝑑 ∈ ℝ+)
2423rpxrd 12423 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → 𝑑 ∈ ℝ*)
251blres 23048 . . . . . . . . . . . . 13 ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ (𝑋𝑌) ∧ 𝑑 ∈ ℝ*) → (𝑥(ball‘𝑁)𝑑) = ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌))
2614, 22, 24, 25syl3anc 1368 . . . . . . . . . . . 12 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → (𝑥(ball‘𝑁)𝑑) = ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌))
27 inss1 4155 . . . . . . . . . . . 12 ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌) ⊆ (𝑥(ball‘𝑀)𝑑)
2826, 27eqsstrdi 3969 . . . . . . . . . . 11 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑))
2928ralrimiva 3149 . . . . . . . . . 10 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) → ∀𝑥𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑))
30 ss2iun 4900 . . . . . . . . . 10 (∀𝑥𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑) → 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑))
3129, 30syl 17 . . . . . . . . 9 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) → 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑))
3231adantrr 716 . . . . . . . 8 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑))
3312, 32eqsstrrd 3954 . . . . . . 7 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑))
3411, 33jca 515 . . . . . 6 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑)))
3534ex 416 . . . . 5 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) → ((𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌) → (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑))))
3635reximdv2 3230 . . . 4 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) → (∃𝑣 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌 → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑)))
3736ralimdva 3144 . . 3 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → (∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌 → ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑)))
386, 37sylbid 243 . 2 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → (𝑁 ∈ (TotBnd‘𝑌) → ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑)))
39 simpr 488 . . . . . . 7 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) → 𝑐 ∈ ℝ+)
4039rphalfcld 12434 . . . . . 6 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) → (𝑐 / 2) ∈ ℝ+)
41 oveq2 7144 . . . . . . . . . 10 (𝑑 = (𝑐 / 2) → (𝑥(ball‘𝑀)𝑑) = (𝑥(ball‘𝑀)(𝑐 / 2)))
4241iuneq2d 4911 . . . . . . . . 9 (𝑑 = (𝑐 / 2) → 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))
4342sseq2d 3947 . . . . . . . 8 (𝑑 = (𝑐 / 2) → (𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) ↔ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
4443rexbidv 3256 . . . . . . 7 (𝑑 = (𝑐 / 2) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) ↔ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
4544rspcv 3566 . . . . . 6 ((𝑐 / 2) ∈ ℝ+ → (∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
4640, 45syl 17 . . . . 5 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) → (∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
47 elfpw 8813 . . . . . . . . . . 11 (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ↔ (𝑣𝑋𝑣 ∈ Fin))
4847simprbi 500 . . . . . . . . . 10 (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ∈ Fin)
4948ad2antrl 727 . . . . . . . . 9 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → 𝑣 ∈ Fin)
50 ssrab2 4007 . . . . . . . . 9 {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ⊆ 𝑣
51 ssfi 8725 . . . . . . . . 9 ((𝑣 ∈ Fin ∧ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ⊆ 𝑣) → {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin)
5249, 50, 51sylancl 589 . . . . . . . 8 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin)
53 oveq1 7143 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑥(ball‘𝑀)(𝑐 / 2)) = (𝑦(ball‘𝑀)(𝑐 / 2)))
5453ineq1d 4138 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌))
55 incom 4128 . . . . . . . . . . . . . . 15 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2)))
5654, 55eqtrdi 2849 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2))))
57 dfin5 3889 . . . . . . . . . . . . . 14 (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2))) = {𝑧𝑌𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))}
5856, 57eqtrdi 2849 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = {𝑧𝑌𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))})
5958neeq1d 3046 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ {𝑧𝑌𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))} ≠ ∅))
60 rabn0 4293 . . . . . . . . . . . 12 ({𝑧𝑌𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))} ≠ ∅ ↔ ∃𝑧𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
6159, 60syl6bb 290 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ ∃𝑧𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
6261elrab 3628 . . . . . . . . . 10 (𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ↔ (𝑦𝑣 ∧ ∃𝑧𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
6362simprbi 500 . . . . . . . . 9 (𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} → ∃𝑧𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
6463rgen 3116 . . . . . . . 8 𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}∃𝑧𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))
65 eleq1 2877 . . . . . . . . 9 (𝑧 = (𝑓𝑦) → (𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)) ↔ (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
6665ac6sfi 8749 . . . . . . . 8 (({𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}∃𝑧𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → ∃𝑓(𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
6752, 64, 66sylancl 589 . . . . . . 7 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ∃𝑓(𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
68 fdm 6496 . . . . . . . . . . . . . 14 (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → dom 𝑓 = {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅})
6968ad2antrl 727 . . . . . . . . . . . . 13 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → dom 𝑓 = {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅})
7069, 50eqsstrdi 3969 . . . . . . . . . . . 12 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → dom 𝑓𝑣)
71 simprl 770 . . . . . . . . . . . . 13 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌)
7269feq2d 6474 . . . . . . . . . . . . 13 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓:dom 𝑓𝑌𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌))
7371, 72mpbird 260 . . . . . . . . . . . 12 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑓:dom 𝑓𝑌)
74 simprr 772 . . . . . . . . . . . . . 14 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
75 ffn 6488 . . . . . . . . . . . . . . . . . 18 (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌𝑓 Fn {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅})
76 elpreima 6806 . . . . . . . . . . . . . . . . . 18 (𝑓 Fn {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} → (𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∧ (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))))
7775, 76syl 17 . . . . . . . . . . . . . . . . 17 (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → (𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∧ (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))))
7877baibd 543 . . . . . . . . . . . . . . . 16 ((𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}) → (𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
7978ralbidva 3161 . . . . . . . . . . . . . . 15 (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → (∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
8079ad2antrl 727 . . . . . . . . . . . . . 14 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
8174, 80mpbird 260 . . . . . . . . . . . . 13 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))
82 id 22 . . . . . . . . . . . . . . 15 (𝑦 = 𝑥𝑦 = 𝑥)
83 oveq1 7143 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑥 → (𝑦(ball‘𝑀)(𝑐 / 2)) = (𝑥(ball‘𝑀)(𝑐 / 2)))
8483imaeq2d 5897 . . . . . . . . . . . . . . 15 (𝑦 = 𝑥 → (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) = (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))
8582, 84eleq12d 2884 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))
8685ralrab2 3638 . . . . . . . . . . . . 13 (∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))
8781, 86sylib 221 . . . . . . . . . . . 12 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))
8870, 73, 873jca 1125 . . . . . . . . . . 11 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))))
8988ex 416 . . . . . . . . . 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 1192 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓:dom 𝑓𝑌)
9291frnd 6495 . . . . . . . . . . . 12 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓𝑌)
9391ffnd 6489 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓 Fn dom 𝑓)
9449adantr 484 . . . . . . . . . . . . . . 15 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑣 ∈ Fin)
95 simpr1 1191 . . . . . . . . . . . . . . 15 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓𝑣)
96 ssfi 8725 . . . . . . . . . . . . . . 15 ((𝑣 ∈ Fin ∧ dom 𝑓𝑣) → dom 𝑓 ∈ Fin)
9794, 95, 96syl2anc 587 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓 ∈ Fin)
98 fnfi 8783 . . . . . . . . . . . . . 14 ((𝑓 Fn dom 𝑓 ∧ dom 𝑓 ∈ Fin) → 𝑓 ∈ Fin)
9993, 97, 98syl2anc 587 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓 ∈ Fin)
100 rnfi 8794 . . . . . . . . . . . . 13 (𝑓 ∈ Fin → ran 𝑓 ∈ Fin)
10199, 100syl 17 . . . . . . . . . . . 12 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓 ∈ Fin)
102 elfpw 8813 . . . . . . . . . . . 12 (ran 𝑓 ∈ (𝒫 𝑌 ∩ Fin) ↔ (ran 𝑓𝑌 ∧ ran 𝑓 ∈ Fin))
10392, 101, 102sylanbrc 586 . . . . . . . . . . 11 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓 ∈ (𝒫 𝑌 ∩ Fin))
104 oveq1 7143 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑥(ball‘𝑁)𝑐) = (𝑧(ball‘𝑁)𝑐))
105104cbviunv 4928 . . . . . . . . . . . 12 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)
1063ad4antr 731 . . . . . . . . . . . . . . . . 17 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑁 ∈ (Met‘𝑌))
107 metxmet 22951 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (Met‘𝑌) → 𝑁 ∈ (∞Met‘𝑌))
108106, 107syl 17 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑁 ∈ (∞Met‘𝑌))
10992sselda 3915 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑧𝑌)
110 rpxr 12389 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ ℝ+𝑐 ∈ ℝ*)
111110ad4antlr 732 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑐 ∈ ℝ*)
112 blssm 23035 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝑧𝑌𝑐 ∈ ℝ*) → (𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
113108, 109, 111, 112syl3anc 1368 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → (𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
114113ralrimiva 3149 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
115 iunss 4933 . . . . . . . . . . . . . 14 ( 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌 ↔ ∀𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
116114, 115sylibr 237 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
117 iunin1 4958 . . . . . . . . . . . . . . 15 𝑦𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ( 𝑦𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌)
118 simplrr 777 . . . . . . . . . . . . . . . . 17 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))
11953cbviunv 4928 . . . . . . . . . . . . . . . . 17 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)) = 𝑦𝑣 (𝑦(ball‘𝑀)(𝑐 / 2))
120118, 119sseqtrdi 3965 . . . . . . . . . . . . . . . 16 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 𝑦𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)))
121 sseqin2 4142 . . . . . . . . . . . . . . . 16 (𝑌 𝑦𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ↔ ( 𝑦𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌)
122120, 121sylib 221 . . . . . . . . . . . . . . 15 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ( 𝑦𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌)
123117, 122syl5eq 2845 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑦𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌)
124 0ss 4304 . . . . . . . . . . . . . . . . . . 19 ∅ ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)
125 sseq1 3940 . . . . . . . . . . . . . . . . . . 19 (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ∅ → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ↔ ∅ ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)))
126124, 125mpbiri 261 . . . . . . . . . . . . . . . . . 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 1193 . . . . . . . . . . . . . . . . . . 19 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))
12954neeq1d 3046 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅))
130 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦𝑥 = 𝑦)
13153imaeq2d 5897 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))) = (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))
132130, 131eleq12d 2884 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → (𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))) ↔ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))))
133129, 132imbi12d 348 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → ((((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))) ↔ (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))))
134133rspccva 3570 . . . . . . . . . . . . . . . . . . 19 ((∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ 𝑦𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))))
135128, 134sylan 583 . . . . . . . . . . . . . . . . . 18 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))))
13613ad5antr 733 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑀 ∈ (∞Met‘𝑋))
137 cnvimass 5917 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ⊆ dom 𝑓
13847simplbi 501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣𝑋)
139138ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → 𝑣𝑋)
140139adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑣𝑋)
14195, 140sstrd 3925 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓𝑋)
142137, 141sstrid 3926 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ⊆ 𝑋)
143142sselda 3915 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑦𝑋)
144 simp-4r 783 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ+)
145144rpred 12422 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ)
146 elpreima 6806 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 Fn dom 𝑓 → (𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑦 ∈ dom 𝑓 ∧ (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))))
147146simplbda 503 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 Fn dom 𝑓𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
14893, 147sylan 583 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
149 blhalf 23022 . . . . . . . . . . . . . . . . . . . . . . . 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 4162 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ (((𝑓𝑦)(ball‘𝑀)𝑐) ∩ 𝑌))
152137sseli 3911 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) → 𝑦 ∈ dom 𝑓)
153 ffvelrn 6827 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓:dom 𝑓𝑌𝑦 ∈ dom 𝑓) → (𝑓𝑦) ∈ 𝑌)
15491, 152, 153syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓𝑦) ∈ 𝑌)
155 simp-5r 785 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑌𝑋)
156155, 20sylib 221 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑋𝑌) = 𝑌)
157154, 156eleqtrrd 2893 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓𝑦) ∈ (𝑋𝑌))
158110ad4antlr 732 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ*)
1591blres 23048 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀 ∈ (∞Met‘𝑋) ∧ (𝑓𝑦) ∈ (𝑋𝑌) ∧ 𝑐 ∈ ℝ*) → ((𝑓𝑦)(ball‘𝑁)𝑐) = (((𝑓𝑦)(ball‘𝑀)𝑐) ∩ 𝑌))
160136, 157, 158, 159syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑓𝑦)(ball‘𝑁)𝑐) = (((𝑓𝑦)(ball‘𝑀)𝑐) ∩ 𝑌))
161151, 160sseqtrrd 3956 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ((𝑓𝑦)(ball‘𝑁)𝑐))
162 fnfvelrn 6826 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓 Fn dom 𝑓𝑦 ∈ dom 𝑓) → (𝑓𝑦) ∈ ran 𝑓)
16393, 152, 162syl2an 598 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓𝑦) ∈ ran 𝑓)
164 oveq1 7143 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (𝑓𝑦) → (𝑧(ball‘𝑁)𝑐) = ((𝑓𝑦)(ball‘𝑁)𝑐))
165164ssiun2s 4936 . . . . . . . . . . . . . . . . . . . . . 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 3925 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
168167adantlr 714 . . . . . . . . . . . . . . . . . . 19 (((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦𝑣) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
169168ex 416 . . . . . . . . . . . . . . . . . 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 3073 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦𝑣) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
172171ralrimiva 3149 . . . . . . . . . . . . . . 15 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑦𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
173 iunss 4933 . . . . . . . . . . . . . . 15 ( 𝑦𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ↔ ∀𝑦𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
174172, 173sylibr 237 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑦𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
175123, 174eqsstrrd 3954 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
176116, 175eqssd 3932 . . . . . . . . . . . 12 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) = 𝑌)
177105, 176syl5eq 2845 . . . . . . . . . . 11 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌)
178 iuneq1 4898 . . . . . . . . . . . . 13 (𝑤 = ran 𝑓 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐))
179178eqeq1d 2800 . . . . . . . . . . . 12 (𝑤 = ran 𝑓 → ( 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌))
180179rspcev 3571 . . . . . . . . . . 11 ((ran 𝑓 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)
181103, 177, 180syl2anc 587 . . . . . . . . . 10 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)
182181ex 416 . . . . . . . . 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 1934 . . . . . . 7 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → (∃𝑓(𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
18567, 184mpd 15 . . . . . 6 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)
186185rexlimdvaa 3244 . . . . 5 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
18746, 186syld 47 . . . 4 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) → (∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
188187ralrimdva 3154 . . 3 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → (∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) → ∀𝑐 ∈ ℝ+𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
189 istotbnd3 35228 . . . . 5 (𝑁 ∈ (TotBnd‘𝑌) ↔ (𝑁 ∈ (Met‘𝑌) ∧ ∀𝑐 ∈ ℝ+𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
190189baib 539 . . . 4 (𝑁 ∈ (Met‘𝑌) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑐 ∈ ℝ+𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
1913, 190syl 17 . . 3 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑐 ∈ ℝ+𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
192188, 191sylibrd 262 . 2 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → (∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) → 𝑁 ∈ (TotBnd‘𝑌)))
19338, 192impbid 215 1 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  {crab 3110   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  𝒫 cpw 4497  ∪ ciun 4882   × cxp 5518  ◡ccnv 5519  dom cdm 5520  ran crn 5521   ↾ cres 5522   “ cima 5523   Fn wfn 6320  ⟶wf 6321  ‘cfv 6325  (class class class)co 7136  Fincfn 8495  ℝcr 10528  ℝ*cxr 10666   / cdiv 11289  2c2 11683  ℝ+crp 12380  ∞Metcxmet 20080  Metcmet 20081  ballcbl 20082  TotBndctotbnd 35223 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4840  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6117  df-ord 6163  df-on 6164  df-lim 6165  df-suc 6166  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-riota 7094  df-ov 7139  df-oprab 7140  df-mpo 7141  df-om 7564  df-1st 7674  df-2nd 7675  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-oadd 8092  df-er 8275  df-map 8394  df-en 8496  df-dom 8497  df-sdom 8498  df-fin 8499  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-2 11691  df-rp 12381  df-xneg 12498  df-xadd 12499  df-xmul 12500  df-psmet 20087  df-xmet 20088  df-met 20089  df-bl 20090  df-totbnd 35225 This theorem is referenced by:  sstotbnd  35232  sstotbnd3  35233
 Copyright terms: Public domain W3C validator