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 37798

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 24302	. . . . 5 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑀 ↾ (𝑌 × 𝑌)) ∈ (Met‘𝑌))
3	1, 2	eqeltrid 2838	. . . 4 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → 𝑁 ∈ (Met‘𝑌))
4		istotbnd3 37795	. . . . 5 ⊢ (𝑁 ∈ (TotBnd‘𝑌) ↔ (𝑁 ∈ (Met‘𝑌) ∧ ∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌))
5	4	baib 535	. . . 4 ⊢ (𝑁 ∈ (Met‘𝑌) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌))
6	3, 5	syl 17	. . 3 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌))
7		simpllr 775	. . . . . . . . . 10 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑌 ⊆ 𝑋)
8	7	sspwd 4588	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝒫 𝑌 ⊆ 𝒫 𝑋)
9	8	ssrind 4219	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → (𝒫 𝑌 ∩ Fin) ⊆ (𝒫 𝑋 ∩ Fin))
10		simprl 770	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑣 ∈ (𝒫 𝑌 ∩ Fin))
11	9, 10	sseldd 3959	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑣 ∈ (𝒫 𝑋 ∩ Fin))
12		simprr 772	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)
13		metxmet 24273	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀 ∈ (∞Met‘𝑋))
14	13	ad4antr 732	. . . . . . . . . . . . 13 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑀 ∈ (∞Met‘𝑋))
15		elfpw 9366	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ↔ (𝑣 ⊆ 𝑌 ∧ 𝑣 ∈ Fin))
16	15	simplbi 497	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) → 𝑣 ⊆ 𝑌)
17	16	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) → 𝑣 ⊆ 𝑌)
18	17	sselda 3958	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ 𝑌)
19		simp-4r 783	. . . . . . . . . . . . . . 15 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑌 ⊆ 𝑋)
20		sseqin2 4198	. . . . . . . . . . . . . . 15 ⊢ (𝑌 ⊆ 𝑋 ↔ (𝑋 ∩ 𝑌) = 𝑌)
21	19, 20	sylib 218	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → (𝑋 ∩ 𝑌) = 𝑌)
22	18, 21	eleqtrrd 2837	. . . . . . . . . . . . 13 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ (𝑋 ∩ 𝑌))
23		simpllr 775	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑑 ∈ ℝ⁺)
24	23	rpxrd 13052	. . . . . . . . . . . . 13 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑑 ∈ ℝ^*)
25	1	blres 24370	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ (𝑋 ∩ 𝑌) ∧ 𝑑 ∈ ℝ^*) → (𝑥(ball‘𝑁)𝑑) = ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌))
26	14, 22, 24, 25	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → (𝑥(ball‘𝑁)𝑑) = ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌))
27		inss1 4212	. . . . . . . . . . . 12 ⊢ ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌) ⊆ (𝑥(ball‘𝑀)𝑑)
28	26, 27	eqsstrdi 4003	. . . . . . . . . . 11 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑))
29	28	ralrimiva 3132	. . . . . . . . . 10 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) → ∀𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑))
30		ss2iun 4986	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))
31	29, 30	syl 17	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))
32	31	adantrr 717	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))
33	12, 32	eqsstrrd 3994	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))
34	11, 33	jca 511	. . . . . 6 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)))
35	34	ex 412	. . . . 5 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) → ((𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌) → (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))))
36	35	reximdv2 3150	. . . 4 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) → (∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌 → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)))
37	36	ralimdva 3152	. . 3 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌 → ∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)))
38	6, 37	sylbid 240	. 2 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) → ∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)))
39		simpr 484	. . . . . . 7 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) → 𝑐 ∈ ℝ⁺)
40	39	rphalfcld 13063	. . . . . 6 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) → (𝑐 / 2) ∈ ℝ⁺)
41		oveq2 7413	. . . . . . . . . 10 ⊢ (𝑑 = (𝑐 / 2) → (𝑥(ball‘𝑀)𝑑) = (𝑥(ball‘𝑀)(𝑐 / 2)))
42	41	iuneq2d 4998	. . . . . . . . 9 ⊢ (𝑑 = (𝑐 / 2) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))
43	42	sseq2d 3991	. . . . . . . 8 ⊢ (𝑑 = (𝑐 / 2) → (𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) ↔ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
44	43	rexbidv 3164	. . . . . . 7 ⊢ (𝑑 = (𝑐 / 2) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) ↔ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
45	44	rspcv 3597	. . . . . 6 ⊢ ((𝑐 / 2) ∈ ℝ⁺ → (∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
46	40, 45	syl 17	. . . . 5 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) → (∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
47		elfpw 9366	. . . . . . . . . . 11 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ↔ (𝑣 ⊆ 𝑋 ∧ 𝑣 ∈ Fin))
48	47	simprbi 496	. . . . . . . . . 10 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ∈ Fin)
49	48	ad2antrl 728	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → 𝑣 ∈ Fin)
50		ssrab2 4055	. . . . . . . . 9 ⊢ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ⊆ 𝑣
51		ssfi 9187	. . . . . . . . 9 ⊢ ((𝑣 ∈ Fin ∧ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ⊆ 𝑣) → {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin)
52	49, 50, 51	sylancl 586	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin)
53		oveq1 7412	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑥(ball‘𝑀)(𝑐 / 2)) = (𝑦(ball‘𝑀)(𝑐 / 2)))
54	53	ineq1d 4194	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌))
55		incom 4184	. . . . . . . . . . . . . . 15 ⊢ ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2)))
56	54, 55	eqtrdi 2786	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2))))
57		dfin5 3934	. . . . . . . . . . . . . 14 ⊢ (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2))) = {𝑧 ∈ 𝑌 ∣ 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))}
58	56, 57	eqtrdi 2786	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = {𝑧 ∈ 𝑌 ∣ 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))})
59	58	neeq1d 2991	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ {𝑧 ∈ 𝑌 ∣ 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))} ≠ ∅))
60		rabn0 4364	. . . . . . . . . . . 12 ⊢ ({𝑧 ∈ 𝑌 ∣ 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))} ≠ ∅ ↔ ∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
61	59, 60	bitrdi 287	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ ∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
62	61	elrab 3671	. . . . . . . . . 10 ⊢ (𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ↔ (𝑦 ∈ 𝑣 ∧ ∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
63	62	simprbi 496	. . . . . . . . 9 ⊢ (𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} → ∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
64	63	rgen 3053	. . . . . . . 8 ⊢ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))
65		eleq1 2822	. . . . . . . . 9 ⊢ (𝑧 = (𝑓‘𝑦) → (𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)) ↔ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
66	65	ac6sfi 9292	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → ∃𝑓(𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
67	52, 64, 66	sylancl 586	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ∃𝑓(𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
68		fdm 6715	. . . . . . . . . . . . . 14 ⊢ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → dom 𝑓 = {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅})
69	68	ad2antrl 728	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → dom 𝑓 = {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅})
70	69, 50	eqsstrdi 4003	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → dom 𝑓 ⊆ 𝑣)
71		simprl 770	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌)
72	69	feq2d 6692	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓:dom 𝑓⟶𝑌 ↔ 𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌))
73	71, 72	mpbird 257	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑓:dom 𝑓⟶𝑌)
74		simprr 772	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
75		ffn 6706	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → 𝑓 Fn {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅})
76		elpreima 7048	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 Fn {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} → (𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∧ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))))
77	75, 76	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → (𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∧ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))))
78	77	baibd 539	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ 𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}) → (𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
79	78	ralbidva 3161	. . . . . . . . . . . . . . 15 ⊢ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → (∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
80	79	ad2antrl 728	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
81	74, 80	mpbird 257	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))
82		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → 𝑦 = 𝑥)
83		oveq1 7412	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → (𝑦(ball‘𝑀)(𝑐 / 2)) = (𝑥(ball‘𝑀)(𝑐 / 2)))
84	83	imaeq2d 6047	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) = (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))
85	82, 84	eleq12d 2828	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))
86	85	ralrab2 3681	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))
87	81, 86	sylib 218	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))
88	70, 73, 87	3jca 1128	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))))
89	88	ex 412	. . . . . . . . . 10 ⊢ (𝑣 ∈ Fin → ((𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))))
90	49, 89	syl 17	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ((𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))))
91		simpr2 1196	. . . . . . . . . . . . 13 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓:dom 𝑓⟶𝑌)
92	91	frnd 6714	. . . . . . . . . . . 12 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓 ⊆ 𝑌)
93	91	ffnd 6707	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓 Fn dom 𝑓)
94	49	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑣 ∈ Fin)
95		simpr1 1195	. . . . . . . . . . . . . . 15 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓 ⊆ 𝑣)
96		ssfi 9187	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∈ Fin ∧ dom 𝑓 ⊆ 𝑣) → dom 𝑓 ∈ Fin)
97	94, 95, 96	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓 ∈ Fin)
98		fnfi 9192	. . . . . . . . . . . . . 14 ⊢ ((𝑓 Fn dom 𝑓 ∧ dom 𝑓 ∈ Fin) → 𝑓 ∈ Fin)
99	93, 97, 98	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓 ∈ Fin)
100		rnfi 9352	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ Fin → ran 𝑓 ∈ Fin)
101	99, 100	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓 ∈ Fin)
102		elfpw 9366	. . . . . . . . . . . 12 ⊢ (ran 𝑓 ∈ (𝒫 𝑌 ∩ Fin) ↔ (ran 𝑓 ⊆ 𝑌 ∧ ran 𝑓 ∈ Fin))
103	92, 101, 102	sylanbrc 583	. . . . . . . . . . 11 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓 ∈ (𝒫 𝑌 ∩ Fin))
104		oveq1 7412	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑥(ball‘𝑁)𝑐) = (𝑧(ball‘𝑁)𝑐))
105	104	cbviunv 5016	. . . . . . . . . . . 12 ⊢ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)
106	3	ad4antr 732	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑁 ∈ (Met‘𝑌))
107		metxmet 24273	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (Met‘𝑌) → 𝑁 ∈ (∞Met‘𝑌))
108	106, 107	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑁 ∈ (∞Met‘𝑌))
109	92	sselda 3958	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ 𝑌)
110		rpxr 13018	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ ℝ⁺ → 𝑐 ∈ ℝ^*)
111	110	ad4antlr 733	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑐 ∈ ℝ^*)
112		blssm 24357	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝑧 ∈ 𝑌 ∧ 𝑐 ∈ ℝ^*) → (𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
113	108, 109, 111, 112	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → (𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
114	113	ralrimiva 3132	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
115		iunss 5021	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌 ↔ ∀𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
116	114, 115	sylibr 234	. . . . . . . . . . . . 13 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
117		iunin1 5048	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = (∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌)
118		simplrr 777	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))
119	53	cbviunv 5016	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)) = ∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2))
120	118, 119	sseqtrdi 3999	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 ⊆ ∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)))
121		sseqin2 4198	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 ⊆ ∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ↔ (∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌)
122	120, 121	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → (∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌)
123	117, 122	eqtrid 2782	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌)
124		0ss 4375	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)
125		sseq1 3984	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ∅ → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ↔ ∅ ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)))
126	124, 125	mpbiri 258	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ∅ → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
127	126	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ∅ → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)))
128		simpr3 1197	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))
129	54	neeq1d 2991	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅))
130		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
131	53	imaeq2d 6047	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))) = (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))
132	130, 131	eleq12d 2828	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))) ↔ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))))
133	129, 132	imbi12d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → ((((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))) ↔ (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))))
134	133	rspccva 3600	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ 𝑦 ∈ 𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))))
135	128, 134	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))))
136	13	ad5antr 734	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑀 ∈ (∞Met‘𝑋))
137		cnvimass 6069	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ⊆ dom 𝑓
138	47	simplbi 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ⊆ 𝑋)
139	138	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → 𝑣 ⊆ 𝑋)
140	139	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑣 ⊆ 𝑋)
141	95, 140	sstrd 3969	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓 ⊆ 𝑋)
142	137, 141	sstrid 3970	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ⊆ 𝑋)
143	142	sselda 3958	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑦 ∈ 𝑋)
144		simp-4r 783	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ⁺)
145	144	rpred 13051	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ)
146		elpreima 7048	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 Fn dom 𝑓 → (𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑦 ∈ dom 𝑓 ∧ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))))
147	146	simplbda 499	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓 Fn dom 𝑓 ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
148	93, 147	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
149		blhalf 24344	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑐 ∈ ℝ ∧ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑦(ball‘𝑀)(𝑐 / 2)) ⊆ ((𝑓‘𝑦)(ball‘𝑀)𝑐))
150	136, 143, 145, 148, 149	syl22anc 838	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑦(ball‘𝑀)(𝑐 / 2)) ⊆ ((𝑓‘𝑦)(ball‘𝑀)𝑐))
151	150	ssrind 4219	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ (((𝑓‘𝑦)(ball‘𝑀)𝑐) ∩ 𝑌))
152	137	sseli 3954	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) → 𝑦 ∈ dom 𝑓)
153		ffvelcdm 7071	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓:dom 𝑓⟶𝑌 ∧ 𝑦 ∈ dom 𝑓) → (𝑓‘𝑦) ∈ 𝑌)
154	91, 152, 153	syl2an 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ 𝑌)
155		simp-5r 785	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑌 ⊆ 𝑋)
156	155, 20	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑋 ∩ 𝑌) = 𝑌)
157	154, 156	eleqtrrd 2837	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ (𝑋 ∩ 𝑌))
158	110	ad4antlr 733	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ^*)
159	1	blres 24370	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ (𝑓‘𝑦) ∈ (𝑋 ∩ 𝑌) ∧ 𝑐 ∈ ℝ^*) → ((𝑓‘𝑦)(ball‘𝑁)𝑐) = (((𝑓‘𝑦)(ball‘𝑀)𝑐) ∩ 𝑌))
160	136, 157, 158, 159	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑓‘𝑦)(ball‘𝑁)𝑐) = (((𝑓‘𝑦)(ball‘𝑀)𝑐) ∩ 𝑌))
161	151, 160	sseqtrrd 3996	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ((𝑓‘𝑦)(ball‘𝑁)𝑐))
162		fnfvelrn 7070	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 Fn dom 𝑓 ∧ 𝑦 ∈ dom 𝑓) → (𝑓‘𝑦) ∈ ran 𝑓)
163	93, 152, 162	syl2an 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ ran 𝑓)
164		oveq1 7412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = (𝑓‘𝑦) → (𝑧(ball‘𝑁)𝑐) = ((𝑓‘𝑦)(ball‘𝑁)𝑐))
165	164	ssiun2s 5024	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓‘𝑦) ∈ ran 𝑓 → ((𝑓‘𝑦)(ball‘𝑁)𝑐) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
166	163, 165	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑓‘𝑦)(ball‘𝑁)𝑐) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
167	161, 166	sstrd 3969	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
168	167	adantlr 715	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
169	168	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) → (𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)))
170	135, 169	syld 47	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)))
171	127, 170	pm2.61dne 3018	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
172	171	ralrimiva 3132	. . . . . . . . . . . . . . 15 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
173		iunss 5021	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ↔ ∀𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
174	172, 173	sylibr 234	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
175	123, 174	eqsstrrd 3994	. . . . . . . . . . . . 13 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
176	116, 175	eqssd 3976	. . . . . . . . . . . 12 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) = 𝑌)
177	105, 176	eqtrid 2782	. . . . . . . . . . 11 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌)
178		iuneq1 4984	. . . . . . . . . . . . 13 ⊢ (𝑤 = ran 𝑓 → ∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐))
179	178	eqeq1d 2737	. . . . . . . . . . . 12 ⊢ (𝑤 = ran 𝑓 → (∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌 ↔ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌))
180	179	rspcev 3601	. . . . . . . . . . 11 ⊢ ((ran 𝑓 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)
181	103, 177, 180	syl2anc 584	. . . . . . . . . 10 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)
182	181	ex 412	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ((dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
183	90, 182	syld 47	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ((𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
184	183	exlimdv 1933	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → (∃𝑓(𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
185	67, 184	mpd 15	. . . . . 6 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)
186	185	rexlimdvaa 3142	. . . . 5 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
187	46, 186	syld 47	. . . 4 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) → (∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
188	187	ralrimdva 3140	. . 3 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
189		istotbnd3 37795	. . . . 5 ⊢ (𝑁 ∈ (TotBnd‘𝑌) ↔ (𝑁 ∈ (Met‘𝑌) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
190	189	baib 535	. . . 4 ⊢ (𝑁 ∈ (Met‘𝑌) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
191	3, 190	syl 17	. . 3 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
192	188, 191	sylibrd 259	. 2 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → 𝑁 ∈ (TotBnd‘𝑌)))
193	38, 192	impbid 212	1 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∃wex 1779 ∈ wcel 2108 ≠ wne 2932 ∀wral 3051 ∃wrex 3060 {crab 3415 ∩ cin 3925 ⊆ wss 3926 ∅c0 4308 𝒫 cpw 4575 ∪ ciun 4967 × cxp 5652 ^◡ccnv 5653 dom cdm 5654 ran crn 5655 ↾ cres 5656 “ cima 5657 Fn wfn 6526 ⟶wf 6527 ‘cfv 6531 (class class class)co 7405 Fincfn 8959 ℝcr 11128 ℝ^*cxr 11268 / cdiv 11894 2c2 12295 ℝ⁺crp 13008 ∞Metcxmet 21300 Metcmet 21301 ballcbl 21302 TotBndctotbnd 37790

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729 ax-cnex 11185 ax-resscn 11186 ax-1cn 11187 ax-icn 11188 ax-addcl 11189 ax-addrcl 11190 ax-mulcl 11191 ax-mulrcl 11192 ax-mulcom 11193 ax-addass 11194 ax-mulass 11195 ax-distr 11196 ax-i2m1 11197 ax-1ne0 11198 ax-1rid 11199 ax-rnegex 11200 ax-rrecex 11201 ax-cnre 11202 ax-pre-lttri 11203 ax-pre-lttrn 11204 ax-pre-ltadd 11205 ax-pre-mulgt0 11206

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-iun 4969 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7362 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7862 df-1st 7988 df-2nd 7989 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-er 8719 df-map 8842 df-en 8960 df-dom 8961 df-sdom 8962 df-fin 8963 df-pnf 11271 df-mnf 11272 df-xr 11273 df-ltxr 11274 df-le 11275 df-sub 11468 df-neg 11469 df-div 11895 df-nn 12241 df-2 12303 df-rp 13009 df-xneg 13128 df-xadd 13129 df-xmul 13130 df-psmet 21307 df-xmet 21308 df-met 21309 df-bl 21310 df-totbnd 37792

This theorem is referenced by: sstotbnd 37799 sstotbnd3 37800

W3C validator