sstotbnd2

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

		Ref	Expression
	Hypothesis	sstotbnd.2	$⊢ N = {M ↾}_{(Y \times Y)}$
	Assertion	sstotbnd2	$⊢ (M \in Met (X) \land Y \subseteq X) \to (N \in TotBnd (Y) \leftrightarrow \forall d \in ℝ^{+} \exists v \in (𝒫 X \cap Fin) Y \subseteq ⋃_{x \in v} (x ball (M) d))$

Proof

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

Metamath Proof Explorer

Theorem sstotbnd2

Proof