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 35669
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 23261 . . . . 5 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → (𝑀 ↾ (𝑌 × 𝑌)) ∈ (Met‘𝑌))
31, 2eqeltrid 2842 . . . 4 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → 𝑁 ∈ (Met‘𝑌))
4 istotbnd3 35666 . . . . 5 (𝑁 ∈ (TotBnd‘𝑌) ↔ (𝑁 ∈ (Met‘𝑌) ∧ ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌))
54baib 539 . . . 4 (𝑁 ∈ (Met‘𝑌) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌))
63, 5syl 17 . . 3 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌))
7 simpllr 776 . . . . . . . . . 10 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑌𝑋)
87sspwd 4528 . . . . . . . . 9 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝒫 𝑌 ⊆ 𝒫 𝑋)
98ssrind 4150 . . . . . . . 8 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → (𝒫 𝑌 ∩ Fin) ⊆ (𝒫 𝑋 ∩ Fin))
10 simprl 771 . . . . . . . 8 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑣 ∈ (𝒫 𝑌 ∩ Fin))
119, 10sseldd 3902 . . . . . . 7 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑣 ∈ (𝒫 𝑋 ∩ Fin))
12 simprr 773 . . . . . . . 8 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)
13 metxmet 23232 . . . . . . . . . . . . . 14 (𝑀 ∈ (Met‘𝑋) → 𝑀 ∈ (∞Met‘𝑋))
1413ad4antr 732 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → 𝑀 ∈ (∞Met‘𝑋))
15 elfpw 8978 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ↔ (𝑣𝑌𝑣 ∈ Fin))
1615simplbi 501 . . . . . . . . . . . . . . . 16 (𝑣 ∈ (𝒫 𝑌 ∩ Fin) → 𝑣𝑌)
1716adantl 485 . . . . . . . . . . . . . . 15 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) → 𝑣𝑌)
1817sselda 3901 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → 𝑥𝑌)
19 simp-4r 784 . . . . . . . . . . . . . . 15 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → 𝑌𝑋)
20 sseqin2 4130 . . . . . . . . . . . . . . 15 (𝑌𝑋 ↔ (𝑋𝑌) = 𝑌)
2119, 20sylib 221 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → (𝑋𝑌) = 𝑌)
2218, 21eleqtrrd 2841 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → 𝑥 ∈ (𝑋𝑌))
23 simpllr 776 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → 𝑑 ∈ ℝ+)
2423rpxrd 12629 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → 𝑑 ∈ ℝ*)
251blres 23329 . . . . . . . . . . . . 13 ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ (𝑋𝑌) ∧ 𝑑 ∈ ℝ*) → (𝑥(ball‘𝑁)𝑑) = ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌))
2614, 22, 24, 25syl3anc 1373 . . . . . . . . . . . 12 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → (𝑥(ball‘𝑁)𝑑) = ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌))
27 inss1 4143 . . . . . . . . . . . 12 ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌) ⊆ (𝑥(ball‘𝑀)𝑑)
2826, 27eqsstrdi 3955 . . . . . . . . . . 11 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥𝑣) → (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑))
2928ralrimiva 3105 . . . . . . . . . 10 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) → ∀𝑥𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑))
30 ss2iun 4922 . . . . . . . . . 10 (∀𝑥𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑) → 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑))
3129, 30syl 17 . . . . . . . . 9 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) → 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑))
3231adantrr 717 . . . . . . . 8 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ 𝑥𝑣 (𝑥(ball‘𝑀)𝑑))
3312, 32eqsstrrd 3940 . . . . . . 7 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑))
3411, 33jca 515 . . . . . 6 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑)))
3534ex 416 . . . . 5 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) → ((𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌) → (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑))))
3635reximdv2 3190 . . . 4 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑑 ∈ ℝ+) → (∃𝑣 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌 → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑)))
3736ralimdva 3100 . . 3 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → (∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌 → ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑)))
386, 37sylbid 243 . 2 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → (𝑁 ∈ (TotBnd‘𝑌) → ∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑)))
39 simpr 488 . . . . . . 7 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) → 𝑐 ∈ ℝ+)
4039rphalfcld 12640 . . . . . 6 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) → (𝑐 / 2) ∈ ℝ+)
41 oveq2 7221 . . . . . . . . . 10 (𝑑 = (𝑐 / 2) → (𝑥(ball‘𝑀)𝑑) = (𝑥(ball‘𝑀)(𝑐 / 2)))
4241iuneq2d 4933 . . . . . . . . 9 (𝑑 = (𝑐 / 2) → 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))
4342sseq2d 3933 . . . . . . . 8 (𝑑 = (𝑐 / 2) → (𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) ↔ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
4443rexbidv 3216 . . . . . . 7 (𝑑 = (𝑐 / 2) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) ↔ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
4544rspcv 3532 . . . . . 6 ((𝑐 / 2) ∈ ℝ+ → (∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
4640, 45syl 17 . . . . 5 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) → (∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
47 elfpw 8978 . . . . . . . . . . 11 (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ↔ (𝑣𝑋𝑣 ∈ Fin))
4847simprbi 500 . . . . . . . . . 10 (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ∈ Fin)
4948ad2antrl 728 . . . . . . . . 9 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → 𝑣 ∈ Fin)
50 ssrab2 3993 . . . . . . . . 9 {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ⊆ 𝑣
51 ssfi 8851 . . . . . . . . 9 ((𝑣 ∈ Fin ∧ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ⊆ 𝑣) → {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin)
5249, 50, 51sylancl 589 . . . . . . . 8 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin)
53 oveq1 7220 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑥(ball‘𝑀)(𝑐 / 2)) = (𝑦(ball‘𝑀)(𝑐 / 2)))
5453ineq1d 4126 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌))
55 incom 4115 . . . . . . . . . . . . . . 15 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2)))
5654, 55eqtrdi 2794 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2))))
57 dfin5 3874 . . . . . . . . . . . . . 14 (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2))) = {𝑧𝑌𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))}
5856, 57eqtrdi 2794 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = {𝑧𝑌𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))})
5958neeq1d 3000 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ {𝑧𝑌𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))} ≠ ∅))
60 rabn0 4300 . . . . . . . . . . . 12 ({𝑧𝑌𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))} ≠ ∅ ↔ ∃𝑧𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
6159, 60bitrdi 290 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ ∃𝑧𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
6261elrab 3602 . . . . . . . . . 10 (𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ↔ (𝑦𝑣 ∧ ∃𝑧𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
6362simprbi 500 . . . . . . . . 9 (𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} → ∃𝑧𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
6463rgen 3071 . . . . . . . 8 𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}∃𝑧𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))
65 eleq1 2825 . . . . . . . . 9 (𝑧 = (𝑓𝑦) → (𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)) ↔ (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
6665ac6sfi 8915 . . . . . . . 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 6554 . . . . . . . . . . . . . 14 (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → dom 𝑓 = {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅})
6968ad2antrl 728 . . . . . . . . . . . . 13 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → dom 𝑓 = {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅})
7069, 50eqsstrdi 3955 . . . . . . . . . . . 12 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → dom 𝑓𝑣)
71 simprl 771 . . . . . . . . . . . . 13 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌)
7269feq2d 6531 . . . . . . . . . . . . 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 773 . . . . . . . . . . . . . 14 ((𝑣 ∈ Fin ∧ (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
75 ffn 6545 . . . . . . . . . . . . . . . . . 18 (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌𝑓 Fn {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅})
76 elpreima 6878 . . . . . . . . . . . . . . . . . 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 3117 . . . . . . . . . . . . . . 15 (𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → (∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
8079ad2antrl 728 . . . . . . . . . . . . . 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 7220 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑥 → (𝑦(ball‘𝑀)(𝑐 / 2)) = (𝑥(ball‘𝑀)(𝑐 / 2)))
8483imaeq2d 5929 . . . . . . . . . . . . . . 15 (𝑦 = 𝑥 → (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) = (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))
8582, 84eleq12d 2832 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))
8685ralrab2 3612 . . . . . . . . . . . . 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 1130 . . . . . . . . . . 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 1197 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓:dom 𝑓𝑌)
9291frnd 6553 . . . . . . . . . . . 12 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓𝑌)
9391ffnd 6546 . . . . . . . . . . . . . 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 1196 . . . . . . . . . . . . . . 15 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓𝑣)
96 ssfi 8851 . . . . . . . . . . . . . . 15 ((𝑣 ∈ Fin ∧ dom 𝑓𝑣) → dom 𝑓 ∈ Fin)
9794, 95, 96syl2anc 587 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓 ∈ Fin)
98 fnfi 8858 . . . . . . . . . . . . . 14 ((𝑓 Fn dom 𝑓 ∧ dom 𝑓 ∈ Fin) → 𝑓 ∈ Fin)
9993, 97, 98syl2anc 587 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓 ∈ Fin)
100 rnfi 8959 . . . . . . . . . . . . 13 (𝑓 ∈ Fin → ran 𝑓 ∈ Fin)
10199, 100syl 17 . . . . . . . . . . . 12 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓 ∈ Fin)
102 elfpw 8978 . . . . . . . . . . . 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 7220 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑥(ball‘𝑁)𝑐) = (𝑧(ball‘𝑁)𝑐))
105104cbviunv 4949 . . . . . . . . . . . 12 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)
1063ad4antr 732 . . . . . . . . . . . . . . . . 17 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑁 ∈ (Met‘𝑌))
107 metxmet 23232 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (Met‘𝑌) → 𝑁 ∈ (∞Met‘𝑌))
108106, 107syl 17 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑁 ∈ (∞Met‘𝑌))
10992sselda 3901 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑧𝑌)
110 rpxr 12595 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ ℝ+𝑐 ∈ ℝ*)
111110ad4antlr 733 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑐 ∈ ℝ*)
112 blssm 23316 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝑧𝑌𝑐 ∈ ℝ*) → (𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
113108, 109, 111, 112syl3anc 1373 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → (𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
114113ralrimiva 3105 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
115 iunss 4954 . . . . . . . . . . . . . 14 ( 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌 ↔ ∀𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
116114, 115sylibr 237 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
117 iunin1 4980 . . . . . . . . . . . . . . 15 𝑦𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ( 𝑦𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌)
118 simplrr 778 . . . . . . . . . . . . . . . . 17 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))
11953cbviunv 4949 . . . . . . . . . . . . . . . . 17 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)) = 𝑦𝑣 (𝑦(ball‘𝑀)(𝑐 / 2))
120118, 119sseqtrdi 3951 . . . . . . . . . . . . . . . 16 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 𝑦𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)))
121 sseqin2 4130 . . . . . . . . . . . . . . . 16 (𝑌 𝑦𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ↔ ( 𝑦𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌)
122120, 121sylib 221 . . . . . . . . . . . . . . 15 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ( 𝑦𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌)
123117, 122syl5eq 2790 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑦𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌)
124 0ss 4311 . . . . . . . . . . . . . . . . . . 19 ∅ ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)
125 sseq1 3926 . . . . . . . . . . . . . . . . . . 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 1198 . . . . . . . . . . . . . . . . . . 19 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))
12954neeq1d 3000 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅))
130 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦𝑥 = 𝑦)
13153imaeq2d 5929 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))) = (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))
132130, 131eleq12d 2832 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → (𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))) ↔ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))))
133129, 132imbi12d 348 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → ((((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))) ↔ (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))))
134133rspccva 3536 . . . . . . . . . . . . . . . . . . 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 734 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑀 ∈ (∞Met‘𝑋))
137 cnvimass 5949 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ⊆ dom 𝑓
13847simplbi 501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣𝑋)
139138ad2antrl 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → 𝑣𝑋)
140139adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑣𝑋)
14195, 140sstrd 3911 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓𝑋)
142137, 141sstrid 3912 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ⊆ 𝑋)
143142sselda 3901 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑦𝑋)
144 simp-4r 784 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ+)
145144rpred 12628 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ)
146 elpreima 6878 . . . . . . . . . . . . . . . . . . . . . . . . . 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 23303 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋) ∧ (𝑐 ∈ ℝ ∧ (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑦(ball‘𝑀)(𝑐 / 2)) ⊆ ((𝑓𝑦)(ball‘𝑀)𝑐))
150136, 143, 145, 148, 149syl22anc 839 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑦(ball‘𝑀)(𝑐 / 2)) ⊆ ((𝑓𝑦)(ball‘𝑀)𝑐))
151150ssrind 4150 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ (((𝑓𝑦)(ball‘𝑀)𝑐) ∩ 𝑌))
152137sseli 3896 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) → 𝑦 ∈ dom 𝑓)
153 ffvelrn 6902 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓:dom 𝑓𝑌𝑦 ∈ dom 𝑓) → (𝑓𝑦) ∈ 𝑌)
15491, 152, 153syl2an 599 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓𝑦) ∈ 𝑌)
155 simp-5r 786 . . . . . . . . . . . . . . . . . . . . . . . . 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 2841 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓𝑦) ∈ (𝑋𝑌))
158110ad4antlr 733 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ*)
1591blres 23329 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀 ∈ (∞Met‘𝑋) ∧ (𝑓𝑦) ∈ (𝑋𝑌) ∧ 𝑐 ∈ ℝ*) → ((𝑓𝑦)(ball‘𝑁)𝑐) = (((𝑓𝑦)(ball‘𝑀)𝑐) ∩ 𝑌))
160136, 157, 158, 159syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑓𝑦)(ball‘𝑁)𝑐) = (((𝑓𝑦)(ball‘𝑀)𝑐) ∩ 𝑌))
161151, 160sseqtrrd 3942 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ((𝑓𝑦)(ball‘𝑁)𝑐))
162 fnfvelrn 6901 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓 Fn dom 𝑓𝑦 ∈ dom 𝑓) → (𝑓𝑦) ∈ ran 𝑓)
16393, 152, 162syl2an 599 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓𝑦) ∈ ran 𝑓)
164 oveq1 7220 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (𝑓𝑦) → (𝑧(ball‘𝑁)𝑐) = ((𝑓𝑦)(ball‘𝑁)𝑐))
165164ssiun2s 4957 . . . . . . . . . . . . . . . . . . . . . 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 3911 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
168167adantlr 715 . . . . . . . . . . . . . . . . . . 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 3028 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦𝑣) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
172171ralrimiva 3105 . . . . . . . . . . . . . . 15 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑦𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
173 iunss 4954 . . . . . . . . . . . . . . 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 3940 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
176116, 175eqssd 3918 . . . . . . . . . . . 12 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) = 𝑌)
177105, 176syl5eq 2790 . . . . . . . . . . 11 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓𝑣𝑓:dom 𝑓𝑌 ∧ ∀𝑥𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌)
178 iuneq1 4920 . . . . . . . . . . . . 13 (𝑤 = ran 𝑓 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐))
179178eqeq1d 2739 . . . . . . . . . . . 12 (𝑤 = ran 𝑓 → ( 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌))
180179rspcev 3537 . . . . . . . . . . 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 1941 . . . . . . 7 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → (∃𝑓(𝑓:{𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
18567, 184mpd 15 . . . . . 6 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)
186185rexlimdvaa 3204 . . . . 5 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
18746, 186syld 47 . . . 4 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑐 ∈ ℝ+) → (∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
188187ralrimdva 3110 . . 3 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌𝑋) → (∀𝑑 ∈ ℝ+𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 𝑥𝑣 (𝑥(ball‘𝑀)𝑑) → ∀𝑐 ∈ ℝ+𝑤 ∈ (𝒫 𝑌 ∩ Fin) 𝑥𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
189 istotbnd3 35666 . . . . 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 1089   = wceq 1543  wex 1787  wcel 2110  wne 2940  wral 3061  wrex 3062  {crab 3065  cin 3865  wss 3866  c0 4237  𝒫 cpw 4513   ciun 4904   × cxp 5549  ccnv 5550  dom cdm 5551  ran crn 5552  cres 5553  cima 5554   Fn wfn 6375  wf 6376  cfv 6380  (class class class)co 7213  Fincfn 8626  cr 10728  *cxr 10866   / cdiv 11489  2c2 11885  +crp 12586  ∞Metcxmet 20348  Metcmet 20349  ballcbl 20350  TotBndctotbnd 35661
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1st 7761  df-2nd 7762  df-1o 8202  df-er 8391  df-map 8510  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-div 11490  df-2 11893  df-rp 12587  df-xneg 12704  df-xadd 12705  df-xmul 12706  df-psmet 20355  df-xmet 20356  df-met 20357  df-bl 20358  df-totbnd 35663
This theorem is referenced by:  sstotbnd  35670  sstotbnd3  35671
  Copyright terms: Public domain W3C validator