sstotbnd2 - Mathbox for Jeff Madsen

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

Theorem sstotbnd2 33905

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.

Step	Hyp	Ref	Expression
1		sstotbnd.2	. . . . 5 ⊢ 𝑁 = (𝑀 ↾ (𝑌 × 𝑌))
2		metres2 22388	. . . . 5 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑀 ↾ (𝑌 × 𝑌)) ∈ (Met‘𝑌))
3	1, 2	syl5eqel 2854	. . . 4 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → 𝑁 ∈ (Met‘𝑌))
4		istotbnd3 33902	. . . . 5 ⊢ (𝑁 ∈ (TotBnd‘𝑌) ↔ (𝑁 ∈ (Met‘𝑌) ∧ ∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌))
5	4	baib 525	. . . 4 ⊢ (𝑁 ∈ (Met‘𝑌) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌))
6	3, 5	syl 17	. . 3 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌))
7		simpllr 760	. . . . . . . . . 10 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑌 ⊆ 𝑋)
8		sspwb 5045	. . . . . . . . . 10 ⊢ (𝑌 ⊆ 𝑋 ↔ 𝒫 𝑌 ⊆ 𝒫 𝑋)
9	7, 8	sylib 208	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝒫 𝑌 ⊆ 𝒫 𝑋)
10	9	ssrind 3988	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → (𝒫 𝑌 ∩ Fin) ⊆ (𝒫 𝑋 ∩ Fin))
11		simprl 754	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑣 ∈ (𝒫 𝑌 ∩ Fin))
12	10, 11	sseldd 3753	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑣 ∈ (𝒫 𝑋 ∩ Fin))
13		simprr 756	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)
14		metxmet 22359	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀 ∈ (∞Met‘𝑋))
15	14	ad4antr 712	. . . . . . . . . . . . 13 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑀 ∈ (∞Met‘𝑋))
16		elfpw 8424	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ↔ (𝑣 ⊆ 𝑌 ∧ 𝑣 ∈ Fin))
17	16	simplbi 485	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) → 𝑣 ⊆ 𝑌)
18	17	adantl 467	. . . . . . . . . . . . . . 15 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) → 𝑣 ⊆ 𝑌)
19	18	sselda 3752	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ 𝑌)
20		simp-4r 770	. . . . . . . . . . . . . . 15 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑌 ⊆ 𝑋)
21		sseqin2 3968	. . . . . . . . . . . . . . 15 ⊢ (𝑌 ⊆ 𝑋 ↔ (𝑋 ∩ 𝑌) = 𝑌)
22	20, 21	sylib 208	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → (𝑋 ∩ 𝑌) = 𝑌)
23	19, 22	eleqtrrd 2853	. . . . . . . . . . . . 13 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ (𝑋 ∩ 𝑌))
24		simpllr 760	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑑 ∈ ℝ⁺)
25	24	rpxrd 12076	. . . . . . . . . . . . 13 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑑 ∈ ℝ^*)
26	1	blres 22456	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ (𝑋 ∩ 𝑌) ∧ 𝑑 ∈ ℝ^*) → (𝑥(ball‘𝑁)𝑑) = ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌))
27	15, 23, 25, 26	syl3anc 1476	. . . . . . . . . . . 12 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → (𝑥(ball‘𝑁)𝑑) = ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌))
28		inss1 3981	. . . . . . . . . . . 12 ⊢ ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌) ⊆ (𝑥(ball‘𝑀)𝑑)
29	27, 28	syl6eqss 3804	. . . . . . . . . . 11 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑))
30	29	ralrimiva 3115	. . . . . . . . . 10 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) → ∀𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑))
31		ss2iun 4670	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))
32	30, 31	syl 17	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))
33	32	adantrr 696	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))
34	13, 33	eqsstr3d 3789	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))
35	12, 34	jca 501	. . . . . 6 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)))
36	35	ex 397	. . . . 5 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) → ((𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌) → (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))))
37	36	reximdv2 3162	. . . 4 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) → (∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌 → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)))
38	37	ralimdva 3111	. . 3 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌 → ∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)))
39	6, 38	sylbid 230	. 2 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) → ∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)))
40		simpr 471	. . . . . . 7 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) → 𝑐 ∈ ℝ⁺)
41	40	rphalfcld 12087	. . . . . 6 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) → (𝑐 / 2) ∈ ℝ⁺)
42		oveq2 6801	. . . . . . . . . 10 ⊢ (𝑑 = (𝑐 / 2) → (𝑥(ball‘𝑀)𝑑) = (𝑥(ball‘𝑀)(𝑐 / 2)))
43	42	iuneq2d 4681	. . . . . . . . 9 ⊢ (𝑑 = (𝑐 / 2) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))
44	43	sseq2d 3782	. . . . . . . 8 ⊢ (𝑑 = (𝑐 / 2) → (𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) ↔ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
45	44	rexbidv 3200	. . . . . . 7 ⊢ (𝑑 = (𝑐 / 2) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) ↔ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
46	45	rspcv 3456	. . . . . 6 ⊢ ((𝑐 / 2) ∈ ℝ⁺ → (∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
47	41, 46	syl 17	. . . . 5 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) → (∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
48		elfpw 8424	. . . . . . . . . . 11 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ↔ (𝑣 ⊆ 𝑋 ∧ 𝑣 ∈ Fin))
49	48	simprbi 484	. . . . . . . . . 10 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ∈ Fin)
50	49	ad2antrl 707	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → 𝑣 ∈ Fin)
51		ssrab2 3836	. . . . . . . . 9 ⊢ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ⊆ 𝑣
52		ssfi 8336	. . . . . . . . 9 ⊢ ((𝑣 ∈ Fin ∧ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ⊆ 𝑣) → {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin)
53	50, 51, 52	sylancl 574	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin)
54		oveq1 6800	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑥(ball‘𝑀)(𝑐 / 2)) = (𝑦(ball‘𝑀)(𝑐 / 2)))
55	54	ineq1d 3964	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌))
56		incom 3956	. . . . . . . . . . . . . . 15 ⊢ ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2)))
57	55, 56	syl6eq 2821	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2))))
58		dfin5 3731	. . . . . . . . . . . . . 14 ⊢ (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2))) = {𝑧 ∈ 𝑌 ∣ 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))}
59	57, 58	syl6eq 2821	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = {𝑧 ∈ 𝑌 ∣ 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))})
60	59	neeq1d 3002	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ {𝑧 ∈ 𝑌 ∣ 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))} ≠ ∅))
61		rabn0 4104	. . . . . . . . . . . 12 ⊢ ({𝑧 ∈ 𝑌 ∣ 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))} ≠ ∅ ↔ ∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
62	60, 61	syl6bb 276	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ ∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
63	62	elrab 3515	. . . . . . . . . 10 ⊢ (𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ↔ (𝑦 ∈ 𝑣 ∧ ∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
64	63	simprbi 484	. . . . . . . . 9 ⊢ (𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} → ∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
65	64	rgen 3071	. . . . . . . 8 ⊢ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))
66		eleq1 2838	. . . . . . . . 9 ⊢ (𝑧 = (𝑓‘𝑦) → (𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)) ↔ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
67	66	ac6sfi 8360	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → ∃𝑓(𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
68	53, 65, 67	sylancl 574	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ∃𝑓(𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
69		fdm 6191	. . . . . . . . . . . . . 14 ⊢ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → dom 𝑓 = {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅})
70	69	ad2antrl 707	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → dom 𝑓 = {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅})
71	70, 51	syl6eqss 3804	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → dom 𝑓 ⊆ 𝑣)
72		simprl 754	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌)
73	70	feq2d 6171	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓:dom 𝑓⟶𝑌 ↔ 𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌))
74	72, 73	mpbird 247	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑓:dom 𝑓⟶𝑌)
75		simprr 756	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
76		ffn 6185	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → 𝑓 Fn {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅})
77		elpreima 6480	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 Fn {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} → (𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∧ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))))
78	76, 77	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → (𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∧ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))))
79	78	baibd 529	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ 𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}) → (𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
80	79	ralbidva 3134	. . . . . . . . . . . . . . 15 ⊢ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → (∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
81	80	ad2antrl 707	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
82	75, 81	mpbird 247	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))
83		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → 𝑦 = 𝑥)
84		oveq1 6800	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → (𝑦(ball‘𝑀)(𝑐 / 2)) = (𝑥(ball‘𝑀)(𝑐 / 2)))
85	84	imaeq2d 5607	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) = (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))
86	83, 85	eleq12d 2844	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))
87	86	ralrab2 3524	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))
88	82, 87	sylib 208	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))
89	71, 74, 88	3jca 1122	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))))
90	89	ex 397	. . . . . . . . . 10 ⊢ (𝑣 ∈ Fin → ((𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))))
91	50, 90	syl 17	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ((𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))))
92		simpr2 1235	. . . . . . . . . . . . 13 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓:dom 𝑓⟶𝑌)
93		frn 6193	. . . . . . . . . . . . 13 ⊢ (𝑓:dom 𝑓⟶𝑌 → ran 𝑓 ⊆ 𝑌)
94	92, 93	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓 ⊆ 𝑌)
95		ffn 6185	. . . . . . . . . . . . . . 15 ⊢ (𝑓:dom 𝑓⟶𝑌 → 𝑓 Fn dom 𝑓)
96	92, 95	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓 Fn dom 𝑓)
97	50	adantr 466	. . . . . . . . . . . . . . 15 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑣 ∈ Fin)
98		simpr1 1233	. . . . . . . . . . . . . . 15 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓 ⊆ 𝑣)
99		ssfi 8336	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∈ Fin ∧ dom 𝑓 ⊆ 𝑣) → dom 𝑓 ∈ Fin)
100	97, 98, 99	syl2anc 573	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓 ∈ Fin)
101		fnfi 8394	. . . . . . . . . . . . . 14 ⊢ ((𝑓 Fn dom 𝑓 ∧ dom 𝑓 ∈ Fin) → 𝑓 ∈ Fin)
102	96, 100, 101	syl2anc 573	. . . . . . . . . . . . 13 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓 ∈ Fin)
103		rnfi 8405	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ Fin → ran 𝑓 ∈ Fin)
104	102, 103	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓 ∈ Fin)
105		elfpw 8424	. . . . . . . . . . . 12 ⊢ (ran 𝑓 ∈ (𝒫 𝑌 ∩ Fin) ↔ (ran 𝑓 ⊆ 𝑌 ∧ ran 𝑓 ∈ Fin))
106	94, 104, 105	sylanbrc 572	. . . . . . . . . . 11 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓 ∈ (𝒫 𝑌 ∩ Fin))
107		oveq1 6800	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑥(ball‘𝑁)𝑐) = (𝑧(ball‘𝑁)𝑐))
108	107	cbviunv 4693	. . . . . . . . . . . 12 ⊢ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)
109	3	ad4antr 712	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑁 ∈ (Met‘𝑌))
110		metxmet 22359	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (Met‘𝑌) → 𝑁 ∈ (∞Met‘𝑌))
111	109, 110	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑁 ∈ (∞Met‘𝑌))
112	94	sselda 3752	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ 𝑌)
113		rpxr 12043	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ ℝ⁺ → 𝑐 ∈ ℝ^*)
114	113	ad4antlr 714	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑐 ∈ ℝ^*)
115		blssm 22443	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝑧 ∈ 𝑌 ∧ 𝑐 ∈ ℝ^*) → (𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
116	111, 112, 114, 115	syl3anc 1476	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → (𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
117	116	ralrimiva 3115	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
118		iunss 4695	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌 ↔ ∀𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
119	117, 118	sylibr 224	. . . . . . . . . . . . 13 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
120		iunin1 4719	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = (∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌)
121		simplrr 763	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))
122	54	cbviunv 4693	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)) = ∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2))
123	121, 122	syl6sseq 3800	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 ⊆ ∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)))
124		sseqin2 3968	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 ⊆ ∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ↔ (∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌)
125	123, 124	sylib 208	. . . . . . . . . . . . . . 15 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → (∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌)
126	120, 125	syl5eq 2817	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌)
127		0ss 4116	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)
128		sseq1 3775	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ∅ → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ↔ ∅ ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)))
129	127, 128	mpbiri 248	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ∅ → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
130	129	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ∅ → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)))
131		simpr3 1237	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))
132	55	neeq1d 3002	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅))
133		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
134	54	imaeq2d 5607	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))) = (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))
135	133, 134	eleq12d 2844	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))) ↔ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))))
136	132, 135	imbi12d 333	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → ((((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))) ↔ (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))))
137	136	rspccva 3459	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ 𝑦 ∈ 𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))))
138	131, 137	sylan 569	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))))
139	14	ad5antr 716	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑀 ∈ (∞Met‘𝑋))
140		cnvimass 5626	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ⊆ dom 𝑓
141	48	simplbi 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ⊆ 𝑋)
142	141	ad2antrl 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → 𝑣 ⊆ 𝑋)
143	142	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑣 ⊆ 𝑋)
144	98, 143	sstrd 3762	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓 ⊆ 𝑋)
145	140, 144	syl5ss 3763	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ⊆ 𝑋)
146	145	sselda 3752	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑦 ∈ 𝑋)
147		simp-4r 770	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ⁺)
148	147	rpred 12075	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ)
149		elpreima 6480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 Fn dom 𝑓 → (𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑦 ∈ dom 𝑓 ∧ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))))
150	149	simplbda 487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓 Fn dom 𝑓 ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
151	96, 150	sylan 569	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
152		blhalf 22430	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑐 ∈ ℝ ∧ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑦(ball‘𝑀)(𝑐 / 2)) ⊆ ((𝑓‘𝑦)(ball‘𝑀)𝑐))
153	139, 146, 148, 151, 152	syl22anc 1477	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑦(ball‘𝑀)(𝑐 / 2)) ⊆ ((𝑓‘𝑦)(ball‘𝑀)𝑐))
154	153	ssrind 3988	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ (((𝑓‘𝑦)(ball‘𝑀)𝑐) ∩ 𝑌))
155	140	sseli 3748	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) → 𝑦 ∈ dom 𝑓)
156		ffvelrn 6500	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓:dom 𝑓⟶𝑌 ∧ 𝑦 ∈ dom 𝑓) → (𝑓‘𝑦) ∈ 𝑌)
157	92, 155, 156	syl2an 583	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ 𝑌)
158		simp-5r 774	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑌 ⊆ 𝑋)
159	158, 21	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑋 ∩ 𝑌) = 𝑌)
160	157, 159	eleqtrrd 2853	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ (𝑋 ∩ 𝑌))
161	113	ad4antlr 714	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ^*)
162	1	blres 22456	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ (𝑓‘𝑦) ∈ (𝑋 ∩ 𝑌) ∧ 𝑐 ∈ ℝ^*) → ((𝑓‘𝑦)(ball‘𝑁)𝑐) = (((𝑓‘𝑦)(ball‘𝑀)𝑐) ∩ 𝑌))
163	139, 160, 161, 162	syl3anc 1476	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑓‘𝑦)(ball‘𝑁)𝑐) = (((𝑓‘𝑦)(ball‘𝑀)𝑐) ∩ 𝑌))
164	154, 163	sseqtr4d 3791	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ((𝑓‘𝑦)(ball‘𝑁)𝑐))
165		fnfvelrn 6499	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 Fn dom 𝑓 ∧ 𝑦 ∈ dom 𝑓) → (𝑓‘𝑦) ∈ ran 𝑓)
166	96, 155, 165	syl2an 583	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ ran 𝑓)
167		oveq1 6800	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = (𝑓‘𝑦) → (𝑧(ball‘𝑁)𝑐) = ((𝑓‘𝑦)(ball‘𝑁)𝑐))
168	167	ssiun2s 4698	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓‘𝑦) ∈ ran 𝑓 → ((𝑓‘𝑦)(ball‘𝑁)𝑐) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
169	166, 168	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑓‘𝑦)(ball‘𝑁)𝑐) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
170	164, 169	sstrd 3762	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
171	170	adantlr 694	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
172	171	ex 397	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) → (𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)))
173	138, 172	syld 47	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)))
174	130, 173	pm2.61dne 3029	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
175	174	ralrimiva 3115	. . . . . . . . . . . . . . 15 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
176		iunss 4695	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ↔ ∀𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
177	175, 176	sylibr 224	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
178	126, 177	eqsstr3d 3789	. . . . . . . . . . . . 13 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
179	119, 178	eqssd 3769	. . . . . . . . . . . 12 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) = 𝑌)
180	108, 179	syl5eq 2817	. . . . . . . . . . 11 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌)
181		iuneq1 4668	. . . . . . . . . . . . 13 ⊢ (𝑤 = ran 𝑓 → ∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐))
182	181	eqeq1d 2773	. . . . . . . . . . . 12 ⊢ (𝑤 = ran 𝑓 → (∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌 ↔ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌))
183	182	rspcev 3460	. . . . . . . . . . 11 ⊢ ((ran 𝑓 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)
184	106, 180, 183	syl2anc 573	. . . . . . . . . 10 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)
185	184	ex 397	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ((dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
186	91, 185	syld 47	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ((𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
187	186	exlimdv 2013	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → (∃𝑓(𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
188	68, 187	mpd 15	. . . . . 6 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)
189	188	rexlimdvaa 3180	. . . . 5 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
190	47, 189	syld 47	. . . 4 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) → (∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
191	190	ralrimdva 3118	. . 3 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
192		istotbnd3 33902	. . . . 5 ⊢ (𝑁 ∈ (TotBnd‘𝑌) ↔ (𝑁 ∈ (Met‘𝑌) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
193	192	baib 525	. . . 4 ⊢ (𝑁 ∈ (Met‘𝑌) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
194	3, 193	syl 17	. . 3 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
195	191, 194	sylibrd 249	. 2 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → 𝑁 ∈ (TotBnd‘𝑌)))
196	39, 195	impbid 202	1 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 382 ∧ w3a 1071 = wceq 1631 ∃wex 1852 ∈ wcel 2145 ≠ wne 2943 ∀wral 3061 ∃wrex 3062 {crab 3065 ∩ cin 3722 ⊆ wss 3723 ∅c0 4063 𝒫 cpw 4297 ∪ ciun 4654 × cxp 5247 ^◡ccnv 5248 dom cdm 5249 ran crn 5250 ↾ cres 5251 “ cima 5252 Fn wfn 6026 ⟶wf 6027 ‘cfv 6031 (class class class)co 6793 Fincfn 8109 ℝcr 10137 ℝ^*cxr 10275 / cdiv 10886 2c2 11272 ℝ⁺crp 12035 ∞Metcxmt 19946 Metcme 19947 ballcbl 19948 TotBndctotbnd 33897

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-sep 4915 ax-nul 4923 ax-pow 4974 ax-pr 5034 ax-un 7096 ax-cnex 10194 ax-resscn 10195 ax-1cn 10196 ax-icn 10197 ax-addcl 10198 ax-addrcl 10199 ax-mulcl 10200 ax-mulrcl 10201 ax-mulcom 10202 ax-addass 10203 ax-mulass 10204 ax-distr 10205 ax-i2m1 10206 ax-1ne0 10207 ax-1rid 10208 ax-rnegex 10209 ax-rrecex 10210 ax-cnre 10211 ax-pre-lttri 10212 ax-pre-lttrn 10213 ax-pre-ltadd 10214 ax-pre-mulgt0 10215

This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3or 1072 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rmo 3069 df-rab 3070 df-v 3353 df-sbc 3588 df-csb 3683 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-pss 3739 df-nul 4064 df-if 4226 df-pw 4299 df-sn 4317 df-pr 4319 df-tp 4321 df-op 4323 df-uni 4575 df-int 4612 df-iun 4656 df-br 4787 df-opab 4847 df-mpt 4864 df-tr 4887 df-id 5157 df-eprel 5162 df-po 5170 df-so 5171 df-fr 5208 df-we 5210 df-xp 5255 df-rel 5256 df-cnv 5257 df-co 5258 df-dm 5259 df-rn 5260 df-res 5261 df-ima 5262 df-pred 5823 df-ord 5869 df-on 5870 df-lim 5871 df-suc 5872 df-iota 5994 df-fun 6033 df-fn 6034 df-f 6035 df-f1 6036 df-fo 6037 df-f1o 6038 df-fv 6039 df-riota 6754 df-ov 6796 df-oprab 6797 df-mpt2 6798 df-om 7213 df-1st 7315 df-2nd 7316 df-wrecs 7559 df-recs 7621 df-rdg 7659 df-1o 7713 df-oadd 7717 df-er 7896 df-map 8011 df-en 8110 df-dom 8111 df-sdom 8112 df-fin 8113 df-pnf 10278 df-mnf 10279 df-xr 10280 df-ltxr 10281 df-le 10282 df-sub 10470 df-neg 10471 df-div 10887 df-2 11281 df-rp 12036 df-xneg 12151 df-xadd 12152 df-xmul 12153 df-psmet 19953 df-xmet 19954 df-met 19955 df-bl 19956 df-totbnd 33899

This theorem is referenced by: sstotbnd 33906 sstotbnd3 33907

W3C validator