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 37098
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 24190 . . . . 5 ((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (𝑀 β†Ύ (π‘Œ Γ— π‘Œ)) ∈ (Metβ€˜π‘Œ))
31, 2eqeltrid 2829 . . . 4 ((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ 𝑁 ∈ (Metβ€˜π‘Œ))
4 istotbnd3 37095 . . . . 5 (𝑁 ∈ (TotBndβ€˜π‘Œ) ↔ (𝑁 ∈ (Metβ€˜π‘Œ) ∧ βˆ€π‘‘ ∈ ℝ+ βˆƒπ‘£ ∈ (𝒫 π‘Œ ∩ Fin)βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘)𝑑) = π‘Œ))
54baib 535 . . . 4 (𝑁 ∈ (Metβ€˜π‘Œ) β†’ (𝑁 ∈ (TotBndβ€˜π‘Œ) ↔ βˆ€π‘‘ ∈ ℝ+ βˆƒπ‘£ ∈ (𝒫 π‘Œ ∩ Fin)βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘)𝑑) = π‘Œ))
63, 5syl 17 . . 3 ((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (𝑁 ∈ (TotBndβ€˜π‘Œ) ↔ βˆ€π‘‘ ∈ ℝ+ βˆƒπ‘£ ∈ (𝒫 π‘Œ ∩ Fin)βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘)𝑑) = π‘Œ))
7 simpllr 773 . . . . . . . . . 10 ((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 π‘Œ ∩ Fin) ∧ βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘)𝑑) = π‘Œ)) β†’ π‘Œ βŠ† 𝑋)
87sspwd 4607 . . . . . . . . 9 ((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 π‘Œ ∩ Fin) ∧ βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘)𝑑) = π‘Œ)) β†’ 𝒫 π‘Œ βŠ† 𝒫 𝑋)
98ssrind 4227 . . . . . . . 8 ((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 π‘Œ ∩ Fin) ∧ βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘)𝑑) = π‘Œ)) β†’ (𝒫 π‘Œ ∩ Fin) βŠ† (𝒫 𝑋 ∩ Fin))
10 simprl 768 . . . . . . . 8 ((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 π‘Œ ∩ Fin) ∧ βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘)𝑑) = π‘Œ)) β†’ 𝑣 ∈ (𝒫 π‘Œ ∩ Fin))
119, 10sseldd 3975 . . . . . . 7 ((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 π‘Œ ∩ Fin) ∧ βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘)𝑑) = π‘Œ)) β†’ 𝑣 ∈ (𝒫 𝑋 ∩ Fin))
12 simprr 770 . . . . . . . 8 ((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 π‘Œ ∩ Fin) ∧ βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘)𝑑) = π‘Œ)) β†’ βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘)𝑑) = π‘Œ)
13 metxmet 24161 . . . . . . . . . . . . . 14 (𝑀 ∈ (Metβ€˜π‘‹) β†’ 𝑀 ∈ (∞Metβ€˜π‘‹))
1413ad4antr 729 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 π‘Œ ∩ Fin)) ∧ π‘₯ ∈ 𝑣) β†’ 𝑀 ∈ (∞Metβ€˜π‘‹))
15 elfpw 9349 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ (𝒫 π‘Œ ∩ Fin) ↔ (𝑣 βŠ† π‘Œ ∧ 𝑣 ∈ Fin))
1615simplbi 497 . . . . . . . . . . . . . . . 16 (𝑣 ∈ (𝒫 π‘Œ ∩ Fin) β†’ 𝑣 βŠ† π‘Œ)
1716adantl 481 . . . . . . . . . . . . . . 15 ((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 π‘Œ ∩ Fin)) β†’ 𝑣 βŠ† π‘Œ)
1817sselda 3974 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 π‘Œ ∩ Fin)) ∧ π‘₯ ∈ 𝑣) β†’ π‘₯ ∈ π‘Œ)
19 simp-4r 781 . . . . . . . . . . . . . . 15 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 π‘Œ ∩ Fin)) ∧ π‘₯ ∈ 𝑣) β†’ π‘Œ βŠ† 𝑋)
20 sseqin2 4207 . . . . . . . . . . . . . . 15 (π‘Œ βŠ† 𝑋 ↔ (𝑋 ∩ π‘Œ) = π‘Œ)
2119, 20sylib 217 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 π‘Œ ∩ Fin)) ∧ π‘₯ ∈ 𝑣) β†’ (𝑋 ∩ π‘Œ) = π‘Œ)
2218, 21eleqtrrd 2828 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 π‘Œ ∩ Fin)) ∧ π‘₯ ∈ 𝑣) β†’ π‘₯ ∈ (𝑋 ∩ π‘Œ))
23 simpllr 773 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 π‘Œ ∩ Fin)) ∧ π‘₯ ∈ 𝑣) β†’ 𝑑 ∈ ℝ+)
2423rpxrd 13013 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 π‘Œ ∩ Fin)) ∧ π‘₯ ∈ 𝑣) β†’ 𝑑 ∈ ℝ*)
251blres 24258 . . . . . . . . . . . . 13 ((𝑀 ∈ (∞Metβ€˜π‘‹) ∧ π‘₯ ∈ (𝑋 ∩ π‘Œ) ∧ 𝑑 ∈ ℝ*) β†’ (π‘₯(ballβ€˜π‘)𝑑) = ((π‘₯(ballβ€˜π‘€)𝑑) ∩ π‘Œ))
2614, 22, 24, 25syl3anc 1368 . . . . . . . . . . . 12 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 π‘Œ ∩ Fin)) ∧ π‘₯ ∈ 𝑣) β†’ (π‘₯(ballβ€˜π‘)𝑑) = ((π‘₯(ballβ€˜π‘€)𝑑) ∩ π‘Œ))
27 inss1 4220 . . . . . . . . . . . 12 ((π‘₯(ballβ€˜π‘€)𝑑) ∩ π‘Œ) βŠ† (π‘₯(ballβ€˜π‘€)𝑑)
2826, 27eqsstrdi 4028 . . . . . . . . . . 11 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 π‘Œ ∩ Fin)) ∧ π‘₯ ∈ 𝑣) β†’ (π‘₯(ballβ€˜π‘)𝑑) βŠ† (π‘₯(ballβ€˜π‘€)𝑑))
2928ralrimiva 3138 . . . . . . . . . 10 ((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 π‘Œ ∩ Fin)) β†’ βˆ€π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘)𝑑) βŠ† (π‘₯(ballβ€˜π‘€)𝑑))
30 ss2iun 5005 . . . . . . . . . 10 (βˆ€π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘)𝑑) βŠ† (π‘₯(ballβ€˜π‘€)𝑑) β†’ βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘)𝑑) βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)𝑑))
3129, 30syl 17 . . . . . . . . 9 ((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 π‘Œ ∩ Fin)) β†’ βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘)𝑑) βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)𝑑))
3231adantrr 714 . . . . . . . 8 ((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 π‘Œ ∩ Fin) ∧ βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘)𝑑) = π‘Œ)) β†’ βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘)𝑑) βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)𝑑))
3312, 32eqsstrrd 4013 . . . . . . 7 ((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 π‘Œ ∩ Fin) ∧ βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘)𝑑) = π‘Œ)) β†’ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)𝑑))
3411, 33jca 511 . . . . . 6 ((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 π‘Œ ∩ Fin) ∧ βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘)𝑑) = π‘Œ)) β†’ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)𝑑)))
3534ex 412 . . . . 5 (((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) β†’ ((𝑣 ∈ (𝒫 π‘Œ ∩ Fin) ∧ βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘)𝑑) = π‘Œ) β†’ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)𝑑))))
3635reximdv2 3156 . . . 4 (((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑑 ∈ ℝ+) β†’ (βˆƒπ‘£ ∈ (𝒫 π‘Œ ∩ Fin)βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘)𝑑) = π‘Œ β†’ βˆƒπ‘£ ∈ (𝒫 𝑋 ∩ Fin)π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)𝑑)))
3736ralimdva 3159 . . 3 ((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (βˆ€π‘‘ ∈ ℝ+ βˆƒπ‘£ ∈ (𝒫 π‘Œ ∩ Fin)βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘)𝑑) = π‘Œ β†’ βˆ€π‘‘ ∈ ℝ+ βˆƒπ‘£ ∈ (𝒫 𝑋 ∩ Fin)π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)𝑑)))
386, 37sylbid 239 . 2 ((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (𝑁 ∈ (TotBndβ€˜π‘Œ) β†’ βˆ€π‘‘ ∈ ℝ+ βˆƒπ‘£ ∈ (𝒫 𝑋 ∩ Fin)π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)𝑑)))
39 simpr 484 . . . . . . 7 (((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) β†’ 𝑐 ∈ ℝ+)
4039rphalfcld 13024 . . . . . 6 (((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) β†’ (𝑐 / 2) ∈ ℝ+)
41 oveq2 7409 . . . . . . . . . 10 (𝑑 = (𝑐 / 2) β†’ (π‘₯(ballβ€˜π‘€)𝑑) = (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))
4241iuneq2d 5016 . . . . . . . . 9 (𝑑 = (𝑐 / 2) β†’ βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)𝑑) = βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))
4342sseq2d 4006 . . . . . . . 8 (𝑑 = (𝑐 / 2) β†’ (π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)𝑑) ↔ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2))))
4443rexbidv 3170 . . . . . . 7 (𝑑 = (𝑐 / 2) β†’ (βˆƒπ‘£ ∈ (𝒫 𝑋 ∩ Fin)π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)𝑑) ↔ βˆƒπ‘£ ∈ (𝒫 𝑋 ∩ Fin)π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2))))
4544rspcv 3600 . . . . . 6 ((𝑐 / 2) ∈ ℝ+ β†’ (βˆ€π‘‘ ∈ ℝ+ βˆƒπ‘£ ∈ (𝒫 𝑋 ∩ Fin)π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)𝑑) β†’ βˆƒπ‘£ ∈ (𝒫 𝑋 ∩ Fin)π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2))))
4640, 45syl 17 . . . . 5 (((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) β†’ (βˆ€π‘‘ ∈ ℝ+ βˆƒπ‘£ ∈ (𝒫 𝑋 ∩ Fin)π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)𝑑) β†’ βˆƒπ‘£ ∈ (𝒫 𝑋 ∩ Fin)π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2))))
47 elfpw 9349 . . . . . . . . . . 11 (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ↔ (𝑣 βŠ† 𝑋 ∧ 𝑣 ∈ Fin))
4847simprbi 496 . . . . . . . . . 10 (𝑣 ∈ (𝒫 𝑋 ∩ Fin) β†’ 𝑣 ∈ Fin)
4948ad2antrl 725 . . . . . . . . 9 ((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) β†’ 𝑣 ∈ Fin)
50 ssrab2 4069 . . . . . . . . 9 {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} βŠ† 𝑣
51 ssfi 9168 . . . . . . . . 9 ((𝑣 ∈ Fin ∧ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} βŠ† 𝑣) β†’ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} ∈ Fin)
5249, 50, 51sylancl 585 . . . . . . . 8 ((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) β†’ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} ∈ Fin)
53 oveq1 7408 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑦 β†’ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)) = (𝑦(ballβ€˜π‘€)(𝑐 / 2)))
5453ineq1d 4203 . . . . . . . . . . . . . . 15 (π‘₯ = 𝑦 β†’ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) = ((𝑦(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ))
55 incom 4193 . . . . . . . . . . . . . . 15 ((𝑦(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) = (π‘Œ ∩ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))
5654, 55eqtrdi 2780 . . . . . . . . . . . . . 14 (π‘₯ = 𝑦 β†’ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) = (π‘Œ ∩ (𝑦(ballβ€˜π‘€)(𝑐 / 2))))
57 dfin5 3948 . . . . . . . . . . . . . 14 (π‘Œ ∩ (𝑦(ballβ€˜π‘€)(𝑐 / 2))) = {𝑧 ∈ π‘Œ ∣ 𝑧 ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2))}
5856, 57eqtrdi 2780 . . . . . . . . . . . . 13 (π‘₯ = 𝑦 β†’ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) = {𝑧 ∈ π‘Œ ∣ 𝑧 ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2))})
5958neeq1d 2992 . . . . . . . . . . . 12 (π‘₯ = 𝑦 β†’ (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… ↔ {𝑧 ∈ π‘Œ ∣ 𝑧 ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2))} β‰  βˆ…))
60 rabn0 4377 . . . . . . . . . . . 12 ({𝑧 ∈ π‘Œ ∣ 𝑧 ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2))} β‰  βˆ… ↔ βˆƒπ‘§ ∈ π‘Œ 𝑧 ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))
6159, 60bitrdi 287 . . . . . . . . . . 11 (π‘₯ = 𝑦 β†’ (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… ↔ βˆƒπ‘§ ∈ π‘Œ 𝑧 ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2))))
6261elrab 3675 . . . . . . . . . 10 (𝑦 ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} ↔ (𝑦 ∈ 𝑣 ∧ βˆƒπ‘§ ∈ π‘Œ 𝑧 ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2))))
6362simprbi 496 . . . . . . . . 9 (𝑦 ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} β†’ βˆƒπ‘§ ∈ π‘Œ 𝑧 ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))
6463rgen 3055 . . . . . . . 8 βˆ€π‘¦ ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}βˆƒπ‘§ ∈ π‘Œ 𝑧 ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2))
65 eleq1 2813 . . . . . . . . 9 (𝑧 = (π‘“β€˜π‘¦) β†’ (𝑧 ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2)) ↔ (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2))))
6665ac6sfi 9282 . . . . . . . 8 (({π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} ∈ Fin ∧ βˆ€π‘¦ ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}βˆƒπ‘§ ∈ π‘Œ 𝑧 ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2))) β†’ βˆƒπ‘“(𝑓:{π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2))))
6752, 64, 66sylancl 585 . . . . . . 7 ((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) β†’ βˆƒπ‘“(𝑓:{π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2))))
68 fdm 6716 . . . . . . . . . . . . . 14 (𝑓:{π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}βŸΆπ‘Œ β†’ dom 𝑓 = {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…})
6968ad2antrl 725 . . . . . . . . . . . . 13 ((𝑣 ∈ Fin ∧ (𝑓:{π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ dom 𝑓 = {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…})
7069, 50eqsstrdi 4028 . . . . . . . . . . . 12 ((𝑣 ∈ Fin ∧ (𝑓:{π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ dom 𝑓 βŠ† 𝑣)
71 simprl 768 . . . . . . . . . . . . 13 ((𝑣 ∈ Fin ∧ (𝑓:{π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ 𝑓:{π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}βŸΆπ‘Œ)
7269feq2d 6693 . . . . . . . . . . . . 13 ((𝑣 ∈ Fin ∧ (𝑓:{π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ (𝑓:dom π‘“βŸΆπ‘Œ ↔ 𝑓:{π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}βŸΆπ‘Œ))
7371, 72mpbird 257 . . . . . . . . . . . 12 ((𝑣 ∈ Fin ∧ (𝑓:{π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ 𝑓:dom π‘“βŸΆπ‘Œ)
74 simprr 770 . . . . . . . . . . . . . 14 ((𝑣 ∈ Fin ∧ (𝑓:{π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ βˆ€π‘¦ ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))
75 ffn 6707 . . . . . . . . . . . . . . . . . 18 (𝑓:{π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}βŸΆπ‘Œ β†’ 𝑓 Fn {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…})
76 elpreima 7049 . . . . . . . . . . . . . . . . . 18 (𝑓 Fn {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} β†’ (𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2))) ↔ (𝑦 ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} ∧ (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))))
7775, 76syl 17 . . . . . . . . . . . . . . . . 17 (𝑓:{π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}βŸΆπ‘Œ β†’ (𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2))) ↔ (𝑦 ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} ∧ (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))))
7877baibd 539 . . . . . . . . . . . . . . . 16 ((𝑓:{π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}βŸΆπ‘Œ ∧ 𝑦 ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}) β†’ (𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2))) ↔ (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2))))
7978ralbidva 3167 . . . . . . . . . . . . . . 15 (𝑓:{π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}βŸΆπ‘Œ β†’ (βˆ€π‘¦ ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2))) ↔ βˆ€π‘¦ ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2))))
8079ad2antrl 725 . . . . . . . . . . . . . 14 ((𝑣 ∈ Fin ∧ (𝑓:{π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ (βˆ€π‘¦ ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2))) ↔ βˆ€π‘¦ ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2))))
8174, 80mpbird 257 . . . . . . . . . . . . 13 ((𝑣 ∈ Fin ∧ (𝑓:{π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ βˆ€π‘¦ ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2))))
82 id 22 . . . . . . . . . . . . . . 15 (𝑦 = π‘₯ β†’ 𝑦 = π‘₯)
83 oveq1 7408 . . . . . . . . . . . . . . . 16 (𝑦 = π‘₯ β†’ (𝑦(ballβ€˜π‘€)(𝑐 / 2)) = (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))
8483imaeq2d 6049 . . . . . . . . . . . . . . 15 (𝑦 = π‘₯ β†’ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2))) = (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2))))
8582, 84eleq12d 2819 . . . . . . . . . . . . . 14 (𝑦 = π‘₯ β†’ (𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2))) ↔ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))
8685ralrab2 3686 . . . . . . . . . . . . 13 (βˆ€π‘¦ ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2))) ↔ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))
8781, 86sylib 217 . . . . . . . . . . . 12 ((𝑣 ∈ Fin ∧ (𝑓:{π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))
8870, 73, 873jca 1125 . . . . . . . . . . 11 ((𝑣 ∈ Fin ∧ (𝑓:{π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2))))))
8988ex 412 . . . . . . . . . 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 6715 . . . . . . . . . . . 12 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) β†’ ran 𝑓 βŠ† π‘Œ)
9391ffnd 6708 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) β†’ 𝑓 Fn dom 𝑓)
9449adantr 480 . . . . . . . . . . . . . . 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 9168 . . . . . . . . . . . . . . 15 ((𝑣 ∈ Fin ∧ dom 𝑓 βŠ† 𝑣) β†’ dom 𝑓 ∈ Fin)
9794, 95, 96syl2anc 583 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) β†’ dom 𝑓 ∈ Fin)
98 fnfi 9176 . . . . . . . . . . . . . 14 ((𝑓 Fn dom 𝑓 ∧ dom 𝑓 ∈ Fin) β†’ 𝑓 ∈ Fin)
9993, 97, 98syl2anc 583 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) β†’ 𝑓 ∈ Fin)
100 rnfi 9330 . . . . . . . . . . . . 13 (𝑓 ∈ Fin β†’ ran 𝑓 ∈ Fin)
10199, 100syl 17 . . . . . . . . . . . 12 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) β†’ ran 𝑓 ∈ Fin)
102 elfpw 9349 . . . . . . . . . . . 12 (ran 𝑓 ∈ (𝒫 π‘Œ ∩ Fin) ↔ (ran 𝑓 βŠ† π‘Œ ∧ ran 𝑓 ∈ Fin))
10392, 101, 102sylanbrc 582 . . . . . . . . . . 11 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) β†’ ran 𝑓 ∈ (𝒫 π‘Œ ∩ Fin))
104 oveq1 7408 . . . . . . . . . . . . 13 (π‘₯ = 𝑧 β†’ (π‘₯(ballβ€˜π‘)𝑐) = (𝑧(ballβ€˜π‘)𝑐))
105104cbviunv 5033 . . . . . . . . . . . 12 βˆͺ π‘₯ ∈ ran 𝑓(π‘₯(ballβ€˜π‘)𝑐) = βˆͺ 𝑧 ∈ ran 𝑓(𝑧(ballβ€˜π‘)𝑐)
1063ad4antr 729 . . . . . . . . . . . . . . . . 17 ((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) β†’ 𝑁 ∈ (Metβ€˜π‘Œ))
107 metxmet 24161 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (Metβ€˜π‘Œ) β†’ 𝑁 ∈ (∞Metβ€˜π‘Œ))
108106, 107syl 17 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) β†’ 𝑁 ∈ (∞Metβ€˜π‘Œ))
10992sselda 3974 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) β†’ 𝑧 ∈ π‘Œ)
110 rpxr 12979 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ ℝ+ β†’ 𝑐 ∈ ℝ*)
111110ad4antlr 730 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) β†’ 𝑐 ∈ ℝ*)
112 blssm 24245 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ (∞Metβ€˜π‘Œ) ∧ 𝑧 ∈ π‘Œ ∧ 𝑐 ∈ ℝ*) β†’ (𝑧(ballβ€˜π‘)𝑐) βŠ† π‘Œ)
113108, 109, 111, 112syl3anc 1368 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) β†’ (𝑧(ballβ€˜π‘)𝑐) βŠ† π‘Œ)
114113ralrimiva 3138 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) β†’ βˆ€π‘§ ∈ ran 𝑓(𝑧(ballβ€˜π‘)𝑐) βŠ† π‘Œ)
115 iunss 5038 . . . . . . . . . . . . . 14 (βˆͺ 𝑧 ∈ ran 𝑓(𝑧(ballβ€˜π‘)𝑐) βŠ† π‘Œ ↔ βˆ€π‘§ ∈ ran 𝑓(𝑧(ballβ€˜π‘)𝑐) βŠ† π‘Œ)
116114, 115sylibr 233 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) β†’ βˆͺ 𝑧 ∈ ran 𝑓(𝑧(ballβ€˜π‘)𝑐) βŠ† π‘Œ)
117 iunin1 5065 . . . . . . . . . . . . . . 15 βˆͺ 𝑦 ∈ 𝑣 ((𝑦(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) = (βˆͺ 𝑦 ∈ 𝑣 (𝑦(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ)
118 simplrr 775 . . . . . . . . . . . . . . . . 17 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) β†’ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))
11953cbviunv 5033 . . . . . . . . . . . . . . . . 17 βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)) = βˆͺ 𝑦 ∈ 𝑣 (𝑦(ballβ€˜π‘€)(𝑐 / 2))
120118, 119sseqtrdi 4024 . . . . . . . . . . . . . . . 16 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) β†’ π‘Œ βŠ† βˆͺ 𝑦 ∈ 𝑣 (𝑦(ballβ€˜π‘€)(𝑐 / 2)))
121 sseqin2 4207 . . . . . . . . . . . . . . . 16 (π‘Œ βŠ† βˆͺ 𝑦 ∈ 𝑣 (𝑦(ballβ€˜π‘€)(𝑐 / 2)) ↔ (βˆͺ 𝑦 ∈ 𝑣 (𝑦(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) = π‘Œ)
122120, 121sylib 217 . . . . . . . . . . . . . . 15 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) β†’ (βˆͺ 𝑦 ∈ 𝑣 (𝑦(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) = π‘Œ)
123117, 122eqtrid 2776 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) β†’ βˆͺ 𝑦 ∈ 𝑣 ((𝑦(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) = π‘Œ)
124 0ss 4388 . . . . . . . . . . . . . . . . . . 19 βˆ… βŠ† βˆͺ 𝑧 ∈ ran 𝑓(𝑧(ballβ€˜π‘)𝑐)
125 sseq1 3999 . . . . . . . . . . . . . . . . . . 19 (((𝑦(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) = βˆ… β†’ (((𝑦(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) βŠ† βˆͺ 𝑧 ∈ ran 𝑓(𝑧(ballβ€˜π‘)𝑐) ↔ βˆ… βŠ† βˆͺ 𝑧 ∈ ran 𝑓(𝑧(ballβ€˜π‘)𝑐)))
126124, 125mpbiri 258 . . . . . . . . . . . . . . . . . 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 2992 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑦 β†’ (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… ↔ ((𝑦(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…))
130 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = 𝑦 β†’ π‘₯ = 𝑦)
13153imaeq2d 6049 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = 𝑦 β†’ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2))) = (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2))))
132130, 131eleq12d 2819 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑦 β†’ (π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2))) ↔ 𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))))
133129, 132imbi12d 344 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 𝑦 β†’ ((((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ↔ (((𝑦(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ 𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2))))))
134133rspccva 3603 . . . . . . . . . . . . . . . . . . 19 ((βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ 𝑦 ∈ 𝑣) β†’ (((𝑦(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ 𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))))
135128, 134sylan 579 . . . . . . . . . . . . . . . . . 18 ((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) β†’ (((𝑦(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ 𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))))
13613ad5antr 731 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ 𝑀 ∈ (∞Metβ€˜π‘‹))
137 cnvimass 6070 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2))) βŠ† dom 𝑓
13847simplbi 497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 ∈ (𝒫 𝑋 ∩ Fin) β†’ 𝑣 βŠ† 𝑋)
139138ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) β†’ 𝑣 βŠ† 𝑋)
140139adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) β†’ 𝑣 βŠ† 𝑋)
14195, 140sstrd 3984 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) β†’ dom 𝑓 βŠ† 𝑋)
142137, 141sstrid 3985 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) β†’ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2))) βŠ† 𝑋)
143142sselda 3974 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ 𝑦 ∈ 𝑋)
144 simp-4r 781 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ 𝑐 ∈ ℝ+)
145144rpred 13012 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ 𝑐 ∈ ℝ)
146 elpreima 7049 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 Fn dom 𝑓 β†’ (𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2))) ↔ (𝑦 ∈ dom 𝑓 ∧ (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))))
147146simplbda 499 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 Fn dom 𝑓 ∧ 𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))
14893, 147sylan 579 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))
149 blhalf 24232 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ 𝑋) ∧ (𝑐 ∈ ℝ ∧ (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ (𝑦(ballβ€˜π‘€)(𝑐 / 2)) βŠ† ((π‘“β€˜π‘¦)(ballβ€˜π‘€)𝑐))
150136, 143, 145, 148, 149syl22anc 836 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ (𝑦(ballβ€˜π‘€)(𝑐 / 2)) βŠ† ((π‘“β€˜π‘¦)(ballβ€˜π‘€)𝑐))
151150ssrind 4227 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ ((𝑦(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) βŠ† (((π‘“β€˜π‘¦)(ballβ€˜π‘€)𝑐) ∩ π‘Œ))
152137sseli 3970 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2))) β†’ 𝑦 ∈ dom 𝑓)
153 ffvelcdm 7073 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓:dom π‘“βŸΆπ‘Œ ∧ 𝑦 ∈ dom 𝑓) β†’ (π‘“β€˜π‘¦) ∈ π‘Œ)
15491, 152, 153syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ (π‘“β€˜π‘¦) ∈ π‘Œ)
155 simp-5r 783 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ π‘Œ βŠ† 𝑋)
156155, 20sylib 217 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ (𝑋 ∩ π‘Œ) = π‘Œ)
157154, 156eleqtrrd 2828 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ (π‘“β€˜π‘¦) ∈ (𝑋 ∩ π‘Œ))
158110ad4antlr 730 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ 𝑐 ∈ ℝ*)
1591blres 24258 . . . . . . . . . . . . . . . . . . . . . . 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 4015 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ ((𝑦(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) βŠ† ((π‘“β€˜π‘¦)(ballβ€˜π‘)𝑐))
162 fnfvelrn 7072 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓 Fn dom 𝑓 ∧ 𝑦 ∈ dom 𝑓) β†’ (π‘“β€˜π‘¦) ∈ ran 𝑓)
16393, 152, 162syl2an 595 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ (π‘“β€˜π‘¦) ∈ ran 𝑓)
164 oveq1 7408 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (π‘“β€˜π‘¦) β†’ (𝑧(ballβ€˜π‘)𝑐) = ((π‘“β€˜π‘¦)(ballβ€˜π‘)𝑐))
165164ssiun2s 5041 . . . . . . . . . . . . . . . . . . . . . 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 3984 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ ((𝑦(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) βŠ† βˆͺ 𝑧 ∈ ran 𝑓(𝑧(ballβ€˜π‘)𝑐))
168167adantlr 712 . . . . . . . . . . . . . . . . . . 19 (((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) ∧ 𝑦 ∈ (◑𝑓 β€œ (𝑦(ballβ€˜π‘€)(𝑐 / 2)))) β†’ ((𝑦(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) βŠ† βˆͺ 𝑧 ∈ ran 𝑓(𝑧(ballβ€˜π‘)𝑐))
169168ex 412 . . . . . . . . . . . . . . . . . 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 3020 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) β†’ ((𝑦(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) βŠ† βˆͺ 𝑧 ∈ ran 𝑓(𝑧(ballβ€˜π‘)𝑐))
172171ralrimiva 3138 . . . . . . . . . . . . . . 15 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) β†’ βˆ€π‘¦ ∈ 𝑣 ((𝑦(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) βŠ† βˆͺ 𝑧 ∈ ran 𝑓(𝑧(ballβ€˜π‘)𝑐))
173 iunss 5038 . . . . . . . . . . . . . . 15 (βˆͺ 𝑦 ∈ 𝑣 ((𝑦(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) βŠ† βˆͺ 𝑧 ∈ ran 𝑓(𝑧(ballβ€˜π‘)𝑐) ↔ βˆ€π‘¦ ∈ 𝑣 ((𝑦(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) βŠ† βˆͺ 𝑧 ∈ ran 𝑓(𝑧(ballβ€˜π‘)𝑐))
174172, 173sylibr 233 . . . . . . . . . . . . . 14 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) β†’ βˆͺ 𝑦 ∈ 𝑣 ((𝑦(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) βŠ† βˆͺ 𝑧 ∈ ran 𝑓(𝑧(ballβ€˜π‘)𝑐))
175123, 174eqsstrrd 4013 . . . . . . . . . . . . 13 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) β†’ π‘Œ βŠ† βˆͺ 𝑧 ∈ ran 𝑓(𝑧(ballβ€˜π‘)𝑐))
176116, 175eqssd 3991 . . . . . . . . . . . 12 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) β†’ βˆͺ 𝑧 ∈ ran 𝑓(𝑧(ballβ€˜π‘)𝑐) = π‘Œ)
177105, 176eqtrid 2776 . . . . . . . . . . 11 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) β†’ βˆͺ π‘₯ ∈ ran 𝑓(π‘₯(ballβ€˜π‘)𝑐) = π‘Œ)
178 iuneq1 5003 . . . . . . . . . . . . 13 (𝑀 = ran 𝑓 β†’ βˆͺ π‘₯ ∈ 𝑀 (π‘₯(ballβ€˜π‘)𝑐) = βˆͺ π‘₯ ∈ ran 𝑓(π‘₯(ballβ€˜π‘)𝑐))
179178eqeq1d 2726 . . . . . . . . . . . 12 (𝑀 = ran 𝑓 β†’ (βˆͺ π‘₯ ∈ 𝑀 (π‘₯(ballβ€˜π‘)𝑐) = π‘Œ ↔ βˆͺ π‘₯ ∈ ran 𝑓(π‘₯(ballβ€˜π‘)𝑐) = π‘Œ))
180179rspcev 3604 . . . . . . . . . . 11 ((ran 𝑓 ∈ (𝒫 π‘Œ ∩ Fin) ∧ βˆͺ π‘₯ ∈ ran 𝑓(π‘₯(ballβ€˜π‘)𝑐) = π‘Œ) β†’ βˆƒπ‘€ ∈ (𝒫 π‘Œ ∩ Fin)βˆͺ π‘₯ ∈ 𝑀 (π‘₯(ballβ€˜π‘)𝑐) = π‘Œ)
181103, 177, 180syl2anc 583 . . . . . . . . . 10 (((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) ∧ (dom 𝑓 βŠ† 𝑣 ∧ 𝑓:dom π‘“βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑣 (((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ… β†’ π‘₯ ∈ (◑𝑓 β€œ (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))))) β†’ βˆƒπ‘€ ∈ (𝒫 π‘Œ ∩ Fin)βˆͺ π‘₯ ∈ 𝑀 (π‘₯(ballβ€˜π‘)𝑐) = π‘Œ)
182181ex 412 . . . . . . . . 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 1928 . . . . . . 7 ((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) β†’ (βˆƒπ‘“(𝑓:{π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…}βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ {π‘₯ ∈ 𝑣 ∣ ((π‘₯(ballβ€˜π‘€)(𝑐 / 2)) ∩ π‘Œ) β‰  βˆ…} (π‘“β€˜π‘¦) ∈ (𝑦(ballβ€˜π‘€)(𝑐 / 2))) β†’ βˆƒπ‘€ ∈ (𝒫 π‘Œ ∩ Fin)βˆͺ π‘₯ ∈ 𝑀 (π‘₯(ballβ€˜π‘)𝑐) = π‘Œ))
18567, 184mpd 15 . . . . . 6 ((((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)))) β†’ βˆƒπ‘€ ∈ (𝒫 π‘Œ ∩ Fin)βˆͺ π‘₯ ∈ 𝑀 (π‘₯(ballβ€˜π‘)𝑐) = π‘Œ)
186185rexlimdvaa 3148 . . . . 5 (((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) β†’ (βˆƒπ‘£ ∈ (𝒫 𝑋 ∩ Fin)π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)(𝑐 / 2)) β†’ βˆƒπ‘€ ∈ (𝒫 π‘Œ ∩ Fin)βˆͺ π‘₯ ∈ 𝑀 (π‘₯(ballβ€˜π‘)𝑐) = π‘Œ))
18746, 186syld 47 . . . 4 (((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑐 ∈ ℝ+) β†’ (βˆ€π‘‘ ∈ ℝ+ βˆƒπ‘£ ∈ (𝒫 𝑋 ∩ Fin)π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)𝑑) β†’ βˆƒπ‘€ ∈ (𝒫 π‘Œ ∩ Fin)βˆͺ π‘₯ ∈ 𝑀 (π‘₯(ballβ€˜π‘)𝑐) = π‘Œ))
188187ralrimdva 3146 . . 3 ((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (βˆ€π‘‘ ∈ ℝ+ βˆƒπ‘£ ∈ (𝒫 𝑋 ∩ Fin)π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)𝑑) β†’ βˆ€π‘ ∈ ℝ+ βˆƒπ‘€ ∈ (𝒫 π‘Œ ∩ Fin)βˆͺ π‘₯ ∈ 𝑀 (π‘₯(ballβ€˜π‘)𝑐) = π‘Œ))
189 istotbnd3 37095 . . . . 5 (𝑁 ∈ (TotBndβ€˜π‘Œ) ↔ (𝑁 ∈ (Metβ€˜π‘Œ) ∧ βˆ€π‘ ∈ ℝ+ βˆƒπ‘€ ∈ (𝒫 π‘Œ ∩ Fin)βˆͺ π‘₯ ∈ 𝑀 (π‘₯(ballβ€˜π‘)𝑐) = π‘Œ))
190189baib 535 . . . 4 (𝑁 ∈ (Metβ€˜π‘Œ) β†’ (𝑁 ∈ (TotBndβ€˜π‘Œ) ↔ βˆ€π‘ ∈ ℝ+ βˆƒπ‘€ ∈ (𝒫 π‘Œ ∩ Fin)βˆͺ π‘₯ ∈ 𝑀 (π‘₯(ballβ€˜π‘)𝑐) = π‘Œ))
1913, 190syl 17 . . 3 ((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (𝑁 ∈ (TotBndβ€˜π‘Œ) ↔ βˆ€π‘ ∈ ℝ+ βˆƒπ‘€ ∈ (𝒫 π‘Œ ∩ Fin)βˆͺ π‘₯ ∈ 𝑀 (π‘₯(ballβ€˜π‘)𝑐) = π‘Œ))
192188, 191sylibrd 259 . 2 ((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (βˆ€π‘‘ ∈ ℝ+ βˆƒπ‘£ ∈ (𝒫 𝑋 ∩ Fin)π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)𝑑) β†’ 𝑁 ∈ (TotBndβ€˜π‘Œ)))
19338, 192impbid 211 1 ((𝑀 ∈ (Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (𝑁 ∈ (TotBndβ€˜π‘Œ) ↔ βˆ€π‘‘ ∈ ℝ+ βˆƒπ‘£ ∈ (𝒫 𝑋 ∩ Fin)π‘Œ βŠ† βˆͺ π‘₯ ∈ 𝑣 (π‘₯(ballβ€˜π‘€)𝑑)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533  βˆƒwex 1773   ∈ wcel 2098   β‰  wne 2932  βˆ€wral 3053  βˆƒwrex 3062  {crab 3424   ∩ cin 3939   βŠ† wss 3940  βˆ…c0 4314  π’« cpw 4594  βˆͺ ciun 4987   Γ— cxp 5664  β—‘ccnv 5665  dom cdm 5666  ran crn 5667   β†Ύ cres 5668   β€œ cima 5669   Fn wfn 6528  βŸΆwf 6529  β€˜cfv 6533  (class class class)co 7401  Fincfn 8934  β„cr 11104  β„*cxr 11243   / cdiv 11867  2c2 12263  β„+crp 12970  βˆžMetcxmet 21212  Metcmet 21213  ballcbl 21214  TotBndctotbnd 37090
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11161  ax-resscn 11162  ax-1cn 11163  ax-icn 11164  ax-addcl 11165  ax-addrcl 11166  ax-mulcl 11167  ax-mulrcl 11168  ax-mulcom 11169  ax-addass 11170  ax-mulass 11171  ax-distr 11172  ax-i2m1 11173  ax-1ne0 11174  ax-1rid 11175  ax-rnegex 11176  ax-rrecex 11177  ax-cnre 11178  ax-pre-lttri 11179  ax-pre-lttrn 11180  ax-pre-ltadd 11181  ax-pre-mulgt0 11182
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-1st 7968  df-2nd 7969  df-1o 8461  df-er 8698  df-map 8817  df-en 8935  df-dom 8936  df-sdom 8937  df-fin 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-2 12271  df-rp 12971  df-xneg 13088  df-xadd 13089  df-xmul 13090  df-psmet 21219  df-xmet 21220  df-met 21221  df-bl 21222  df-totbnd 37092
This theorem is referenced by:  sstotbnd  37099  sstotbnd3  37100
  Copyright terms: Public domain W3C validator