This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sstotbnd2

Description: Condition for a subset of a metric space to be totally bounded. (Contributed by Mario Carneiro, 12-Sep-2015)

Ref Expression
Hypothesis sstotbnd.2 ⊢ 𝑁 = ( 𝑀 ↾ ( 𝑌 × 𝑌 ) )
Assertion sstotbnd2 ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑁 ∈ ( TotBnd ‘ 𝑌 ) ↔ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )

Proof

Step Hyp Ref Expression
1 sstotbnd.2 ⊢ 𝑁 = ( 𝑀 ↾ ( 𝑌 × 𝑌 ) )
2 metres2 ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑀 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( Met ‘ 𝑌 ) )
3 1 2 eqeltrid ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → 𝑁 ∈ ( Met ‘ 𝑌 ) )
4 istotbnd3 ⊢ ( 𝑁 ∈ ( TotBnd ‘ 𝑌 ) ↔ ( 𝑁 ∈ ( Met ‘ 𝑌 ) ∧ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) = 𝑌 ) )
5 4 baib ⊢ ( 𝑁 ∈ ( Met ‘ 𝑌 ) → ( 𝑁 ∈ ( TotBnd ‘ 𝑌 ) ↔ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) = 𝑌 ) )
6 3 5 syl ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑁 ∈ ( TotBnd ‘ 𝑌 ) ↔ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) = 𝑌 ) )
7 simpllr ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) = 𝑌 ) ) → 𝑌 ⊆ 𝑋 )
8 7 sspwd ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) = 𝑌 ) ) → 𝒫 𝑌 ⊆ 𝒫 𝑋 )
9 8 ssrind ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) = 𝑌 ) ) → ( 𝒫 𝑌 ∩ Fin ) ⊆ ( 𝒫 𝑋 ∩ Fin ) )
10 simprl ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) = 𝑌 ) ) → 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) )
11 9 10 sseldd ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) = 𝑌 ) ) → 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) )
12 simprr ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) = 𝑌 ) ) → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) = 𝑌 )
13 metxmet ⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
14 13 ad4antr ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
15 elfpw ⊢ ( 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ↔ ( 𝑣 ⊆ 𝑌 ∧ 𝑣 ∈ Fin ) )
16 15 simplbi ⊢ ( 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) → 𝑣 ⊆ 𝑌 )
17 16 adantl ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ) → 𝑣 ⊆ 𝑌 )
18 17 sselda ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → 𝑥 ∈ 𝑌 )
19 simp-4r ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → 𝑌 ⊆ 𝑋 )
20 sseqin2 ⊢ ( 𝑌 ⊆ 𝑋 ↔ ( 𝑋 ∩ 𝑌 ) = 𝑌 )
21 19 20 sylib ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → ( 𝑋 ∩ 𝑌 ) = 𝑌 )
22 18 21 eleqtrrd ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) )
23 simpllr ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → 𝑑 ∈ ℝ+ )
24 23 rpxrd ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → 𝑑 ∈ ℝ* )
25 1 blres ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) ∧ 𝑑 ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) = ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) )
26 14 22 24 25 syl3anc ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) = ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) )
27 inss1 ⊢ ( ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∩ 𝑌 ) ⊆ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 )
28 26 27 eqsstrdi ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) ⊆ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
29 28 ralrimiva ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ) → ∀ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) ⊆ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
30 ss2iun ⊢ ( ∀ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) ⊆ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
31 29 30 syl ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ) → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
32 31 adantrr ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) = 𝑌 ) ) → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
33 12 32 eqsstrrd ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) = 𝑌 ) ) → 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
34 11 33 jca ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) = 𝑌 ) ) → ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
35 34 ex ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) → ( ( 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) = 𝑌 ) → ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) )
36 35 reximdv2 ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) → ( ∃ 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) = 𝑌 → ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
37 36 ralimdva ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑌 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑑 ) = 𝑌 → ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
38 6 37 sylbid ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑁 ∈ ( TotBnd ‘ 𝑌 ) → ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
39 simpr ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) → 𝑐 ∈ ℝ+ )
40 39 rphalfcld ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) → ( 𝑐 / 2 ) ∈ ℝ+ )
41 oveq2 ⊢ ( 𝑑 = ( 𝑐 / 2 ) → ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) )
42 41 iuneq2d ⊢ ( 𝑑 = ( 𝑐 / 2 ) → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) )
43 42 sseq2d ⊢ ( 𝑑 = ( 𝑐 / 2 ) → ( 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ↔ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) )
44 43 rexbidv ⊢ ( 𝑑 = ( 𝑐 / 2 ) → ( ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ↔ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) )
45 44 rspcv ⊢ ( ( 𝑐 / 2 ) ∈ ℝ+ → ( ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) → ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) )
46 40 45 syl ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) → ( ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) → ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) )
47 elfpw ⊢ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ↔ ( 𝑣 ⊆ 𝑋 ∧ 𝑣 ∈ Fin ) )
48 47 simprbi ⊢ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑣 ∈ Fin )
49 48 ad2antrl ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → 𝑣 ∈ Fin )
50 ssrab2 ⊢ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⊆ 𝑣
51 ssfi ⊢ ( ( 𝑣 ∈ Fin ∧ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⊆ 𝑣 ) → { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin )
52 49 50 51 sylancl ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin )
53 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) = ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) )
54 53 ineq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) = ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) )
55 incom ⊢ ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) = ( 𝑌 ∩ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) )
56 54 55 eqtrdi ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) = ( 𝑌 ∩ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) )
57 dfin5 ⊢ ( 𝑌 ∩ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) = { 𝑧 ∈ 𝑌 ∣ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) }
58 56 57 eqtrdi ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) = { 𝑧 ∈ 𝑌 ∣ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) } )
59 58 neeq1d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ ↔ { 𝑧 ∈ 𝑌 ∣ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) } ≠ ∅ ) )
60 rabn0 ⊢ ( { 𝑧 ∈ 𝑌 ∣ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) } ≠ ∅ ↔ ∃ 𝑧 ∈ 𝑌 𝑧 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) )
61 59 60 bitrdi ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ ↔ ∃ 𝑧 ∈ 𝑌 𝑧 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) )
62 61 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ↔ ( 𝑦 ∈ 𝑣 ∧ ∃ 𝑧 ∈ 𝑌 𝑧 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) )
63 62 simprbi ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } → ∃ 𝑧 ∈ 𝑌 𝑧 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) )
64 63 rgen ⊢ ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ∃ 𝑧 ∈ 𝑌 𝑧 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) )
65 eleq1 ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑦 ) → ( 𝑧 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ↔ ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) )
66 65 ac6sfi ⊢ ( ( { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ∈ Fin ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ∃ 𝑧 ∈ 𝑌 𝑧 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) → ∃ 𝑓 ( 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) )
67 52 64 66 sylancl ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ∃ 𝑓 ( 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) )
68 fdm ⊢ ( 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 → dom 𝑓 = { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } )
69 68 ad2antrl ⊢ ( ( 𝑣 ∈ Fin ∧ ( 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → dom 𝑓 = { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } )
70 69 50 eqsstrdi ⊢ ( ( 𝑣 ∈ Fin ∧ ( 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → dom 𝑓 ⊆ 𝑣 )
71 simprl ⊢ ( ( 𝑣 ∈ Fin ∧ ( 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 )
72 69 feq2d ⊢ ( ( 𝑣 ∈ Fin ∧ ( 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ( 𝑓 : dom 𝑓 ⟶ 𝑌 ↔ 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 ) )
73 71 72 mpbird ⊢ ( ( 𝑣 ∈ Fin ∧ ( 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → 𝑓 : dom 𝑓 ⟶ 𝑌 )
74 simprr ⊢ ( ( 𝑣 ∈ Fin ∧ ( 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) )
75 ffn ⊢ ( 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 → 𝑓 Fn { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } )
76 elpreima ⊢ ( 𝑓 Fn { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } → ( 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ↔ ( 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ∧ ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) )
77 75 76 syl ⊢ ( 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 → ( 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ↔ ( 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ∧ ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) )
78 77 baibd ⊢ ( ( 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 ∧ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ) → ( 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ↔ ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) )
79 78 ralbidva ⊢ ( 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 → ( ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ↔ ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) )
80 79 ad2antrl ⊢ ( ( 𝑣 ∈ Fin ∧ ( 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ( ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ↔ ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) )
81 74 80 mpbird ⊢ ( ( 𝑣 ∈ Fin ∧ ( 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) )
82 id ⊢ ( 𝑦 = 𝑥 → 𝑦 = 𝑥 )
83 oveq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) = ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) )
84 83 imaeq2d ⊢ ( 𝑦 = 𝑥 → ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) = ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) )
85 82 84 eleq12d ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ↔ 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) )
86 85 ralrab2 ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ↔ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) )
87 81 86 sylib ⊢ ( ( 𝑣 ∈ Fin ∧ ( 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) )
88 70 73 87 3jca ⊢ ( ( 𝑣 ∈ Fin ∧ ( 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) )
89 88 ex ⊢ ( 𝑣 ∈ Fin → ( ( 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) → ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) )
90 49 89 syl ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ( ( 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) → ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) )
91 simpr2 ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → 𝑓 : dom 𝑓 ⟶ 𝑌 )
92 91 frnd ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → ran 𝑓 ⊆ 𝑌 )
93 91 ffnd ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → 𝑓 Fn dom 𝑓 )
94 49 adantr ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → 𝑣 ∈ Fin )
95 simpr1 ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → dom 𝑓 ⊆ 𝑣 )
96 ssfi ⊢ ( ( 𝑣 ∈ Fin ∧ dom 𝑓 ⊆ 𝑣 ) → dom 𝑓 ∈ Fin )
97 94 95 96 syl2anc ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → dom 𝑓 ∈ Fin )
98 fnfi ⊢ ( ( 𝑓 Fn dom 𝑓 ∧ dom 𝑓 ∈ Fin ) → 𝑓 ∈ Fin )
99 93 97 98 syl2anc ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → 𝑓 ∈ Fin )
100 rnfi ⊢ ( 𝑓 ∈ Fin → ran 𝑓 ∈ Fin )
101 99 100 syl ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → ran 𝑓 ∈ Fin )
102 elfpw ⊢ ( ran 𝑓 ∈ ( 𝒫 𝑌 ∩ Fin ) ↔ ( ran 𝑓 ⊆ 𝑌 ∧ ran 𝑓 ∈ Fin ) )
103 92 101 102 sylanbrc ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → ran 𝑓 ∈ ( 𝒫 𝑌 ∩ Fin ) )
104 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ( ball ‘ 𝑁 ) 𝑐 ) = ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) )
105 104 cbviunv ⊢ ∪ 𝑥 ∈ ran 𝑓 ( 𝑥 ( ball ‘ 𝑁 ) 𝑐 ) = ∪ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 )
106 3 ad4antr ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) → 𝑁 ∈ ( Met ‘ 𝑌 ) )
107 metxmet ⊢ ( 𝑁 ∈ ( Met ‘ 𝑌 ) → 𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
108 106 107 syl ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) → 𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
109 92 sselda ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) → 𝑧 ∈ 𝑌 )
110 rpxr ⊢ ( 𝑐 ∈ ℝ+ → 𝑐 ∈ ℝ* )
111 110 ad4antlr ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) → 𝑐 ∈ ℝ* )
112 blssm ⊢ ( ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑧 ∈ 𝑌 ∧ 𝑐 ∈ ℝ* ) → ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) ⊆ 𝑌 )
113 108 109 111 112 syl3anc ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) → ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) ⊆ 𝑌 )
114 113 ralrimiva ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → ∀ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) ⊆ 𝑌 )
115 iunss ⊢ ( ∪ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) ⊆ 𝑌 ↔ ∀ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) ⊆ 𝑌 )
116 114 115 sylibr ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → ∪ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) ⊆ 𝑌 )
117 iunin1 ⊢ ∪ 𝑦 ∈ 𝑣 ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) = ( ∪ 𝑦 ∈ 𝑣 ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 )
118 simplrr ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) )
119 53 cbviunv ⊢ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) = ∪ 𝑦 ∈ 𝑣 ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) )
120 118 119 sseqtrdi ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → 𝑌 ⊆ ∪ 𝑦 ∈ 𝑣 ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) )
121 sseqin2 ⊢ ( 𝑌 ⊆ ∪ 𝑦 ∈ 𝑣 ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ↔ ( ∪ 𝑦 ∈ 𝑣 ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) = 𝑌 )
122 120 121 sylib ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → ( ∪ 𝑦 ∈ 𝑣 ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) = 𝑌 )
123 117 122 eqtrid ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → ∪ 𝑦 ∈ 𝑣 ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) = 𝑌 )
124 0ss ⊢ ∅ ⊆ ∪ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 )
125 sseq1 ⊢ ( ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) = ∅ → ( ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ⊆ ∪ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) ↔ ∅ ⊆ ∪ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) ) )
126 124 125 mpbiri ⊢ ( ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) = ∅ → ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ⊆ ∪ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) )
127 126 a1i ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ 𝑣 ) → ( ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) = ∅ → ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ⊆ ∪ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) ) )
128 simpr3 ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) )
129 54 neeq1d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ ↔ ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ ) )
130 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
131 53 imaeq2d ⊢ ( 𝑥 = 𝑦 → ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) = ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) )
132 130 131 eleq12d ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ↔ 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) )
133 129 132 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ↔ ( ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) )
134 133 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ 𝑦 ∈ 𝑣 ) → ( ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) )
135 128 134 sylan ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ 𝑣 ) → ( ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) )
136 13 ad5antr ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
137 cnvimass ⊢ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ⊆ dom 𝑓
138 47 simplbi ⊢ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑣 ⊆ 𝑋 )
139 138 ad2antrl ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → 𝑣 ⊆ 𝑋 )
140 139 adantr ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → 𝑣 ⊆ 𝑋 )
141 95 140 sstrd ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → dom 𝑓 ⊆ 𝑋 )
142 137 141 sstrid ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ⊆ 𝑋 )
143 142 sselda ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → 𝑦 ∈ 𝑋 )
144 simp-4r ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → 𝑐 ∈ ℝ+ )
145 144 rpred ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → 𝑐 ∈ ℝ )
146 elpreima ⊢ ( 𝑓 Fn dom 𝑓 → ( 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ↔ ( 𝑦 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) )
147 146 simplbda ⊢ ( ( 𝑓 Fn dom 𝑓 ∧ 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) )
148 93 147 sylan ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) )
149 blhalf ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑐 ∈ ℝ ∧ ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ⊆ ( ( 𝑓 ‘ 𝑦 ) ( ball ‘ 𝑀 ) 𝑐 ) )
150 136 143 145 148 149 syl22anc ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ⊆ ( ( 𝑓 ‘ 𝑦 ) ( ball ‘ 𝑀 ) 𝑐 ) )
151 150 ssrind ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ⊆ ( ( ( 𝑓 ‘ 𝑦 ) ( ball ‘ 𝑀 ) 𝑐 ) ∩ 𝑌 ) )
152 137 sseli ⊢ ( 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) → 𝑦 ∈ dom 𝑓 )
153 ffvelcdm ⊢ ( ( 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ 𝑦 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑦 ) ∈ 𝑌 )
154 91 152 153 syl2an ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ( 𝑓 ‘ 𝑦 ) ∈ 𝑌 )
155 simp-5r ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → 𝑌 ⊆ 𝑋 )
156 155 20 sylib ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ( 𝑋 ∩ 𝑌 ) = 𝑌 )
157 154 156 eleqtrrd ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑋 ∩ 𝑌 ) )
158 110 ad4antlr ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → 𝑐 ∈ ℝ* )
159 1 blres ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑋 ∩ 𝑌 ) ∧ 𝑐 ∈ ℝ* ) → ( ( 𝑓 ‘ 𝑦 ) ( ball ‘ 𝑁 ) 𝑐 ) = ( ( ( 𝑓 ‘ 𝑦 ) ( ball ‘ 𝑀 ) 𝑐 ) ∩ 𝑌 ) )
160 136 157 158 159 syl3anc ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ( ( 𝑓 ‘ 𝑦 ) ( ball ‘ 𝑁 ) 𝑐 ) = ( ( ( 𝑓 ‘ 𝑦 ) ( ball ‘ 𝑀 ) 𝑐 ) ∩ 𝑌 ) )
161 151 160 sseqtrrd ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ⊆ ( ( 𝑓 ‘ 𝑦 ) ( ball ‘ 𝑁 ) 𝑐 ) )
162 fnfvelrn ⊢ ( ( 𝑓 Fn dom 𝑓 ∧ 𝑦 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑦 ) ∈ ran 𝑓 )
163 93 152 162 syl2an ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ( 𝑓 ‘ 𝑦 ) ∈ ran 𝑓 )
164 oveq1 ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑦 ) → ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) = ( ( 𝑓 ‘ 𝑦 ) ( ball ‘ 𝑁 ) 𝑐 ) )
165 164 ssiun2s ⊢ ( ( 𝑓 ‘ 𝑦 ) ∈ ran 𝑓 → ( ( 𝑓 ‘ 𝑦 ) ( ball ‘ 𝑁 ) 𝑐 ) ⊆ ∪ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) )
166 163 165 syl ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ( ( 𝑓 ‘ 𝑦 ) ( ball ‘ 𝑁 ) 𝑐 ) ⊆ ∪ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) )
167 161 166 sstrd ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ⊆ ∪ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) )
168 167 adantlr ⊢ ( ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ 𝑣 ) ∧ 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ⊆ ∪ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) )
169 168 ex ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ 𝑣 ) → ( 𝑦 ∈ ( ◡ 𝑓 “ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) → ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ⊆ ∪ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) ) )
170 135 169 syld ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ 𝑣 ) → ( ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ⊆ ∪ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) ) )
171 127 170 pm2.61dne ⊢ ( ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) ∧ 𝑦 ∈ 𝑣 ) → ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ⊆ ∪ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) )
172 171 ralrimiva ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → ∀ 𝑦 ∈ 𝑣 ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ⊆ ∪ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) )
173 iunss ⊢ ( ∪ 𝑦 ∈ 𝑣 ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ⊆ ∪ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) ↔ ∀ 𝑦 ∈ 𝑣 ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ⊆ ∪ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) )
174 172 173 sylibr ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → ∪ 𝑦 ∈ 𝑣 ( ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ⊆ ∪ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) )
175 123 174 eqsstrrd ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → 𝑌 ⊆ ∪ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) )
176 116 175 eqssd ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → ∪ 𝑧 ∈ ran 𝑓 ( 𝑧 ( ball ‘ 𝑁 ) 𝑐 ) = 𝑌 )
177 105 176 eqtrid ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → ∪ 𝑥 ∈ ran 𝑓 ( 𝑥 ( ball ‘ 𝑁 ) 𝑐 ) = 𝑌 )
178 iuneq1 ⊢ ( 𝑤 = ran 𝑓 → ∪ 𝑥 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝑁 ) 𝑐 ) = ∪ 𝑥 ∈ ran 𝑓 ( 𝑥 ( ball ‘ 𝑁 ) 𝑐 ) )
179 178 eqeq1d ⊢ ( 𝑤 = ran 𝑓 → ( ∪ 𝑥 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝑁 ) 𝑐 ) = 𝑌 ↔ ∪ 𝑥 ∈ ran 𝑓 ( 𝑥 ( ball ‘ 𝑁 ) 𝑐 ) = 𝑌 ) )
180 179 rspcev ⊢ ( ( ran 𝑓 ∈ ( 𝒫 𝑌 ∩ Fin ) ∧ ∪ 𝑥 ∈ ran 𝑓 ( 𝑥 ( ball ‘ 𝑁 ) 𝑐 ) = 𝑌 ) → ∃ 𝑤 ∈ ( 𝒫 𝑌 ∩ Fin ) ∪ 𝑥 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝑁 ) 𝑐 ) = 𝑌 )
181 103 177 180 syl2anc ⊢ ( ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ∧ ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) ) → ∃ 𝑤 ∈ ( 𝒫 𝑌 ∩ Fin ) ∪ 𝑥 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝑁 ) 𝑐 ) = 𝑌 )
182 181 ex ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ( ( dom 𝑓 ⊆ 𝑣 ∧ 𝑓 : dom 𝑓 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑣 ( ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ → 𝑥 ∈ ( ◡ 𝑓 “ ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) ) → ∃ 𝑤 ∈ ( 𝒫 𝑌 ∩ Fin ) ∪ 𝑥 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝑁 ) 𝑐 ) = 𝑌 ) )
183 90 182 syld ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ( ( 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) → ∃ 𝑤 ∈ ( 𝒫 𝑌 ∩ Fin ) ∪ 𝑥 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝑁 ) 𝑐 ) = 𝑌 ) )
184 183 exlimdv ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ( ∃ 𝑓 ( 𝑓 : { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ⟶ 𝑌 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝑣 ∣ ( ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ∩ 𝑌 ) ≠ ∅ } ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) → ∃ 𝑤 ∈ ( 𝒫 𝑌 ∩ Fin ) ∪ 𝑥 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝑁 ) 𝑐 ) = 𝑌 ) )
185 67 184 mpd ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) ) ) → ∃ 𝑤 ∈ ( 𝒫 𝑌 ∩ Fin ) ∪ 𝑥 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝑁 ) 𝑐 ) = 𝑌 )
186 185 rexlimdvaa ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) → ( ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑐 / 2 ) ) → ∃ 𝑤 ∈ ( 𝒫 𝑌 ∩ Fin ) ∪ 𝑥 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝑁 ) 𝑐 ) = 𝑌 ) )
187 46 186 syld ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ 𝑐 ∈ ℝ+ ) → ( ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) → ∃ 𝑤 ∈ ( 𝒫 𝑌 ∩ Fin ) ∪ 𝑥 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝑁 ) 𝑐 ) = 𝑌 ) )
188 187 ralrimdva ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) → ∀ 𝑐 ∈ ℝ+ ∃ 𝑤 ∈ ( 𝒫 𝑌 ∩ Fin ) ∪ 𝑥 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝑁 ) 𝑐 ) = 𝑌 ) )
189 istotbnd3 ⊢ ( 𝑁 ∈ ( TotBnd ‘ 𝑌 ) ↔ ( 𝑁 ∈ ( Met ‘ 𝑌 ) ∧ ∀ 𝑐 ∈ ℝ+ ∃ 𝑤 ∈ ( 𝒫 𝑌 ∩ Fin ) ∪ 𝑥 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝑁 ) 𝑐 ) = 𝑌 ) )
190 189 baib ⊢ ( 𝑁 ∈ ( Met ‘ 𝑌 ) → ( 𝑁 ∈ ( TotBnd ‘ 𝑌 ) ↔ ∀ 𝑐 ∈ ℝ+ ∃ 𝑤 ∈ ( 𝒫 𝑌 ∩ Fin ) ∪ 𝑥 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝑁 ) 𝑐 ) = 𝑌 ) )
191 3 190 syl ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑁 ∈ ( TotBnd ‘ 𝑌 ) ↔ ∀ 𝑐 ∈ ℝ+ ∃ 𝑤 ∈ ( 𝒫 𝑌 ∩ Fin ) ∪ 𝑥 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝑁 ) 𝑐 ) = 𝑌 ) )
192 188 191 sylibrd ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) → 𝑁 ∈ ( TotBnd ‘ 𝑌 ) ) )
193 38 192 impbid ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑁 ∈ ( TotBnd ‘ 𝑌 ) ↔ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )