heicant

Description: Heine-Cantor theorem: a continuous mapping between metric spaces whose domain is compact is uniformly continuous. Theorem on Rosenlicht p. 80. (Contributed by Brendan Leahy, 13-Aug-2018) (Proof shortened by AV, 27-Sep-2020)

	Ref	Expression
Hypotheses	heicant.c	$⊢ φ \to C \in ∞Met (X)$
	heicant.d	$⊢ φ \to D \in ∞Met (Y)$
	heicant.j	$⊢ φ \to MetOpen (C) \in Comp$
	heicant.x	$⊢ φ \to X \neq \emptyset$
	heicant.y	$⊢ φ \to Y \neq \emptyset$
Assertion	heicant	$⊢ φ \to metUnif (C) uCn metUnif (D) = MetOpen (C) Cn MetOpen (D)$

Proof

Step	Hyp	Ref	Expression
1		heicant.c	$⊢ φ \to C \in ∞Met (X)$
2		heicant.d	$⊢ φ \to D \in ∞Met (Y)$
3		heicant.j	$⊢ φ \to MetOpen (C) \in Comp$
4		heicant.x	$⊢ φ \to X \neq \emptyset$
5		heicant.y	$⊢ φ \to Y \neq \emptyset$
6		breq2	$⊢ d = y \to (f (x) D f (w) < d \leftrightarrow f (x) D f (w) < y)$
7	6	imbi2d	$⊢ d = y \to ((x C w < z \to f (x) D f (w) < d) \leftrightarrow (x C w < z \to f (x) D f (w) < y))$
8	7	2ralbidv	$⊢ d = y \to (\forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d) \leftrightarrow \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < y))$
9	8	rexbidv	$⊢ d = y \to (\exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d) \leftrightarrow \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < y))$
10	9	cbvralvw	$⊢ \forall d \in ℝ^{+} \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d) \leftrightarrow \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < y)$
11		r19.12	$⊢ \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < y) \to \forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < y)$
12	11	ralimi	$⊢ \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < y) \to \forall y \in ℝ^{+} \forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < y)$
13	10 12	sylbi	$⊢ \forall d \in ℝ^{+} \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d) \to \forall y \in ℝ^{+} \forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < y)$
14		rphalfcl	$⊢ d \in ℝ^{+} \to \frac{d}{2} \in ℝ^{+}$
15		breq2	$⊢ y = \frac{d}{2} \to (f (x) D f (w) < y \leftrightarrow f (x) D f (w) < \frac{d}{2})$
16	15	imbi2d	$⊢ y = \frac{d}{2} \to ((x C w < z \to f (x) D f (w) < y) \leftrightarrow (x C w < z \to f (x) D f (w) < \frac{d}{2}))$
17	16	ralbidv	$⊢ y = \frac{d}{2} \to (\forall w \in X (x C w < z \to f (x) D f (w) < y) \leftrightarrow \forall w \in X (x C w < z \to f (x) D f (w) < \frac{d}{2}))$
18	17	rexbidv	$⊢ y = \frac{d}{2} \to (\exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < y) \leftrightarrow \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < \frac{d}{2}))$
19	18	ralbidv	$⊢ y = \frac{d}{2} \to (\forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < y) \leftrightarrow \forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < \frac{d}{2}))$
20	19	rspcva	$⊢ (\frac{d}{2} \in ℝ^{+} \land \forall y \in ℝ^{+} \forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < y)) \to \forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < \frac{d}{2})$
21	3	ad3antrrr	$⊢ (((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land \forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < \frac{d}{2})) \to MetOpen (C) \in Comp$
22	1	ad2antrr	$⊢ ((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \to C \in ∞Met (X)$
23	22	anim1i	$⊢ (((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land x \in X) \to (C \in ∞Met (X) \land x \in X)$
24		rphalfcl	$⊢ z \in ℝ^{+} \to \frac{z}{2} \in ℝ^{+}$
25	24	rpxrd	$⊢ z \in ℝ^{+} \to \frac{z}{2} \in ℝ^{*}$
26		eqid	$⊢ MetOpen (C) = MetOpen (C)$
27	26	blopn	$⊢ (C \in ∞Met (X) \land x \in X \land \frac{z}{2} \in ℝ^{*}) \to x ball (C) (\frac{z}{2}) \in MetOpen (C)$
28	27	3expa	$⊢ ((C \in ∞Met (X) \land x \in X) \land \frac{z}{2} \in ℝ^{*}) \to x ball (C) (\frac{z}{2}) \in MetOpen (C)$
29	23 25 28	syl2an	$⊢ ((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land x \in X) \land z \in ℝ^{+}) \to x ball (C) (\frac{z}{2}) \in MetOpen (C)$
30	29	adantr	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land x \in X) \land z \in ℝ^{+}) \land \forall w \in X (x C w < z \to f (x) D f (w) < \frac{d}{2})) \to x ball (C) (\frac{z}{2}) \in MetOpen (C)$
31	24	rpgt0d	$⊢ z \in ℝ^{+} \to 0 < \frac{z}{2}$
32	25 31	jca	$⊢ z \in ℝ^{+} \to (\frac{z}{2} \in ℝ^{*} \land 0 < \frac{z}{2})$
33		xblcntr	$⊢ (C \in ∞Met (X) \land x \in X \land (\frac{z}{2} \in ℝ^{*} \land 0 < \frac{z}{2})) \to x \in (x ball (C) (\frac{z}{2}))$
34	33	3expa	$⊢ ((C \in ∞Met (X) \land x \in X) \land (\frac{z}{2} \in ℝ^{*} \land 0 < \frac{z}{2})) \to x \in (x ball (C) (\frac{z}{2}))$
35	23 32 34	syl2an	$⊢ ((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land x \in X) \land z \in ℝ^{+}) \to x \in (x ball (C) (\frac{z}{2}))$
36	35	adantr	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land x \in X) \land z \in ℝ^{+}) \land \forall w \in X (x C w < z \to f (x) D f (w) < \frac{d}{2})) \to x \in (x ball (C) (\frac{z}{2}))$
37		opelxpi	$⊢ (x \in X \land \frac{z}{2} \in ℝ^{+}) \to ⟨x, \frac{z}{2}⟩ \in (X \times ℝ^{+})$
38	24 37	sylan2	$⊢ (x \in X \land z \in ℝ^{+}) \to ⟨x, \frac{z}{2}⟩ \in (X \times ℝ^{+})$
39	38	ad4ant23	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land x \in X) \land z \in ℝ^{+}) \land \forall w \in X (x C w < z \to f (x) D f (w) < \frac{d}{2})) \to ⟨x, \frac{z}{2}⟩ \in (X \times ℝ^{+})$
40		rpcn	$⊢ z \in ℝ^{+} \to z \in ℂ$
41	40	2halvesd	$⊢ z \in ℝ^{+} \to (\frac{z}{2}) + (\frac{z}{2}) = z$
42	41	breq2d	$⊢ z \in ℝ^{+} \to (x C c < (\frac{z}{2}) + (\frac{z}{2}) \leftrightarrow x C c < z)$
43	42	imbi1d	$⊢ z \in ℝ^{+} \to ((x C c < (\frac{z}{2}) + (\frac{z}{2}) \to f (x) D f (c) < \frac{d}{2}) \leftrightarrow (x C c < z \to f (x) D f (c) < \frac{d}{2}))$
44	43	ralbidv	$⊢ z \in ℝ^{+} \to (\forall c \in X (x C c < (\frac{z}{2}) + (\frac{z}{2}) \to f (x) D f (c) < \frac{d}{2}) \leftrightarrow \forall c \in X (x C c < z \to f (x) D f (c) < \frac{d}{2}))$
45		oveq2	$⊢ c = w \to x C c = x C w$
46	45	breq1d	$⊢ c = w \to (x C c < z \leftrightarrow x C w < z)$
47		fveq2	$⊢ c = w \to f (c) = f (w)$
48	47	oveq2d	$⊢ c = w \to f (x) D f (c) = f (x) D f (w)$
49	48	breq1d	$⊢ c = w \to (f (x) D f (c) < \frac{d}{2} \leftrightarrow f (x) D f (w) < \frac{d}{2})$
50	46 49	imbi12d	$⊢ c = w \to ((x C c < z \to f (x) D f (c) < \frac{d}{2}) \leftrightarrow (x C w < z \to f (x) D f (w) < \frac{d}{2}))$
51	50	cbvralvw	$⊢ \forall c \in X (x C c < z \to f (x) D f (c) < \frac{d}{2}) \leftrightarrow \forall w \in X (x C w < z \to f (x) D f (w) < \frac{d}{2})$
52	44 51	bitrdi	$⊢ z \in ℝ^{+} \to (\forall c \in X (x C c < (\frac{z}{2}) + (\frac{z}{2}) \to f (x) D f (c) < \frac{d}{2}) \leftrightarrow \forall w \in X (x C w < z \to f (x) D f (w) < \frac{d}{2}))$
53	52	biimpar	$⊢ (z \in ℝ^{+} \land \forall w \in X (x C w < z \to f (x) D f (w) < \frac{d}{2})) \to \forall c \in X (x C c < (\frac{z}{2}) + (\frac{z}{2}) \to f (x) D f (c) < \frac{d}{2})$
54	53	adantll	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land x \in X) \land z \in ℝ^{+}) \land \forall w \in X (x C w < z \to f (x) D f (w) < \frac{d}{2})) \to \forall c \in X (x C c < (\frac{z}{2}) + (\frac{z}{2}) \to f (x) D f (c) < \frac{d}{2})$
55		vex	$⊢ x \in V$
56		ovex	$⊢ \frac{z}{2} \in V$
57	55 56	op1std	$⊢ p = ⟨x, \frac{z}{2}⟩ \to 1^{st} (p) = x$
58	55 56	op2ndd	$⊢ p = ⟨x, \frac{z}{2}⟩ \to 2^{nd} (p) = \frac{z}{2}$
59	57 58	oveq12d	$⊢ p = ⟨x, \frac{z}{2}⟩ \to 1^{st} (p) ball (C) 2^{nd} (p) = x ball (C) (\frac{z}{2})$
60	59	eqcomd	$⊢ p = ⟨x, \frac{z}{2}⟩ \to x ball (C) (\frac{z}{2}) = 1^{st} (p) ball (C) 2^{nd} (p)$
61	60	biantrurd	$⊢ p = ⟨x, \frac{z}{2}⟩ \to (\forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2}) \leftrightarrow (x ball (C) (\frac{z}{2}) = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2})))$
62	57	oveq1d	$⊢ p = ⟨x, \frac{z}{2}⟩ \to 1^{st} (p) C c = x C c$
63	58 58	oveq12d	$⊢ p = ⟨x, \frac{z}{2}⟩ \to 2^{nd} (p) + 2^{nd} (p) = (\frac{z}{2}) + (\frac{z}{2})$
64	62 63	breq12d	$⊢ p = ⟨x, \frac{z}{2}⟩ \to (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \leftrightarrow x C c < (\frac{z}{2}) + (\frac{z}{2}))$
65	57	fveq2d	$⊢ p = ⟨x, \frac{z}{2}⟩ \to f (1^{st} (p)) = f (x)$
66	65	oveq1d	$⊢ p = ⟨x, \frac{z}{2}⟩ \to f (1^{st} (p)) D f (c) = f (x) D f (c)$
67	66	breq1d	$⊢ p = ⟨x, \frac{z}{2}⟩ \to (f (1^{st} (p)) D f (c) < \frac{d}{2} \leftrightarrow f (x) D f (c) < \frac{d}{2})$
68	64 67	imbi12d	$⊢ p = ⟨x, \frac{z}{2}⟩ \to ((1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2}) \leftrightarrow (x C c < (\frac{z}{2}) + (\frac{z}{2}) \to f (x) D f (c) < \frac{d}{2}))$
69	68	ralbidv	$⊢ p = ⟨x, \frac{z}{2}⟩ \to (\forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2}) \leftrightarrow \forall c \in X (x C c < (\frac{z}{2}) + (\frac{z}{2}) \to f (x) D f (c) < \frac{d}{2}))$
70	61 69	bitr3d	$⊢ p = ⟨x, \frac{z}{2}⟩ \to ((x ball (C) (\frac{z}{2}) = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2})) \leftrightarrow \forall c \in X (x C c < (\frac{z}{2}) + (\frac{z}{2}) \to f (x) D f (c) < \frac{d}{2}))$
71	70	rspcev	$⊢ (⟨x, \frac{z}{2}⟩ \in (X \times ℝ^{+}) \land \forall c \in X (x C c < (\frac{z}{2}) + (\frac{z}{2}) \to f (x) D f (c) < \frac{d}{2})) \to \exists p \in (X \times ℝ^{+}) (x ball (C) (\frac{z}{2}) = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2}))$
72	39 54 71	syl2anc	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land x \in X) \land z \in ℝ^{+}) \land \forall w \in X (x C w < z \to f (x) D f (w) < \frac{d}{2})) \to \exists p \in (X \times ℝ^{+}) (x ball (C) (\frac{z}{2}) = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2}))$
73		eleq2	$⊢ b = x ball (C) (\frac{z}{2}) \to (x \in b \leftrightarrow x \in (x ball (C) (\frac{z}{2})))$
74		eqeq1	$⊢ b = x ball (C) (\frac{z}{2}) \to (b = 1^{st} (p) ball (C) 2^{nd} (p) \leftrightarrow x ball (C) (\frac{z}{2}) = 1^{st} (p) ball (C) 2^{nd} (p))$
75	74	anbi1d	$⊢ b = x ball (C) (\frac{z}{2}) \to ((b = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2})) \leftrightarrow (x ball (C) (\frac{z}{2}) = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2})))$
76	75	rexbidv	$⊢ b = x ball (C) (\frac{z}{2}) \to (\exists p \in (X \times ℝ^{+}) (b = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2})) \leftrightarrow \exists p \in (X \times ℝ^{+}) (x ball (C) (\frac{z}{2}) = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2})))$
77	73 76	anbi12d	$⊢ b = x ball (C) (\frac{z}{2}) \to ((x \in b \land \exists p \in (X \times ℝ^{+}) (b = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2}))) \leftrightarrow (x \in (x ball (C) (\frac{z}{2})) \land \exists p \in (X \times ℝ^{+}) (x ball (C) (\frac{z}{2}) = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2}))))$
78	77	rspcev	$⊢ (x ball (C) (\frac{z}{2}) \in MetOpen (C) \land (x \in (x ball (C) (\frac{z}{2})) \land \exists p \in (X \times ℝ^{+}) (x ball (C) (\frac{z}{2}) = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2})))) \to \exists b \in MetOpen (C) (x \in b \land \exists p \in (X \times ℝ^{+}) (b = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2})))$
79	30 36 72 78	syl12anc	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land x \in X) \land z \in ℝ^{+}) \land \forall w \in X (x C w < z \to f (x) D f (w) < \frac{d}{2})) \to \exists b \in MetOpen (C) (x \in b \land \exists p \in (X \times ℝ^{+}) (b = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2})))$
80	79	rexlimdva2	$⊢ (((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land x \in X) \to (\exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < \frac{d}{2}) \to \exists b \in MetOpen (C) (x \in b \land \exists p \in (X \times ℝ^{+}) (b = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2}))))$
81	80	ralimdva	$⊢ ((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \to (\forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < \frac{d}{2}) \to \forall x \in X \exists b \in MetOpen (C) (x \in b \land \exists p \in (X \times ℝ^{+}) (b = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2}))))$
82	81	imp	$⊢ (((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land \forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < \frac{d}{2})) \to \forall x \in X \exists b \in MetOpen (C) (x \in b \land \exists p \in (X \times ℝ^{+}) (b = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2})))$
83	26	mopnuni	$⊢ C \in ∞Met (X) \to X = ⋃ MetOpen (C)$
84	1 83	syl	$⊢ φ \to X = ⋃ MetOpen (C)$
85	84	raleqdv	$⊢ φ \to (\forall x \in X \exists b \in MetOpen (C) (x \in b \land \exists p \in (X \times ℝ^{+}) (b = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2}))) \leftrightarrow \forall x \in ⋃ MetOpen (C) \exists b \in MetOpen (C) (x \in b \land \exists p \in (X \times ℝ^{+}) (b = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2}))))$
86	85	ad3antrrr	$⊢ (((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land \forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < \frac{d}{2})) \to (\forall x \in X \exists b \in MetOpen (C) (x \in b \land \exists p \in (X \times ℝ^{+}) (b = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2}))) \leftrightarrow \forall x \in ⋃ MetOpen (C) \exists b \in MetOpen (C) (x \in b \land \exists p \in (X \times ℝ^{+}) (b = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2}))))$
87	82 86	mpbid	$⊢ (((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land \forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < \frac{d}{2})) \to \forall x \in ⋃ MetOpen (C) \exists b \in MetOpen (C) (x \in b \land \exists p \in (X \times ℝ^{+}) (b = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2})))$
88		eqid	$⊢ ⋃ MetOpen (C) = ⋃ MetOpen (C)$
89		fveq2	$⊢ p = g (b) \to 1^{st} (p) = 1^{st} (g (b))$
90		fveq2	$⊢ p = g (b) \to 2^{nd} (p) = 2^{nd} (g (b))$
91	89 90	oveq12d	$⊢ p = g (b) \to 1^{st} (p) ball (C) 2^{nd} (p) = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))$
92	91	eqeq2d	$⊢ p = g (b) \to (b = 1^{st} (p) ball (C) 2^{nd} (p) \leftrightarrow b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)))$
93	89	oveq1d	$⊢ p = g (b) \to 1^{st} (p) C c = 1^{st} (g (b)) C c$
94	90 90	oveq12d	$⊢ p = g (b) \to 2^{nd} (p) + 2^{nd} (p) = 2^{nd} (g (b)) + 2^{nd} (g (b))$
95	93 94	breq12d	$⊢ p = g (b) \to (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \leftrightarrow 1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)))$
96	89	fveq2d	$⊢ p = g (b) \to f (1^{st} (p)) = f (1^{st} (g (b)))$
97	96	oveq1d	$⊢ p = g (b) \to f (1^{st} (p)) D f (c) = f (1^{st} (g (b))) D f (c)$
98	97	breq1d	$⊢ p = g (b) \to (f (1^{st} (p)) D f (c) < \frac{d}{2} \leftrightarrow f (1^{st} (g (b))) D f (c) < \frac{d}{2})$
99	95 98	imbi12d	$⊢ p = g (b) \to ((1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2}) \leftrightarrow (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))$
100	99	ralbidv	$⊢ p = g (b) \to (\forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2}) \leftrightarrow \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))$
101	92 100	anbi12d	$⊢ p = g (b) \to ((b = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2})) \leftrightarrow (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2})))$
102	88 101	cmpcovf	$⊢ (MetOpen (C) \in Comp \land \forall x \in ⋃ MetOpen (C) \exists b \in MetOpen (C) (x \in b \land \exists p \in (X \times ℝ^{+}) (b = 1^{st} (p) ball (C) 2^{nd} (p) \land \forall c \in X (1^{st} (p) C c < 2^{nd} (p) + 2^{nd} (p) \to f (1^{st} (p)) D f (c) < \frac{d}{2})))) \to \exists s \in (𝒫 MetOpen (C) \cap Fin) (⋃ MetOpen (C) = ⋃ s \land \exists g (g : s ⟶ X \times ℝ^{+} \land \forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))))$
103	21 87 102	syl2anc	$⊢ (((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land \forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < \frac{d}{2})) \to \exists s \in (𝒫 MetOpen (C) \cap Fin) (⋃ MetOpen (C) = ⋃ s \land \exists g (g : s ⟶ X \times ℝ^{+} \land \forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))))$
104	103	ex	$⊢ ((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \to (\forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < \frac{d}{2}) \to \exists s \in (𝒫 MetOpen (C) \cap Fin) (⋃ MetOpen (C) = ⋃ s \land \exists g (g : s ⟶ X \times ℝ^{+} \land \forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2})))))$
105		elinel2	$⊢ s \in (𝒫 MetOpen (C) \cap Fin) \to s \in Fin$
106		simpll	$⊢ ((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \to φ$
107	106	anim1i	$⊢ (((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \to (φ \land s \in Fin)$
108		frn	$⊢ g : s ⟶ X \times ℝ^{+} \to ran g \subseteq X \times ℝ^{+}$
109		rnss	$⊢ ran g \subseteq X \times ℝ^{+} \to ran ran g \subseteq ran (X \times ℝ^{+})$
110	108 109	syl	$⊢ g : s ⟶ X \times ℝ^{+} \to ran ran g \subseteq ran (X \times ℝ^{+})$
111		rnxpss	$⊢ ran (X \times ℝ^{+}) \subseteq ℝ^{+}$
112	110 111	sstrdi	$⊢ g : s ⟶ X \times ℝ^{+} \to ran ran g \subseteq ℝ^{+}$
113	112	adantl	$⊢ (((φ \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \to ran ran g \subseteq ℝ^{+}$
114		simplr	$⊢ ((φ \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \to s \in Fin$
115		ffun	$⊢ g : s ⟶ X \times ℝ^{+} \to Fun g$
116		vex	$⊢ g \in V$
117	116	fundmen	$⊢ Fun g \to dom g \approx g$
118	117	ensymd	$⊢ Fun g \to g \approx dom g$
119	115 118	syl	$⊢ g : s ⟶ X \times ℝ^{+} \to g \approx dom g$
120		fdm	$⊢ g : s ⟶ X \times ℝ^{+} \to dom g = s$
121	119 120	breqtrd	$⊢ g : s ⟶ X \times ℝ^{+} \to g \approx s$
122		enfii	$⊢ (s \in Fin \land g \approx s) \to g \in Fin$
123	121 122	sylan2	$⊢ (s \in Fin \land g : s ⟶ X \times ℝ^{+}) \to g \in Fin$
124		rnfi	$⊢ g \in Fin \to ran g \in Fin$
125		rnfi	$⊢ ran g \in Fin \to ran ran g \in Fin$
126	123 124 125	3syl	$⊢ (s \in Fin \land g : s ⟶ X \times ℝ^{+}) \to ran ran g \in Fin$
127	114 126	sylan	$⊢ (((φ \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \to ran ran g \in Fin$
128	120	adantl	$⊢ ((φ \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \to dom g = s$
129		eqtr	$⊢ (X = ⋃ MetOpen (C) \land ⋃ MetOpen (C) = ⋃ s) \to X = ⋃ s$
130	84 129	sylan	$⊢ (φ \land ⋃ MetOpen (C) = ⋃ s) \to X = ⋃ s$
131	4	adantr	$⊢ (φ \land ⋃ MetOpen (C) = ⋃ s) \to X \neq \emptyset$
132	130 131	eqnetrrd	$⊢ (φ \land ⋃ MetOpen (C) = ⋃ s) \to ⋃ s \neq \emptyset$
133		unieq	$⊢ s = \emptyset \to ⋃ s = ⋃ \emptyset$
134		uni0	$⊢ ⋃ \emptyset = \emptyset$
135	133 134	eqtrdi	$⊢ s = \emptyset \to ⋃ s = \emptyset$
136	135	necon3i	$⊢ ⋃ s \neq \emptyset \to s \neq \emptyset$
137	132 136	syl	$⊢ (φ \land ⋃ MetOpen (C) = ⋃ s) \to s \neq \emptyset$
138	137	adantr	$⊢ ((φ \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \to s \neq \emptyset$
139	128 138	eqnetrd	$⊢ ((φ \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \to dom g \neq \emptyset$
140		dm0rn0	$⊢ dom g = \emptyset \leftrightarrow ran g = \emptyset$
141	140	necon3bii	$⊢ dom g \neq \emptyset \leftrightarrow ran g \neq \emptyset$
142	139 141	sylib	$⊢ ((φ \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \to ran g \neq \emptyset$
143		relxp	$⊢ Rel (X \times ℝ^{+})$
144		relss	$⊢ ran g \subseteq X \times ℝ^{+} \to (Rel (X \times ℝ^{+}) \to Rel ran g)$
145	108 143 144	mpisyl	$⊢ g : s ⟶ X \times ℝ^{+} \to Rel ran g$
146		relrn0	$⊢ Rel ran g \to (ran g = \emptyset \leftrightarrow ran ran g = \emptyset)$
147	146	necon3bid	$⊢ Rel ran g \to (ran g \neq \emptyset \leftrightarrow ran ran g \neq \emptyset)$
148	145 147	syl	$⊢ g : s ⟶ X \times ℝ^{+} \to (ran g \neq \emptyset \leftrightarrow ran ran g \neq \emptyset)$
149	148	adantl	$⊢ ((φ \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \to (ran g \neq \emptyset \leftrightarrow ran ran g \neq \emptyset)$
150	142 149	mpbid	$⊢ ((φ \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \to ran ran g \neq \emptyset$
151	150	adantllr	$⊢ (((φ \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \to ran ran g \neq \emptyset$
152		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
153	113 152	sstrdi	$⊢ (((φ \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \to ran ran g \subseteq ℝ$
154		ltso	$⊢ < Or ℝ$
155		fiinfcl	$⊢ (< Or ℝ \land (ran ran g \in Fin \land ran ran g \neq \emptyset \land ran ran g \subseteq ℝ)) \to sup (ran ran g ℝ <) \in ran ran g$
156	154 155	mpan	$⊢ (ran ran g \in Fin \land ran ran g \neq \emptyset \land ran ran g \subseteq ℝ) \to sup (ran ran g ℝ <) \in ran ran g$
157	127 151 153 156	syl3anc	$⊢ (((φ \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \to sup (ran ran g ℝ <) \in ran ran g$
158	113 157	sseldd	$⊢ (((φ \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \to sup (ran ran g ℝ <) \in ℝ^{+}$
159	107 158	sylanl1	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \to sup (ran ran g ℝ <) \in ℝ^{+}$
160	159	adantr	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \land \forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))) \to sup (ran ran g ℝ <) \in ℝ^{+}$
161	84	ad3antrrr	$⊢ (((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \to X = ⋃ MetOpen (C)$
162	161	anim1i	$⊢ ((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \to (X = ⋃ MetOpen (C) \land ⋃ MetOpen (C) = ⋃ s)$
163	162	ad2antrr	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \land \forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))) \to (X = ⋃ MetOpen (C) \land ⋃ MetOpen (C) = ⋃ s)$
164		simpl	$⊢ (x \in X \land w \in X) \to x \in X$
165	129	eleq2d	$⊢ (X = ⋃ MetOpen (C) \land ⋃ MetOpen (C) = ⋃ s) \to (x \in X \leftrightarrow x \in ⋃ s)$
166		eluni2	$⊢ x \in ⋃ s \leftrightarrow \exists b \in s x \in b$
167	165 166	bitrdi	$⊢ (X = ⋃ MetOpen (C) \land ⋃ MetOpen (C) = ⋃ s) \to (x \in X \leftrightarrow \exists b \in s x \in b)$
168	167	biimpa	$⊢ ((X = ⋃ MetOpen (C) \land ⋃ MetOpen (C) = ⋃ s) \land x \in X) \to \exists b \in s x \in b$
169	163 164 168	syl2an	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \land \forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))) \land (x \in X \land w \in X)) \to \exists b \in s x \in b$
170		nfv	$⊢ Ⅎ b (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+})$
171		nfra1	$⊢ Ⅎ b \forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))$
172	170 171	nfan	$⊢ Ⅎ b ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \land \forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2})))$
173		nfv	$⊢ Ⅎ b (x \in X \land w \in X)$
174	172 173	nfan	$⊢ Ⅎ b (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \land \forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))) \land (x \in X \land w \in X))$
175		nfv	$⊢ Ⅎ b (x C w < sup (ran ran g ℝ <) \to f (x) D f (w) < d)$
176		rspa	$⊢ (\forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2})) \land b \in s) \to (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))$
177		oveq2	$⊢ c = x \to 1^{st} (g (b)) C c = 1^{st} (g (b)) C x$
178	177	breq1d	$⊢ c = x \to (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \leftrightarrow 1^{st} (g (b)) C x < 2^{nd} (g (b)) + 2^{nd} (g (b)))$
179		fveq2	$⊢ c = x \to f (c) = f (x)$
180	179	oveq2d	$⊢ c = x \to f (1^{st} (g (b))) D f (c) = f (1^{st} (g (b))) D f (x)$
181	180	breq1d	$⊢ c = x \to (f (1^{st} (g (b))) D f (c) < \frac{d}{2} \leftrightarrow f (1^{st} (g (b))) D f (x) < \frac{d}{2})$
182	178 181	imbi12d	$⊢ c = x \to ((1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}) \leftrightarrow (1^{st} (g (b)) C x < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (x) < \frac{d}{2}))$
183	182	rspcva	$⊢ (x \in X \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2})) \to (1^{st} (g (b)) C x < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (x) < \frac{d}{2})$
184		oveq2	$⊢ c = w \to 1^{st} (g (b)) C c = 1^{st} (g (b)) C w$
185	184	breq1d	$⊢ c = w \to (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \leftrightarrow 1^{st} (g (b)) C w < 2^{nd} (g (b)) + 2^{nd} (g (b)))$
186	47	oveq2d	$⊢ c = w \to f (1^{st} (g (b))) D f (c) = f (1^{st} (g (b))) D f (w)$
187	186	breq1d	$⊢ c = w \to (f (1^{st} (g (b))) D f (c) < \frac{d}{2} \leftrightarrow f (1^{st} (g (b))) D f (w) < \frac{d}{2})$
188	185 187	imbi12d	$⊢ c = w \to ((1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}) \leftrightarrow (1^{st} (g (b)) C w < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (w) < \frac{d}{2}))$
189	188	rspcva	$⊢ (w \in X \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2})) \to (1^{st} (g (b)) C w < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (w) < \frac{d}{2})$
190	183 189	anim12i	$⊢ ((x \in X \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2})) \land (w \in X \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))) \to ((1^{st} (g (b)) C x < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (x) < \frac{d}{2}) \land (1^{st} (g (b)) C w < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (w) < \frac{d}{2}))$
191	190	anandirs	$⊢ ((x \in X \land w \in X) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2})) \to ((1^{st} (g (b)) C x < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (x) < \frac{d}{2}) \land (1^{st} (g (b)) C w < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (w) < \frac{d}{2}))$
192		anim12	$⊢ ((1^{st} (g (b)) C x < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (x) < \frac{d}{2}) \land (1^{st} (g (b)) C w < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (w) < \frac{d}{2})) \to ((1^{st} (g (b)) C x < 2^{nd} (g (b)) + 2^{nd} (g (b)) \land 1^{st} (g (b)) C w < 2^{nd} (g (b)) + 2^{nd} (g (b))) \to (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2}))$
193	191 192	syl	$⊢ ((x \in X \land w \in X) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2})) \to ((1^{st} (g (b)) C x < 2^{nd} (g (b)) + 2^{nd} (g (b)) \land 1^{st} (g (b)) C w < 2^{nd} (g (b)) + 2^{nd} (g (b))) \to (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2}))$
194	193	adantrl	$⊢ ((x \in X \land w \in X) \land (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))) \to ((1^{st} (g (b)) C x < 2^{nd} (g (b)) + 2^{nd} (g (b)) \land 1^{st} (g (b)) C w < 2^{nd} (g (b)) + 2^{nd} (g (b))) \to (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2}))$
195	194	ad4ant23	$⊢ ((((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))) \land (b \in s \land x \in b)) \to ((1^{st} (g (b)) C x < 2^{nd} (g (b)) + 2^{nd} (g (b)) \land 1^{st} (g (b)) C w < 2^{nd} (g (b)) + 2^{nd} (g (b))) \to (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2}))$
196		simpll	$⊢ ((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \to ((φ \land f : X ⟶ Y) \land d \in ℝ^{+})$
197	196	anim1i	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \to (((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+})$
198	197	anim1i	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \to ((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X))$
199	112 152	sstrdi	$⊢ g : s ⟶ X \times ℝ^{+} \to ran ran g \subseteq ℝ$
200	199	adantr	$⊢ (g : s ⟶ X \times ℝ^{+} \land b \in s) \to ran ran g \subseteq ℝ$
201		0re	$⊢ 0 \in ℝ$
202		rpge0	$⊢ y \in ℝ^{+} \to 0 \leq y$
203	202	rgen	$⊢ \forall y \in ℝ^{+} 0 \leq y$
204		ssralv	$⊢ ran ran g \subseteq ℝ^{+} \to (\forall y \in ℝ^{+} 0 \leq y \to \forall y \in ran ran g 0 \leq y)$
205	112 203 204	mpisyl	$⊢ g : s ⟶ X \times ℝ^{+} \to \forall y \in ran ran g 0 \leq y$
206		breq1	$⊢ x = 0 \to (x \leq y \leftrightarrow 0 \leq y)$
207	206	ralbidv	$⊢ x = 0 \to (\forall y \in ran ran g x \leq y \leftrightarrow \forall y \in ran ran g 0 \leq y)$
208	207	rspcev	$⊢ (0 \in ℝ \land \forall y \in ran ran g 0 \leq y) \to \exists x \in ℝ \forall y \in ran ran g x \leq y$
209	201 205 208	sylancr	$⊢ g : s ⟶ X \times ℝ^{+} \to \exists x \in ℝ \forall y \in ran ran g x \leq y$
210	209	adantr	$⊢ (g : s ⟶ X \times ℝ^{+} \land b \in s) \to \exists x \in ℝ \forall y \in ran ran g x \leq y$
211	145	adantr	$⊢ (g : s ⟶ X \times ℝ^{+} \land b \in s) \to Rel ran g$
212		ffn	$⊢ g : s ⟶ X \times ℝ^{+} \to g Fn s$
213		fnfvelrn	$⊢ (g Fn s \land b \in s) \to g (b) \in ran g$
214	212 213	sylan	$⊢ (g : s ⟶ X \times ℝ^{+} \land b \in s) \to g (b) \in ran g$
215		2ndrn	$⊢ (Rel ran g \land g (b) \in ran g) \to 2^{nd} (g (b)) \in ran ran g$
216	211 214 215	syl2anc	$⊢ (g : s ⟶ X \times ℝ^{+} \land b \in s) \to 2^{nd} (g (b)) \in ran ran g$
217		infrelb	$⊢ (ran ran g \subseteq ℝ \land \exists x \in ℝ \forall y \in ran ran g x \leq y \land 2^{nd} (g (b)) \in ran ran g) \to sup (ran ran g ℝ <) \leq 2^{nd} (g (b))$
218	200 210 216 217	syl3anc	$⊢ (g : s ⟶ X \times ℝ^{+} \land b \in s) \to sup (ran ran g ℝ <) \leq 2^{nd} (g (b))$
219	218	adantll	$⊢ ((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land b \in s) \to sup (ran ran g ℝ <) \leq 2^{nd} (g (b))$
220	219	ad2ant2r	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land (b \in s \land x \in b)) \to sup (ran ran g ℝ <) \leq 2^{nd} (g (b))$
221	1	ad3antrrr	$⊢ (((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \to C \in ∞Met (X)$
222		xmetcl	$⊢ (C \in ∞Met (X) \land x \in X \land w \in X) \to x C w \in ℝ^{*}$
223	222	3expb	$⊢ (C \in ∞Met (X) \land (x \in X \land w \in X)) \to x C w \in ℝ^{*}$
224	221 223	sylan	$⊢ ((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \to x C w \in ℝ^{*}$
225	224	adantr	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land (b \in s \land x \in b)) \to x C w \in ℝ^{*}$
226		simplr	$⊢ ((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \to g : s ⟶ X \times ℝ^{+}$
227		simpl	$⊢ (b \in s \land x \in b) \to b \in s$
228	216	ne0d	$⊢ (g : s ⟶ X \times ℝ^{+} \land b \in s) \to ran ran g \neq \emptyset$
229		infrecl	$⊢ (ran ran g \subseteq ℝ \land ran ran g \neq \emptyset \land \exists x \in ℝ \forall y \in ran ran g x \leq y) \to sup (ran ran g ℝ <) \in ℝ$
230	200 228 210 229	syl3anc	$⊢ (g : s ⟶ X \times ℝ^{+} \land b \in s) \to sup (ran ran g ℝ <) \in ℝ$
231	230	rexrd	$⊢ (g : s ⟶ X \times ℝ^{+} \land b \in s) \to sup (ran ran g ℝ <) \in ℝ^{*}$
232	226 227 231	syl2an	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land (b \in s \land x \in b)) \to sup (ran ran g ℝ <) \in ℝ^{*}$
233		simpr	$⊢ (((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \to g : s ⟶ X \times ℝ^{+}$
234	233	ffvelrnda	$⊢ ((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land b \in s) \to g (b) \in (X \times ℝ^{+})$
235		xp2nd	$⊢ g (b) \in (X \times ℝ^{+}) \to 2^{nd} (g (b)) \in ℝ^{+}$
236	234 235	syl	$⊢ ((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land b \in s) \to 2^{nd} (g (b)) \in ℝ^{+}$
237	236	rpxrd	$⊢ ((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land b \in s) \to 2^{nd} (g (b)) \in ℝ^{*}$
238	237	ad2ant2r	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land (b \in s \land x \in b)) \to 2^{nd} (g (b)) \in ℝ^{*}$
239		xrltletr	$⊢ (x C w \in ℝ^{} \land sup (ran ran g ℝ <) \in ℝ^{} \land 2^{nd} (g (b)) \in ℝ^{*}) \to ((x C w < sup (ran ran g ℝ <) \land sup (ran ran g ℝ <) \leq 2^{nd} (g (b))) \to x C w < 2^{nd} (g (b)))$
240	225 232 238 239	syl3anc	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land (b \in s \land x \in b)) \to ((x C w < sup (ran ran g ℝ <) \land sup (ran ran g ℝ <) \leq 2^{nd} (g (b))) \to x C w < 2^{nd} (g (b)))$
241	220 240	mpan2d	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land (b \in s \land x \in b)) \to (x C w < sup (ran ran g ℝ <) \to x C w < 2^{nd} (g (b)))$
242	241	adantlr	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to (x C w < sup (ran ran g ℝ <) \to x C w < 2^{nd} (g (b)))$
243	1	ad6antr	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to C \in ∞Met (X)$
244		simpllr	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \to g : s ⟶ X \times ℝ^{+}$
245		ffvelrn	$⊢ (g : s ⟶ X \times ℝ^{+} \land b \in s) \to g (b) \in (X \times ℝ^{+})$
246		xp1st	$⊢ g (b) \in (X \times ℝ^{+}) \to 1^{st} (g (b)) \in X$
247	245 246	syl	$⊢ (g : s ⟶ X \times ℝ^{+} \land b \in s) \to 1^{st} (g (b)) \in X$
248	244 227 247	syl2an	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to 1^{st} (g (b)) \in X$
249		simpr	$⊢ (x \in X \land w \in X) \to w \in X$
250	249	ad3antlr	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to w \in X$
251		xmetcl	$⊢ (C \in ∞Met (X) \land 1^{st} (g (b)) \in X \land w \in X) \to 1^{st} (g (b)) C w \in ℝ^{*}$
252	243 248 250 251	syl3anc	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to 1^{st} (g (b)) C w \in ℝ^{*}$
253	252	adantr	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land x C w < 2^{nd} (g (b))) \to 1^{st} (g (b)) C w \in ℝ^{*}$
254	245 235	syl	$⊢ (g : s ⟶ X \times ℝ^{+} \land b \in s) \to 2^{nd} (g (b)) \in ℝ^{+}$
255	226 254	sylan	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to 2^{nd} (g (b)) \in ℝ^{+}$
256	255	ad2ant2r	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to 2^{nd} (g (b)) \in ℝ^{+}$
257	256	rpred	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to 2^{nd} (g (b)) \in ℝ$
258	164	ad3antlr	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to x \in X$
259		xmetcl	$⊢ (C \in ∞Met (X) \land 1^{st} (g (b)) \in X \land x \in X) \to 1^{st} (g (b)) C x \in ℝ^{*}$
260	243 248 258 259	syl3anc	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to 1^{st} (g (b)) C x \in ℝ^{*}$
261	254	rpxrd	$⊢ (g : s ⟶ X \times ℝ^{+} \land b \in s) \to 2^{nd} (g (b)) \in ℝ^{*}$
262	244 227 261	syl2an	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to 2^{nd} (g (b)) \in ℝ^{*}$
263		eleq2	$⊢ b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \to (x \in b \leftrightarrow x \in (1^{st} (g (b)) ball (C) 2^{nd} (g (b))))$
264	1	ad5antr	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to C \in ∞Met (X)$
265	226 247	sylan	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to 1^{st} (g (b)) \in X$
266	255	rpxrd	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to 2^{nd} (g (b)) \in ℝ^{*}$
267		elbl	$⊢ (C \in ∞Met (X) \land 1^{st} (g (b)) \in X \land 2^{nd} (g (b)) \in ℝ^{*}) \to (x \in (1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \leftrightarrow (x \in X \land 1^{st} (g (b)) C x < 2^{nd} (g (b))))$
268	264 265 266 267	syl3anc	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to (x \in (1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \leftrightarrow (x \in X \land 1^{st} (g (b)) C x < 2^{nd} (g (b))))$
269	263 268	sylan9bbr	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \to (x \in b \leftrightarrow (x \in X \land 1^{st} (g (b)) C x < 2^{nd} (g (b))))$
270	269	biimpd	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \to (x \in b \to (x \in X \land 1^{st} (g (b)) C x < 2^{nd} (g (b))))$
271	270	an32s	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land b \in s) \to (x \in b \to (x \in X \land 1^{st} (g (b)) C x < 2^{nd} (g (b))))$
272	271	impr	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to (x \in X \land 1^{st} (g (b)) C x < 2^{nd} (g (b)))$
273	272	simprd	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to 1^{st} (g (b)) C x < 2^{nd} (g (b))$
274	260 262 273	xrltled	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to 1^{st} (g (b)) C x \leq 2^{nd} (g (b))$
275	226	ffvelrnda	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to g (b) \in (X \times ℝ^{+})$
276	275 246	syl	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to 1^{st} (g (b)) \in X$
277		simplrl	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to x \in X$
278	264 276 277 259	syl3anc	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to 1^{st} (g (b)) C x \in ℝ^{*}$
279		xmetge0	$⊢ (C \in ∞Met (X) \land 1^{st} (g (b)) \in X \land x \in X) \to 0 \leq 1^{st} (g (b)) C x$
280	264 276 277 279	syl3anc	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to 0 \leq 1^{st} (g (b)) C x$
281		xrrege0	$⊢ ((1^{st} (g (b)) C x \in ℝ^{*} \land 2^{nd} (g (b)) \in ℝ) \land (0 \leq 1^{st} (g (b)) C x \land 1^{st} (g (b)) C x \leq 2^{nd} (g (b)))) \to 1^{st} (g (b)) C x \in ℝ$
282	281	an4s	$⊢ ((1^{st} (g (b)) C x \in ℝ^{*} \land 0 \leq 1^{st} (g (b)) C x) \land (2^{nd} (g (b)) \in ℝ \land 1^{st} (g (b)) C x \leq 2^{nd} (g (b)))) \to 1^{st} (g (b)) C x \in ℝ$
283	282	ex	$⊢ (1^{st} (g (b)) C x \in ℝ^{*} \land 0 \leq 1^{st} (g (b)) C x) \to ((2^{nd} (g (b)) \in ℝ \land 1^{st} (g (b)) C x \leq 2^{nd} (g (b))) \to 1^{st} (g (b)) C x \in ℝ)$
284	278 280 283	syl2anc	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to ((2^{nd} (g (b)) \in ℝ \land 1^{st} (g (b)) C x \leq 2^{nd} (g (b))) \to 1^{st} (g (b)) C x \in ℝ)$
285	284	ad2ant2r	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to ((2^{nd} (g (b)) \in ℝ \land 1^{st} (g (b)) C x \leq 2^{nd} (g (b))) \to 1^{st} (g (b)) C x \in ℝ)$
286	257 274 285	mp2and	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to 1^{st} (g (b)) C x \in ℝ$
287	286	adantr	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land x C w < 2^{nd} (g (b))) \to 1^{st} (g (b)) C x \in ℝ$
288		xrltle	$⊢ (x C w \in ℝ^{} \land 2^{nd} (g (b)) \in ℝ^{}) \to (x C w < 2^{nd} (g (b)) \to x C w \leq 2^{nd} (g (b)))$
289	225 238 288	syl2anc	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land (b \in s \land x \in b)) \to (x C w < 2^{nd} (g (b)) \to x C w \leq 2^{nd} (g (b)))$
290		xmetge0	$⊢ (C \in ∞Met (X) \land x \in X \land w \in X) \to 0 \leq x C w$
291	290	3expb	$⊢ (C \in ∞Met (X) \land (x \in X \land w \in X)) \to 0 \leq x C w$
292	221 291	sylan	$⊢ ((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \to 0 \leq x C w$
293	292	adantr	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land (b \in s \land x \in b)) \to 0 \leq x C w$
294	236	rpred	$⊢ ((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land b \in s) \to 2^{nd} (g (b)) \in ℝ$
295	294	ad2ant2r	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land (b \in s \land x \in b)) \to 2^{nd} (g (b)) \in ℝ$
296		xrrege0	$⊢ ((x C w \in ℝ^{*} \land 2^{nd} (g (b)) \in ℝ) \land (0 \leq x C w \land x C w \leq 2^{nd} (g (b)))) \to x C w \in ℝ$
297	296	ex	$⊢ (x C w \in ℝ^{*} \land 2^{nd} (g (b)) \in ℝ) \to ((0 \leq x C w \land x C w \leq 2^{nd} (g (b))) \to x C w \in ℝ)$
298	225 295 297	syl2anc	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land (b \in s \land x \in b)) \to ((0 \leq x C w \land x C w \leq 2^{nd} (g (b))) \to x C w \in ℝ)$
299	293 298	mpand	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land (b \in s \land x \in b)) \to (x C w \leq 2^{nd} (g (b)) \to x C w \in ℝ)$
300	289 299	syld	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land (b \in s \land x \in b)) \to (x C w < 2^{nd} (g (b)) \to x C w \in ℝ)$
301	300	adantlr	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to (x C w < 2^{nd} (g (b)) \to x C w \in ℝ)$
302	301	imp	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land x C w < 2^{nd} (g (b))) \to x C w \in ℝ$
303	287 302	readdcld	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land x C w < 2^{nd} (g (b))) \to (1^{st} (g (b)) C x) + (x C w) \in ℝ$
304	303	rexrd	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land x C w < 2^{nd} (g (b))) \to (1^{st} (g (b)) C x) + (x C w) \in ℝ^{*}$
305	256 256	rpaddcld	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to 2^{nd} (g (b)) + 2^{nd} (g (b)) \in ℝ^{+}$
306	305	rpxrd	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to 2^{nd} (g (b)) + 2^{nd} (g (b)) \in ℝ^{*}$
307	306	adantr	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land x C w < 2^{nd} (g (b))) \to 2^{nd} (g (b)) + 2^{nd} (g (b)) \in ℝ^{*}$
308		xmettri	$⊢ (C \in ∞Met (X) \land (1^{st} (g (b)) \in X \land w \in X \land x \in X)) \to 1^{st} (g (b)) C w \leq (1^{st} (g (b)) C x) +_{𝑒} (x C w)$
309	243 248 250 258 308	syl13anc	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to 1^{st} (g (b)) C w \leq (1^{st} (g (b)) C x) +_{𝑒} (x C w)$
310	309	adantr	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land x C w < 2^{nd} (g (b))) \to 1^{st} (g (b)) C w \leq (1^{st} (g (b)) C x) +_{𝑒} (x C w)$
311		rexadd	$⊢ (1^{st} (g (b)) C x \in ℝ \land x C w \in ℝ) \to (1^{st} (g (b)) C x) +_{𝑒} (x C w) = (1^{st} (g (b)) C x) + (x C w)$
312	287 302 311	syl2anc	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land x C w < 2^{nd} (g (b))) \to (1^{st} (g (b)) C x) +_{𝑒} (x C w) = (1^{st} (g (b)) C x) + (x C w)$
313	310 312	breqtrd	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land x C w < 2^{nd} (g (b))) \to 1^{st} (g (b)) C w \leq (1^{st} (g (b)) C x) + (x C w)$
314	257	adantr	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land x C w < 2^{nd} (g (b))) \to 2^{nd} (g (b)) \in ℝ$
315	273	adantr	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land x C w < 2^{nd} (g (b))) \to 1^{st} (g (b)) C x < 2^{nd} (g (b))$
316		simpr	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land x C w < 2^{nd} (g (b))) \to x C w < 2^{nd} (g (b))$
317	287 302 314 314 315 316	lt2addd	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land x C w < 2^{nd} (g (b))) \to (1^{st} (g (b)) C x) + (x C w) < 2^{nd} (g (b)) + 2^{nd} (g (b))$
318	253 304 307 313 317	xrlelttrd	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land x C w < 2^{nd} (g (b))) \to 1^{st} (g (b)) C w < 2^{nd} (g (b)) + 2^{nd} (g (b))$
319	318	ex	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to (x C w < 2^{nd} (g (b)) \to 1^{st} (g (b)) C w < 2^{nd} (g (b)) + 2^{nd} (g (b)))$
320	254	rpred	$⊢ (g : s ⟶ X \times ℝ^{+} \land b \in s) \to 2^{nd} (g (b)) \in ℝ$
321	320 254	ltaddrpd	$⊢ (g : s ⟶ X \times ℝ^{+} \land b \in s) \to 2^{nd} (g (b)) < 2^{nd} (g (b)) + 2^{nd} (g (b))$
322	244 227 321	syl2an	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to 2^{nd} (g (b)) < 2^{nd} (g (b)) + 2^{nd} (g (b))$
323	260 262 306 273 322	xrlttrd	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to 1^{st} (g (b)) C x < 2^{nd} (g (b)) + 2^{nd} (g (b))$
324	319 323	jctild	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to (x C w < 2^{nd} (g (b)) \to (1^{st} (g (b)) C x < 2^{nd} (g (b)) + 2^{nd} (g (b)) \land 1^{st} (g (b)) C w < 2^{nd} (g (b)) + 2^{nd} (g (b))))$
325	242 324	syld	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to (x C w < sup (ran ran g ℝ <) \to (1^{st} (g (b)) C x < 2^{nd} (g (b)) + 2^{nd} (g (b)) \land 1^{st} (g (b)) C w < 2^{nd} (g (b)) + 2^{nd} (g (b))))$
326		simpll	$⊢ (((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \to (φ \land f : X ⟶ Y)$
327		ffvelrn	$⊢ (f : X ⟶ Y \land x \in X) \to f (x) \in Y$
328		ffvelrn	$⊢ (f : X ⟶ Y \land w \in X) \to f (w) \in Y$
329	327 328	anim12dan	$⊢ (f : X ⟶ Y \land (x \in X \land w \in X)) \to (f (x) \in Y \land f (w) \in Y)$
330		xmetcl	$⊢ (D \in ∞Met (Y) \land f (x) \in Y \land f (w) \in Y) \to f (x) D f (w) \in ℝ^{*}$
331	330	3expb	$⊢ (D \in ∞Met (Y) \land (f (x) \in Y \land f (w) \in Y)) \to f (x) D f (w) \in ℝ^{*}$
332	2 329 331	syl2an	$⊢ (φ \land (f : X ⟶ Y \land (x \in X \land w \in X))) \to f (x) D f (w) \in ℝ^{*}$
333	332	anassrs	$⊢ ((φ \land f : X ⟶ Y) \land (x \in X \land w \in X)) \to f (x) D f (w) \in ℝ^{*}$
334	326 333	sylan	$⊢ ((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \to f (x) D f (w) \in ℝ^{*}$
335	334	ad3antrrr	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2})) \to f (x) D f (w) \in ℝ^{*}$
336	2	ad5antr	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to D \in ∞Met (Y)$
337		simp-5r	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to f : X ⟶ Y$
338	337 276	ffvelrnd	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to f (1^{st} (g (b))) \in Y$
339		simpllr	$⊢ (((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \to f : X ⟶ Y$
340	339	ffvelrnda	$⊢ ((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land x \in X) \to f (x) \in Y$
341	340	adantrr	$⊢ ((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \to f (x) \in Y$
342	341	adantr	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to f (x) \in Y$
343		xmetcl	$⊢ (D \in ∞Met (Y) \land f (1^{st} (g (b))) \in Y \land f (x) \in Y) \to f (1^{st} (g (b))) D f (x) \in ℝ^{*}$
344	336 338 342 343	syl3anc	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to f (1^{st} (g (b))) D f (x) \in ℝ^{*}$
345	14	rpxrd	$⊢ d \in ℝ^{+} \to \frac{d}{2} \in ℝ^{*}$
346	345	ad4antlr	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to \frac{d}{2} \in ℝ^{*}$
347		xrltle	$⊢ (f (1^{st} (g (b))) D f (x) \in ℝ^{} \land \frac{d}{2} \in ℝ^{}) \to (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \to f (1^{st} (g (b))) D f (x) \leq \frac{d}{2})$
348	344 346 347	syl2anc	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \to f (1^{st} (g (b))) D f (x) \leq \frac{d}{2})$
349		xmetge0	$⊢ (D \in ∞Met (Y) \land f (1^{st} (g (b))) \in Y \land f (x) \in Y) \to 0 \leq f (1^{st} (g (b))) D f (x)$
350	336 338 342 349	syl3anc	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to 0 \leq f (1^{st} (g (b))) D f (x)$
351	14	rpred	$⊢ d \in ℝ^{+} \to \frac{d}{2} \in ℝ$
352	351	ad4antlr	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to \frac{d}{2} \in ℝ$
353		xrrege0	$⊢ ((f (1^{st} (g (b))) D f (x) \in ℝ^{*} \land \frac{d}{2} \in ℝ) \land (0 \leq f (1^{st} (g (b))) D f (x) \land f (1^{st} (g (b))) D f (x) \leq \frac{d}{2})) \to f (1^{st} (g (b))) D f (x) \in ℝ$
354	353	ex	$⊢ (f (1^{st} (g (b))) D f (x) \in ℝ^{*} \land \frac{d}{2} \in ℝ) \to ((0 \leq f (1^{st} (g (b))) D f (x) \land f (1^{st} (g (b))) D f (x) \leq \frac{d}{2}) \to f (1^{st} (g (b))) D f (x) \in ℝ)$
355	344 352 354	syl2anc	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to ((0 \leq f (1^{st} (g (b))) D f (x) \land f (1^{st} (g (b))) D f (x) \leq \frac{d}{2}) \to f (1^{st} (g (b))) D f (x) \in ℝ)$
356	350 355	mpand	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to (f (1^{st} (g (b))) D f (x) \leq \frac{d}{2} \to f (1^{st} (g (b))) D f (x) \in ℝ)$
357	348 356	syld	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \to f (1^{st} (g (b))) D f (x) \in ℝ)$
358	357	ad2ant2r	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \to f (1^{st} (g (b))) D f (x) \in ℝ)$
359	358	imp	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land f (1^{st} (g (b))) D f (x) < \frac{d}{2}) \to f (1^{st} (g (b))) D f (x) \in ℝ$
360	339	ffvelrnda	$⊢ ((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land w \in X) \to f (w) \in Y$
361	360	adantrl	$⊢ ((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \to f (w) \in Y$
362	361	adantr	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to f (w) \in Y$
363		xmetcl	$⊢ (D \in ∞Met (Y) \land f (1^{st} (g (b))) \in Y \land f (w) \in Y) \to f (1^{st} (g (b))) D f (w) \in ℝ^{*}$
364	336 338 362 363	syl3anc	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to f (1^{st} (g (b))) D f (w) \in ℝ^{*}$
365		xrltle	$⊢ (f (1^{st} (g (b))) D f (w) \in ℝ^{} \land \frac{d}{2} \in ℝ^{}) \to (f (1^{st} (g (b))) D f (w) < \frac{d}{2} \to f (1^{st} (g (b))) D f (w) \leq \frac{d}{2})$
366	364 346 365	syl2anc	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to (f (1^{st} (g (b))) D f (w) < \frac{d}{2} \to f (1^{st} (g (b))) D f (w) \leq \frac{d}{2})$
367		xmetge0	$⊢ (D \in ∞Met (Y) \land f (1^{st} (g (b))) \in Y \land f (w) \in Y) \to 0 \leq f (1^{st} (g (b))) D f (w)$
368	336 338 362 367	syl3anc	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to 0 \leq f (1^{st} (g (b))) D f (w)$
369		xrrege0	$⊢ ((f (1^{st} (g (b))) D f (w) \in ℝ^{*} \land \frac{d}{2} \in ℝ) \land (0 \leq f (1^{st} (g (b))) D f (w) \land f (1^{st} (g (b))) D f (w) \leq \frac{d}{2})) \to f (1^{st} (g (b))) D f (w) \in ℝ$
370	369	ex	$⊢ (f (1^{st} (g (b))) D f (w) \in ℝ^{*} \land \frac{d}{2} \in ℝ) \to ((0 \leq f (1^{st} (g (b))) D f (w) \land f (1^{st} (g (b))) D f (w) \leq \frac{d}{2}) \to f (1^{st} (g (b))) D f (w) \in ℝ)$
371	364 352 370	syl2anc	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to ((0 \leq f (1^{st} (g (b))) D f (w) \land f (1^{st} (g (b))) D f (w) \leq \frac{d}{2}) \to f (1^{st} (g (b))) D f (w) \in ℝ)$
372	368 371	mpand	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to (f (1^{st} (g (b))) D f (w) \leq \frac{d}{2} \to f (1^{st} (g (b))) D f (w) \in ℝ)$
373	366 372	syld	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to (f (1^{st} (g (b))) D f (w) < \frac{d}{2} \to f (1^{st} (g (b))) D f (w) \in ℝ)$
374	373	ad2ant2r	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to (f (1^{st} (g (b))) D f (w) < \frac{d}{2} \to f (1^{st} (g (b))) D f (w) \in ℝ)$
375	374	imp	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land f (1^{st} (g (b))) D f (w) < \frac{d}{2}) \to f (1^{st} (g (b))) D f (w) \in ℝ$
376		readdcl	$⊢ (f (1^{st} (g (b))) D f (x) \in ℝ \land f (1^{st} (g (b))) D f (w) \in ℝ) \to (f (1^{st} (g (b))) D f (x)) + (f (1^{st} (g (b))) D f (w)) \in ℝ$
377	359 375 376	syl2an	$⊢ ((((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land f (1^{st} (g (b))) D f (x) < \frac{d}{2}) \land (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land f (1^{st} (g (b))) D f (w) < \frac{d}{2})) \to (f (1^{st} (g (b))) D f (x)) + (f (1^{st} (g (b))) D f (w)) \in ℝ$
378	377	anandis	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2})) \to (f (1^{st} (g (b))) D f (x)) + (f (1^{st} (g (b))) D f (w)) \in ℝ$
379	378	rexrd	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2})) \to (f (1^{st} (g (b))) D f (x)) + (f (1^{st} (g (b))) D f (w)) \in ℝ^{*}$
380		rpxr	$⊢ d \in ℝ^{+} \to d \in ℝ^{*}$
381	380	ad6antlr	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2})) \to d \in ℝ^{*}$
382		xmettri	$⊢ (D \in ∞Met (Y) \land (f (x) \in Y \land f (w) \in Y \land f (1^{st} (g (b))) \in Y)) \to f (x) D f (w) \leq (f (x) D f (1^{st} (g (b)))) +_{𝑒} (f (1^{st} (g (b))) D f (w))$
383	336 342 362 338 382	syl13anc	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to f (x) D f (w) \leq (f (x) D f (1^{st} (g (b)))) +_{𝑒} (f (1^{st} (g (b))) D f (w))$
384	383	ad2ant2r	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to f (x) D f (w) \leq (f (x) D f (1^{st} (g (b)))) +_{𝑒} (f (1^{st} (g (b))) D f (w))$
385	384	adantr	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2})) \to f (x) D f (w) \leq (f (x) D f (1^{st} (g (b)))) +_{𝑒} (f (1^{st} (g (b))) D f (w))$
386		xmetsym	$⊢ (D \in ∞Met (Y) \land f (x) \in Y \land f (1^{st} (g (b))) \in Y) \to f (x) D f (1^{st} (g (b))) = f (1^{st} (g (b))) D f (x)$
387	336 342 338 386	syl3anc	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to f (x) D f (1^{st} (g (b))) = f (1^{st} (g (b))) D f (x)$
388	387	ad2ant2r	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to f (x) D f (1^{st} (g (b))) = f (1^{st} (g (b))) D f (x)$
389	388	adantr	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2})) \to f (x) D f (1^{st} (g (b))) = f (1^{st} (g (b))) D f (x)$
390	389	oveq1d	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2})) \to (f (x) D f (1^{st} (g (b)))) +_{𝑒} (f (1^{st} (g (b))) D f (w)) = (f (1^{st} (g (b))) D f (x)) +_{𝑒} (f (1^{st} (g (b))) D f (w))$
391		rexadd	$⊢ (f (1^{st} (g (b))) D f (x) \in ℝ \land f (1^{st} (g (b))) D f (w) \in ℝ) \to (f (1^{st} (g (b))) D f (x)) +_{𝑒} (f (1^{st} (g (b))) D f (w)) = (f (1^{st} (g (b))) D f (x)) + (f (1^{st} (g (b))) D f (w))$
392	359 375 391	syl2an	$⊢ ((((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land f (1^{st} (g (b))) D f (x) < \frac{d}{2}) \land (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land f (1^{st} (g (b))) D f (w) < \frac{d}{2})) \to (f (1^{st} (g (b))) D f (x)) +_{𝑒} (f (1^{st} (g (b))) D f (w)) = (f (1^{st} (g (b))) D f (x)) + (f (1^{st} (g (b))) D f (w))$
393	392	anandis	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2})) \to (f (1^{st} (g (b))) D f (x)) +_{𝑒} (f (1^{st} (g (b))) D f (w)) = (f (1^{st} (g (b))) D f (x)) + (f (1^{st} (g (b))) D f (w))$
394	390 393	eqtrd	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2})) \to (f (x) D f (1^{st} (g (b)))) +_{𝑒} (f (1^{st} (g (b))) D f (w)) = (f (1^{st} (g (b))) D f (x)) + (f (1^{st} (g (b))) D f (w))$
395	385 394	breqtrd	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2})) \to f (x) D f (w) \leq (f (1^{st} (g (b))) D f (x)) + (f (1^{st} (g (b))) D f (w))$
396		lt2add	$⊢ ((f (1^{st} (g (b))) D f (x) \in ℝ \land f (1^{st} (g (b))) D f (w) \in ℝ) \land (\frac{d}{2} \in ℝ \land \frac{d}{2} \in ℝ)) \to ((f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2}) \to (f (1^{st} (g (b))) D f (x)) + (f (1^{st} (g (b))) D f (w)) < (\frac{d}{2}) + (\frac{d}{2}))$
397	396	expcom	$⊢ (\frac{d}{2} \in ℝ \land \frac{d}{2} \in ℝ) \to ((f (1^{st} (g (b))) D f (x) \in ℝ \land f (1^{st} (g (b))) D f (w) \in ℝ) \to ((f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2}) \to (f (1^{st} (g (b))) D f (x)) + (f (1^{st} (g (b))) D f (w)) < (\frac{d}{2}) + (\frac{d}{2})))$
398	352 352 397	syl2anc	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to ((f (1^{st} (g (b))) D f (x) \in ℝ \land f (1^{st} (g (b))) D f (w) \in ℝ) \to ((f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2}) \to (f (1^{st} (g (b))) D f (x)) + (f (1^{st} (g (b))) D f (w)) < (\frac{d}{2}) + (\frac{d}{2})))$
399	357 373 398	syl2and	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to ((f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2}) \to ((f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2}) \to (f (1^{st} (g (b))) D f (x)) + (f (1^{st} (g (b))) D f (w)) < (\frac{d}{2}) + (\frac{d}{2})))$
400	399	pm2.43d	$⊢ (((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b \in s) \to ((f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2}) \to (f (1^{st} (g (b))) D f (x)) + (f (1^{st} (g (b))) D f (w)) < (\frac{d}{2}) + (\frac{d}{2}))$
401	400	ad2ant2r	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to ((f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2}) \to (f (1^{st} (g (b))) D f (x)) + (f (1^{st} (g (b))) D f (w)) < (\frac{d}{2}) + (\frac{d}{2}))$
402	401	imp	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2})) \to (f (1^{st} (g (b))) D f (x)) + (f (1^{st} (g (b))) D f (w)) < (\frac{d}{2}) + (\frac{d}{2})$
403		rpcn	$⊢ d \in ℝ^{+} \to d \in ℂ$
404	403	2halvesd	$⊢ d \in ℝ^{+} \to (\frac{d}{2}) + (\frac{d}{2}) = d$
405	404	ad6antlr	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2})) \to (\frac{d}{2}) + (\frac{d}{2}) = d$
406	402 405	breqtrd	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2})) \to (f (1^{st} (g (b))) D f (x)) + (f (1^{st} (g (b))) D f (w)) < d$
407	335 379 381 395 406	xrlelttrd	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \land (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2})) \to f (x) D f (w) < d$
408	407	ex	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to ((f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2}) \to f (x) D f (w) < d)$
409	325 408	imim12d	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to (((1^{st} (g (b)) C x < 2^{nd} (g (b)) + 2^{nd} (g (b)) \land 1^{st} (g (b)) C w < 2^{nd} (g (b)) + 2^{nd} (g (b))) \to (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2})) \to (x C w < sup (ran ran g ℝ <) \to f (x) D f (w) < d))$
410	198 409	sylanl1	$⊢ ((((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b))) \land (b \in s \land x \in b)) \to (((1^{st} (g (b)) C x < 2^{nd} (g (b)) + 2^{nd} (g (b)) \land 1^{st} (g (b)) C w < 2^{nd} (g (b)) + 2^{nd} (g (b))) \to (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2})) \to (x C w < sup (ran ran g ℝ <) \to f (x) D f (w) < d))$
411	410	adantlrr	$⊢ ((((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))) \land (b \in s \land x \in b)) \to (((1^{st} (g (b)) C x < 2^{nd} (g (b)) + 2^{nd} (g (b)) \land 1^{st} (g (b)) C w < 2^{nd} (g (b)) + 2^{nd} (g (b))) \to (f (1^{st} (g (b))) D f (x) < \frac{d}{2} \land f (1^{st} (g (b))) D f (w) < \frac{d}{2})) \to (x C w < sup (ran ran g ℝ <) \to f (x) D f (w) < d))$
412	195 411	mpd	$⊢ ((((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))) \land (b \in s \land x \in b)) \to (x C w < sup (ran ran g ℝ <) \to f (x) D f (w) < d)$
413	412	exp32	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))) \to (b \in s \to (x \in b \to (x C w < sup (ran ran g ℝ <) \to f (x) D f (w) < d)))$
414	176 413	sylan2	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land (\forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2})) \land b \in s)) \to (b \in s \to (x \in b \to (x C w < sup (ran ran g ℝ <) \to f (x) D f (w) < d)))$
415	414	expr	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land \forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))) \to (b \in s \to (b \in s \to (x \in b \to (x C w < sup (ran ran g ℝ <) \to f (x) D f (w) < d))))$
416	415	pm2.43d	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \land (x \in X \land w \in X)) \land \forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))) \to (b \in s \to (x \in b \to (x C w < sup (ran ran g ℝ <) \to f (x) D f (w) < d)))$
417	416	an32s	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \land \forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))) \land (x \in X \land w \in X)) \to (b \in s \to (x \in b \to (x C w < sup (ran ran g ℝ <) \to f (x) D f (w) < d)))$
418	174 175 417	rexlimd	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \land \forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))) \land (x \in X \land w \in X)) \to (\exists b \in s x \in b \to (x C w < sup (ran ran g ℝ <) \to f (x) D f (w) < d))$
419	169 418	mpd	$⊢ (((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \land \forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))) \land (x \in X \land w \in X)) \to (x C w < sup (ran ran g ℝ <) \to f (x) D f (w) < d)$
420	419	ralrimivva	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \land \forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))) \to \forall x \in X \forall w \in X (x C w < sup (ran ran g ℝ <) \to f (x) D f (w) < d)$
421		breq2	$⊢ z = sup (ran ran g ℝ <) \to (x C w < z \leftrightarrow x C w < sup (ran ran g ℝ <))$
422	421	imbi1d	$⊢ z = sup (ran ran g ℝ <) \to ((x C w < z \to f (x) D f (w) < d) \leftrightarrow (x C w < sup (ran ran g ℝ <) \to f (x) D f (w) < d))$
423	422	2ralbidv	$⊢ z = sup (ran ran g ℝ <) \to (\forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d) \leftrightarrow \forall x \in X \forall w \in X (x C w < sup (ran ran g ℝ <) \to f (x) D f (w) < d))$
424	423	rspcev	$⊢ (sup (ran ran g ℝ <) \in ℝ^{+} \land \forall x \in X \forall w \in X (x C w < sup (ran ran g ℝ <) \to f (x) D f (w) < d)) \to \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d)$
425	160 420 424	syl2anc	$⊢ ((((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \land g : s ⟶ X \times ℝ^{+}) \land \forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))) \to \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d)$
426	425	expl	$⊢ ((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \to ((g : s ⟶ X \times ℝ^{+} \land \forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))) \to \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d))$
427	426	exlimdv	$⊢ ((((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \land ⋃ MetOpen (C) = ⋃ s) \to (\exists g (g : s ⟶ X \times ℝ^{+} \land \forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2}))) \to \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d))$
428	427	expimpd	$⊢ (((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in Fin) \to ((⋃ MetOpen (C) = ⋃ s \land \exists g (g : s ⟶ X \times ℝ^{+} \land \forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2})))) \to \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d))$
429	105 428	sylan2	$⊢ (((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \land s \in (𝒫 MetOpen (C) \cap Fin)) \to ((⋃ MetOpen (C) = ⋃ s \land \exists g (g : s ⟶ X \times ℝ^{+} \land \forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2})))) \to \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d))$
430	429	rexlimdva	$⊢ ((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \to (\exists s \in (𝒫 MetOpen (C) \cap Fin) (⋃ MetOpen (C) = ⋃ s \land \exists g (g : s ⟶ X \times ℝ^{+} \land \forall b \in s (b = 1^{st} (g (b)) ball (C) 2^{nd} (g (b)) \land \forall c \in X (1^{st} (g (b)) C c < 2^{nd} (g (b)) + 2^{nd} (g (b)) \to f (1^{st} (g (b))) D f (c) < \frac{d}{2})))) \to \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d))$
431	104 430	syld	$⊢ ((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \to (\forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < \frac{d}{2}) \to \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d))$
432	20 431	syl5	$⊢ ((φ \land f : X ⟶ Y) \land d \in ℝ^{+}) \to ((\frac{d}{2} \in ℝ^{+} \land \forall y \in ℝ^{+} \forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < y)) \to \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d))$
433	432	exp4b	$⊢ (φ \land f : X ⟶ Y) \to (d \in ℝ^{+} \to (\frac{d}{2} \in ℝ^{+} \to (\forall y \in ℝ^{+} \forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < y) \to \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d))))$
434	14 433	mpdi	$⊢ (φ \land f : X ⟶ Y) \to (d \in ℝ^{+} \to (\forall y \in ℝ^{+} \forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < y) \to \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d)))$
435	434	ralrimiv	$⊢ (φ \land f : X ⟶ Y) \to \forall d \in ℝ^{+} (\forall y \in ℝ^{+} \forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < y) \to \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d))$
436		r19.21v	$⊢ \forall d \in ℝ^{+} (\forall y \in ℝ^{+} \forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < y) \to \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d)) \leftrightarrow (\forall y \in ℝ^{+} \forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < y) \to \forall d \in ℝ^{+} \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d))$
437	435 436	sylib	$⊢ (φ \land f : X ⟶ Y) \to (\forall y \in ℝ^{+} \forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < y) \to \forall d \in ℝ^{+} \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d))$
438	13 437	impbid2	$⊢ (φ \land f : X ⟶ Y) \to (\forall d \in ℝ^{+} \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d) \leftrightarrow \forall y \in ℝ^{+} \forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < y))$
439		ralcom	$⊢ \forall y \in ℝ^{+} \forall x \in X \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < y) \leftrightarrow \forall x \in X \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < y)$
440	438 439	bitrdi	$⊢ (φ \land f : X ⟶ Y) \to (\forall d \in ℝ^{+} \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d) \leftrightarrow \forall x \in X \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < y))$
441	440	pm5.32da	$⊢ φ \to ((f : X ⟶ Y \land \forall d \in ℝ^{+} \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d)) \leftrightarrow (f : X ⟶ Y \land \forall x \in X \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < y)))$
442		eqid	$⊢ metUnif (C) = metUnif (C)$
443		eqid	$⊢ metUnif (D) = metUnif (D)$
444		xmetpsmet	$⊢ C \in ∞Met (X) \to C \in PsMet (X)$
445	1 444	syl	$⊢ φ \to C \in PsMet (X)$
446		xmetpsmet	$⊢ D \in ∞Met (Y) \to D \in PsMet (Y)$
447	2 446	syl	$⊢ φ \to D \in PsMet (Y)$
448	442 443 4 5 445 447	metucn	$⊢ φ \to (f \in (metUnif (C) uCn metUnif (D)) \leftrightarrow (f : X ⟶ Y \land \forall d \in ℝ^{+} \exists z \in ℝ^{+} \forall x \in X \forall w \in X (x C w < z \to f (x) D f (w) < d)))$
449		eqid	$⊢ MetOpen (D) = MetOpen (D)$
450	26 449	metcn	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y)) \to (f \in (MetOpen (C) Cn MetOpen (D)) \leftrightarrow (f : X ⟶ Y \land \forall x \in X \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < y)))$
451	1 2 450	syl2anc	$⊢ φ \to (f \in (MetOpen (C) Cn MetOpen (D)) \leftrightarrow (f : X ⟶ Y \land \forall x \in X \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in X (x C w < z \to f (x) D f (w) < y)))$
452	441 448 451	3bitr4d	$⊢ φ \to (f \in (metUnif (C) uCn metUnif (D)) \leftrightarrow f \in (MetOpen (C) Cn MetOpen (D)))$
453	452	eqrdv	$⊢ φ \to metUnif (C) uCn metUnif (D) = MetOpen (C) Cn MetOpen (D)$

Metamath Proof Explorer

Theorem heicant

Proof