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 35054

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 22975	. . . . 5 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑀 ↾ (𝑌 × 𝑌)) ∈ (Met‘𝑌))
3	1, 2	eqeltrid 2919	. . . 4 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → 𝑁 ∈ (Met‘𝑌))
4		istotbnd3 35051	. . . . 5 ⊢ (𝑁 ∈ (TotBnd‘𝑌) ↔ (𝑁 ∈ (Met‘𝑌) ∧ ∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌))
5	4	baib 538	. . . 4 ⊢ (𝑁 ∈ (Met‘𝑌) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌))
6	3, 5	syl 17	. . 3 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌))
7		simpllr 774	. . . . . . . . . 10 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑌 ⊆ 𝑋)
8	7	sspwd 4556	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝒫 𝑌 ⊆ 𝒫 𝑋)
9	8	ssrind 4214	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → (𝒫 𝑌 ∩ Fin) ⊆ (𝒫 𝑋 ∩ Fin))
10		simprl 769	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑣 ∈ (𝒫 𝑌 ∩ Fin))
11	9, 10	sseldd 3970	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑣 ∈ (𝒫 𝑋 ∩ Fin))
12		simprr 771	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)
13		metxmet 22946	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀 ∈ (∞Met‘𝑋))
14	13	ad4antr 730	. . . . . . . . . . . . 13 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑀 ∈ (∞Met‘𝑋))
15		elfpw 8828	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ↔ (𝑣 ⊆ 𝑌 ∧ 𝑣 ∈ Fin))
16	15	simplbi 500	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) → 𝑣 ⊆ 𝑌)
17	16	adantl 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) → 𝑣 ⊆ 𝑌)
18	17	sselda 3969	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ 𝑌)
19		simp-4r 782	. . . . . . . . . . . . . . 15 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑌 ⊆ 𝑋)
20		sseqin2 4194	. . . . . . . . . . . . . . 15 ⊢ (𝑌 ⊆ 𝑋 ↔ (𝑋 ∩ 𝑌) = 𝑌)
21	19, 20	sylib 220	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → (𝑋 ∩ 𝑌) = 𝑌)
22	18, 21	eleqtrrd 2918	. . . . . . . . . . . . 13 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ (𝑋 ∩ 𝑌))
23		simpllr 774	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑑 ∈ ℝ⁺)
24	23	rpxrd 12435	. . . . . . . . . . . . 13 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑑 ∈ ℝ^*)
25	1	blres 23043	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ (𝑋 ∩ 𝑌) ∧ 𝑑 ∈ ℝ^*) → (𝑥(ball‘𝑁)𝑑) = ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌))
26	14, 22, 24, 25	syl3anc 1367	. . . . . . . . . . . 12 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → (𝑥(ball‘𝑁)𝑑) = ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌))
27		inss1 4207	. . . . . . . . . . . 12 ⊢ ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌) ⊆ (𝑥(ball‘𝑀)𝑑)
28	26, 27	eqsstrdi 4023	. . . . . . . . . . 11 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑))
29	28	ralrimiva 3184	. . . . . . . . . 10 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) → ∀𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑))
30		ss2iun 4939	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ (𝑥(ball‘𝑀)𝑑) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))
31	29, 30	syl 17	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑣 ∈ (𝒫 𝑌 ∩ Fin)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))
32	31	adantrr 715	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))
33	12, 32	eqsstrrd 4008	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))
34	11, 33	jca 514	. . . . . 6 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌)) → (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)))
35	34	ex 415	. . . . 5 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) → ((𝑣 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌) → (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))))
36	35	reximdv2 3273	. . . 4 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑑 ∈ ℝ⁺) → (∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌 → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)))
37	36	ralimdva 3179	. . 3 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑑) = 𝑌 → ∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)))
38	6, 37	sylbid 242	. 2 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) → ∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)))
39		simpr 487	. . . . . . 7 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) → 𝑐 ∈ ℝ⁺)
40	39	rphalfcld 12446	. . . . . 6 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) → (𝑐 / 2) ∈ ℝ⁺)
41		oveq2 7166	. . . . . . . . . 10 ⊢ (𝑑 = (𝑐 / 2) → (𝑥(ball‘𝑀)𝑑) = (𝑥(ball‘𝑀)(𝑐 / 2)))
42	41	iuneq2d 4950	. . . . . . . . 9 ⊢ (𝑑 = (𝑐 / 2) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))
43	42	sseq2d 4001	. . . . . . . 8 ⊢ (𝑑 = (𝑐 / 2) → (𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) ↔ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
44	43	rexbidv 3299	. . . . . . 7 ⊢ (𝑑 = (𝑐 / 2) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) ↔ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
45	44	rspcv 3620	. . . . . 6 ⊢ ((𝑐 / 2) ∈ ℝ⁺ → (∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
46	40, 45	syl 17	. . . . 5 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) → (∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2))))
47		elfpw 8828	. . . . . . . . . . 11 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ↔ (𝑣 ⊆ 𝑋 ∧ 𝑣 ∈ Fin))
48	47	simprbi 499	. . . . . . . . . 10 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ∈ Fin)
49	48	ad2antrl 726	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → 𝑣 ∈ Fin)
50		ssrab2 4058	. . . . . . . . 9 ⊢ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ⊆ 𝑣
51		ssfi 8740	. . . . . . . . 9 ⊢ ((𝑣 ∈ Fin ∧ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ⊆ 𝑣) → {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin)
52	49, 50, 51	sylancl 588	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin)
53		oveq1 7165	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑥(ball‘𝑀)(𝑐 / 2)) = (𝑦(ball‘𝑀)(𝑐 / 2)))
54	53	ineq1d 4190	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌))
55		incom 4180	. . . . . . . . . . . . . . 15 ⊢ ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2)))
56	54, 55	syl6eq 2874	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2))))
57		dfin5 3946	. . . . . . . . . . . . . 14 ⊢ (𝑌 ∩ (𝑦(ball‘𝑀)(𝑐 / 2))) = {𝑧 ∈ 𝑌 ∣ 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))}
58	56, 57	syl6eq 2874	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = {𝑧 ∈ 𝑌 ∣ 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))})
59	58	neeq1d 3077	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ {𝑧 ∈ 𝑌 ∣ 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))} ≠ ∅))
60		rabn0 4341	. . . . . . . . . . . 12 ⊢ ({𝑧 ∈ 𝑌 ∣ 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))} ≠ ∅ ↔ ∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
61	59, 60	syl6bb 289	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ ∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
62	61	elrab 3682	. . . . . . . . . 10 ⊢ (𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ↔ (𝑦 ∈ 𝑣 ∧ ∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
63	62	simprbi 499	. . . . . . . . 9 ⊢ (𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} → ∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
64	63	rgen 3150	. . . . . . . 8 ⊢ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))
65		eleq1 2902	. . . . . . . . 9 ⊢ (𝑧 = (𝑓‘𝑦) → (𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2)) ↔ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
66	65	ac6sfi 8764	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} ∈ Fin ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}∃𝑧 ∈ 𝑌 𝑧 ∈ (𝑦(ball‘𝑀)(𝑐 / 2))) → ∃𝑓(𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
67	52, 64, 66	sylancl 588	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → ∃𝑓(𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
68		fdm 6524	. . . . . . . . . . . . . 14 ⊢ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → dom 𝑓 = {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅})
69	68	ad2antrl 726	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → dom 𝑓 = {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅})
70	69, 50	eqsstrdi 4023	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → dom 𝑓 ⊆ 𝑣)
71		simprl 769	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌)
72	69	feq2d 6502	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓:dom 𝑓⟶𝑌 ↔ 𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌))
73	71, 72	mpbird 259	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑓:dom 𝑓⟶𝑌)
74		simprr 771	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
75		ffn 6516	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → 𝑓 Fn {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅})
76		elpreima 6830	. . . . . . . . . . . . . . . . . 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 542	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ 𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}) → (𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
79	78	ralbidva 3198	. . . . . . . . . . . . . . 15 ⊢ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 → (∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
80	79	ad2antrl 726	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2))))
81	74, 80	mpbird 259	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))
82		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → 𝑦 = 𝑥)
83		oveq1 7165	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → (𝑦(ball‘𝑀)(𝑐 / 2)) = (𝑥(ball‘𝑀)(𝑐 / 2)))
84	83	imaeq2d 5931	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) = (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))
85	82, 84	eleq12d 2909	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))
86	85	ralrab2 3692	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))
87	81, 86	sylib 220	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))
88	70, 73, 87	3jca 1124	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ Fin ∧ (𝑓:{𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅}⟶𝑌 ∧ ∀𝑦 ∈ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅} (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))))))
89	88	ex 415	. . . . . . . . . 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 1191	. . . . . . . . . . . . 13 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓:dom 𝑓⟶𝑌)
92	91	frnd 6523	. . . . . . . . . . . 12 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓 ⊆ 𝑌)
93	91	ffnd 6517	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓 Fn dom 𝑓)
94	49	adantr 483	. . . . . . . . . . . . . . 15 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑣 ∈ Fin)
95		simpr1 1190	. . . . . . . . . . . . . . 15 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓 ⊆ 𝑣)
96		ssfi 8740	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∈ Fin ∧ dom 𝑓 ⊆ 𝑣) → dom 𝑓 ∈ Fin)
97	94, 95, 96	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓 ∈ Fin)
98		fnfi 8798	. . . . . . . . . . . . . 14 ⊢ ((𝑓 Fn dom 𝑓 ∧ dom 𝑓 ∈ Fin) → 𝑓 ∈ Fin)
99	93, 97, 98	syl2anc 586	. . . . . . . . . . . . 13 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑓 ∈ Fin)
100		rnfi 8809	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ Fin → ran 𝑓 ∈ Fin)
101	99, 100	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓 ∈ Fin)
102		elfpw 8828	. . . . . . . . . . . 12 ⊢ (ran 𝑓 ∈ (𝒫 𝑌 ∩ Fin) ↔ (ran 𝑓 ⊆ 𝑌 ∧ ran 𝑓 ∈ Fin))
103	92, 101, 102	sylanbrc 585	. . . . . . . . . . 11 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ran 𝑓 ∈ (𝒫 𝑌 ∩ Fin))
104		oveq1 7165	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑥(ball‘𝑁)𝑐) = (𝑧(ball‘𝑁)𝑐))
105	104	cbviunv 4967	. . . . . . . . . . . 12 ⊢ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)
106	3	ad4antr 730	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑁 ∈ (Met‘𝑌))
107		metxmet 22946	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (Met‘𝑌) → 𝑁 ∈ (∞Met‘𝑌))
108	106, 107	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑁 ∈ (∞Met‘𝑌))
109	92	sselda 3969	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ 𝑌)
110		rpxr 12401	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ ℝ⁺ → 𝑐 ∈ ℝ^*)
111	110	ad4antlr 731	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → 𝑐 ∈ ℝ^*)
112		blssm 23030	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝑧 ∈ 𝑌 ∧ 𝑐 ∈ ℝ^*) → (𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
113	108, 109, 111, 112	syl3anc 1367	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑧 ∈ ran 𝑓) → (𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
114	113	ralrimiva 3184	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
115		iunss 4971	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌 ↔ ∀𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
116	114, 115	sylibr 236	. . . . . . . . . . . . 13 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ⊆ 𝑌)
117		iunin1 4996	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = (∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌)
118		simplrr 776	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))
119	53	cbviunv 4967	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)) = ∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2))
120	118, 119	sseqtrdi 4019	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 ⊆ ∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)))
121		sseqin2 4194	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 ⊆ ∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ↔ (∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌)
122	120, 121	sylib 220	. . . . . . . . . . . . . . 15 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → (∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌)
123	117, 122	syl5eq 2870	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = 𝑌)
124		0ss 4352	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)
125		sseq1 3994	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) = ∅ → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ↔ ∅ ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐)))
126	124, 125	mpbiri 260	. . . . . . . . . . . . . . . . . 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 1192	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))
129	54	neeq1d 3077	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ ↔ ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅))
130		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
131	53	imaeq2d 5931	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))) = (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))
132	130, 131	eleq12d 2909	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2))) ↔ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))))
133	129, 132	imbi12d 347	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → ((((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))) ↔ (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))))))
134	133	rspccva 3624	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ 𝑦 ∈ 𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))))
135	128, 134	sylan 582	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) → (((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))))
136	13	ad5antr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑀 ∈ (∞Met‘𝑋))
137		cnvimass 5951	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ⊆ dom 𝑓
138	47	simplbi 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ⊆ 𝑋)
139	138	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) → 𝑣 ⊆ 𝑋)
140	139	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑣 ⊆ 𝑋)
141	95, 140	sstrd 3979	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → dom 𝑓 ⊆ 𝑋)
142	137, 141	sstrid 3980	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ⊆ 𝑋)
143	142	sselda 3969	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑦 ∈ 𝑋)
144		simp-4r 782	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ⁺)
145	144	rpred 12434	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ)
146		elpreima 6830	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 Fn dom 𝑓 → (𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) ↔ (𝑦 ∈ dom 𝑓 ∧ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))))
147	146	simplbda 502	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓 Fn dom 𝑓 ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
148	93, 147	sylan 582	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))
149		blhalf 23017	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑐 ∈ ℝ ∧ (𝑓‘𝑦) ∈ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑦(ball‘𝑀)(𝑐 / 2)) ⊆ ((𝑓‘𝑦)(ball‘𝑀)𝑐))
150	136, 143, 145, 148, 149	syl22anc 836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑦(ball‘𝑀)(𝑐 / 2)) ⊆ ((𝑓‘𝑦)(ball‘𝑀)𝑐))
151	150	ssrind 4214	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ (((𝑓‘𝑦)(ball‘𝑀)𝑐) ∩ 𝑌))
152	137	sseli 3965	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2))) → 𝑦 ∈ dom 𝑓)
153		ffvelrn 6851	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓:dom 𝑓⟶𝑌 ∧ 𝑦 ∈ dom 𝑓) → (𝑓‘𝑦) ∈ 𝑌)
154	91, 152, 153	syl2an 597	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ 𝑌)
155		simp-5r 784	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑌 ⊆ 𝑋)
156	155, 20	sylib 220	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑋 ∩ 𝑌) = 𝑌)
157	154, 156	eleqtrrd 2918	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ (𝑋 ∩ 𝑌))
158	110	ad4antlr 731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → 𝑐 ∈ ℝ^*)
159	1	blres 23043	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ (𝑓‘𝑦) ∈ (𝑋 ∩ 𝑌) ∧ 𝑐 ∈ ℝ^*) → ((𝑓‘𝑦)(ball‘𝑁)𝑐) = (((𝑓‘𝑦)(ball‘𝑀)𝑐) ∩ 𝑌))
160	136, 157, 158, 159	syl3anc 1367	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑓‘𝑦)(ball‘𝑁)𝑐) = (((𝑓‘𝑦)(ball‘𝑀)𝑐) ∩ 𝑌))
161	151, 160	sseqtrrd 4010	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ((𝑓‘𝑦)(ball‘𝑁)𝑐))
162		fnfvelrn 6850	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 Fn dom 𝑓 ∧ 𝑦 ∈ dom 𝑓) → (𝑓‘𝑦) ∈ ran 𝑓)
163	93, 152, 162	syl2an 597	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → (𝑓‘𝑦) ∈ ran 𝑓)
164		oveq1 7165	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = (𝑓‘𝑦) → (𝑧(ball‘𝑁)𝑐) = ((𝑓‘𝑦)(ball‘𝑁)𝑐))
165	164	ssiun2s 4974	. . . . . . . . . . . . . . . . . . . . . 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 3979	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
168	167	adantlr 713	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) ∧ 𝑦 ∈ (^◡𝑓 “ (𝑦(ball‘𝑀)(𝑐 / 2)))) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
169	168	ex 415	. . . . . . . . . . . . . . . . . 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 3105	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) ∧ 𝑦 ∈ 𝑣) → ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
172	171	ralrimiva 3184	. . . . . . . . . . . . . . 15 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∀𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
173		iunss 4971	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) ↔ ∀𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
174	172, 173	sylibr 236	. . . . . . . . . . . . . 14 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑦 ∈ 𝑣 ((𝑦(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
175	123, 174	eqsstrrd 4008	. . . . . . . . . . . . 13 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → 𝑌 ⊆ ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐))
176	116, 175	eqssd 3986	. . . . . . . . . . . 12 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑧 ∈ ran 𝑓(𝑧(ball‘𝑁)𝑐) = 𝑌)
177	105, 176	syl5eq 2870	. . . . . . . . . . 11 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌)
178		iuneq1 4937	. . . . . . . . . . . . 13 ⊢ (𝑤 = ran 𝑓 → ∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐))
179	178	eqeq1d 2825	. . . . . . . . . . . 12 ⊢ (𝑤 = ran 𝑓 → (∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌 ↔ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌))
180	179	rspcev 3625	. . . . . . . . . . 11 ⊢ ((ran 𝑓 ∈ (𝒫 𝑌 ∩ Fin) ∧ ∪ 𝑥 ∈ ran 𝑓(𝑥(ball‘𝑁)𝑐) = 𝑌) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)
181	103, 177, 180	syl2anc 586	. . . . . . . . . 10 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) ∧ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)))) ∧ (dom 𝑓 ⊆ 𝑣 ∧ 𝑓:dom 𝑓⟶𝑌 ∧ ∀𝑥 ∈ 𝑣 (((𝑥(ball‘𝑀)(𝑐 / 2)) ∩ 𝑌) ≠ ∅ → 𝑥 ∈ (^◡𝑓 “ (𝑥(ball‘𝑀)(𝑐 / 2)))))) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌)
182	181	ex 415	. . . . . . . . 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 1934	. . . . . . 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 3287	. . . . 5 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑐 / 2)) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
187	46, 186	syld 47	. . . 4 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑐 ∈ ℝ⁺) → (∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
188	187	ralrimdva 3191	. . 3 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
189		istotbnd3 35051	. . . . 5 ⊢ (𝑁 ∈ (TotBnd‘𝑌) ↔ (𝑁 ∈ (Met‘𝑌) ∧ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
190	189	baib 538	. . . 4 ⊢ (𝑁 ∈ (Met‘𝑌) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
191	3, 190	syl 17	. . 3 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑐 ∈ ℝ⁺ ∃𝑤 ∈ (𝒫 𝑌 ∩ Fin)∪ 𝑥 ∈ 𝑤 (𝑥(ball‘𝑁)𝑐) = 𝑌))
192	188, 191	sylibrd 261	. 2 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) → 𝑁 ∈ (TotBnd‘𝑌)))
193	38, 192	impbid 214	1 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ⁺ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1537 ∃wex 1780 ∈ wcel 2114 ≠ wne 3018 ∀wral 3140 ∃wrex 3141 {crab 3144 ∩ cin 3937 ⊆ wss 3938 ∅c0 4293 𝒫 cpw 4541 ∪ ciun 4921 × cxp 5555 ^◡ccnv 5556 dom cdm 5557 ran crn 5558 ↾ cres 5559 “ cima 5560 Fn wfn 6352 ⟶wf 6353 ‘cfv 6357 (class class class)co 7158 Fincfn 8511 ℝcr 10538 ℝ^*cxr 10676 / cdiv 11299 2c2 11695 ℝ⁺crp 12392 ∞Metcxmet 20532 Metcmet 20533 ballcbl 20534 TotBndctotbnd 35046

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-cnex 10595 ax-resscn 10596 ax-1cn 10597 ax-icn 10598 ax-addcl 10599 ax-addrcl 10600 ax-mulcl 10601 ax-mulrcl 10602 ax-mulcom 10603 ax-addass 10604 ax-mulass 10605 ax-distr 10606 ax-i2m1 10607 ax-1ne0 10608 ax-1rid 10609 ax-rnegex 10610 ax-rrecex 10611 ax-cnre 10612 ax-pre-lttri 10613 ax-pre-lttrn 10614 ax-pre-ltadd 10615 ax-pre-mulgt0 10616

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-nel 3126 df-ral 3145 df-rex 3146 df-reu 3147 df-rmo 3148 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-pss 3956 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4841 df-int 4879 df-iun 4923 df-br 5069 df-opab 5131 df-mpt 5149 df-tr 5175 df-id 5462 df-eprel 5467 df-po 5476 df-so 5477 df-fr 5516 df-we 5518 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-pred 6150 df-ord 6196 df-on 6197 df-lim 6198 df-suc 6199 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-riota 7116 df-ov 7161 df-oprab 7162 df-mpo 7163 df-om 7583 df-1st 7691 df-2nd 7692 df-wrecs 7949 df-recs 8010 df-rdg 8048 df-1o 8104 df-oadd 8108 df-er 8291 df-map 8410 df-en 8512 df-dom 8513 df-sdom 8514 df-fin 8515 df-pnf 10679 df-mnf 10680 df-xr 10681 df-ltxr 10682 df-le 10683 df-sub 10874 df-neg 10875 df-div 11300 df-2 11703 df-rp 12393 df-xneg 12510 df-xadd 12511 df-xmul 12512 df-psmet 20539 df-xmet 20540 df-met 20541 df-bl 20542 df-totbnd 35048

This theorem is referenced by: sstotbnd 35055 sstotbnd3 35056

W3C validator