bcthlem2

Description: Lemma for bcth . The balls in the sequence form an inclusion chain. (Contributed by Mario Carneiro, 7-Jan-2014)

	Ref	Expression
Hypotheses	bcth.2	$⊢ J = MetOpen (D)$
	bcthlem.4	$⊢ φ \to D \in CMet (X)$
	bcthlem.5	$⊢ F = (k \in ℕ, z \in (X \times ℝ^{+}) ⟼ \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{k} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (k)))\})$
	bcthlem.6	$⊢ φ \to M : ℕ ⟶ Clsd (J)$
	bcthlem.7	$⊢ φ \to R \in ℝ^{+}$
	bcthlem.8	$⊢ φ \to C \in X$
	bcthlem.9	$⊢ φ \to g : ℕ ⟶ X \times ℝ^{+}$
	bcthlem.10	$⊢ φ \to g (1) = ⟨C, R⟩$
	bcthlem.11	$⊢ φ \to \forall k \in ℕ g (k + 1) \in (k F g (k))$
Assertion	bcthlem2	$⊢ φ \to \forall n \in ℕ ball (D) (g (n + 1)) \subseteq ball (D) (g (n))$

Proof

Step	Hyp	Ref	Expression
1		bcth.2	$⊢ J = MetOpen (D)$
2		bcthlem.4	$⊢ φ \to D \in CMet (X)$
3		bcthlem.5	$⊢ F = (k \in ℕ, z \in (X \times ℝ^{+}) ⟼ \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{k} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (k)))\})$
4		bcthlem.6	$⊢ φ \to M : ℕ ⟶ Clsd (J)$
5		bcthlem.7	$⊢ φ \to R \in ℝ^{+}$
6		bcthlem.8	$⊢ φ \to C \in X$
7		bcthlem.9	$⊢ φ \to g : ℕ ⟶ X \times ℝ^{+}$
8		bcthlem.10	$⊢ φ \to g (1) = ⟨C, R⟩$
9		bcthlem.11	$⊢ φ \to \forall k \in ℕ g (k + 1) \in (k F g (k))$
10		fvoveq1	$⊢ k = n \to g (k + 1) = g (n + 1)$
11		id	$⊢ k = n \to k = n$
12		fveq2	$⊢ k = n \to g (k) = g (n)$
13	11 12	oveq12d	$⊢ k = n \to k F g (k) = n F g (n)$
14	10 13	eleq12d	$⊢ k = n \to (g (k + 1) \in (k F g (k)) \leftrightarrow g (n + 1) \in (n F g (n)))$
15	14	rspccva	$⊢ (\forall k \in ℕ g (k + 1) \in (k F g (k)) \land n \in ℕ) \to g (n + 1) \in (n F g (n))$
16	9 15	sylan	$⊢ (φ \land n \in ℕ) \to g (n + 1) \in (n F g (n))$
17	7	ffvelcdmda	$⊢ (φ \land n \in ℕ) \to g (n) \in (X \times ℝ^{+})$
18	1 2 3	bcthlem1	$⊢ (φ \land (n \in ℕ \land g (n) \in (X \times ℝ^{+}))) \to (g (n + 1) \in (n F g (n)) \leftrightarrow (g (n + 1) \in (X \times ℝ^{+}) \land 2^{nd} (g (n + 1)) < \frac{1}{n} \land cls (J) (ball (D) (g (n + 1))) \subseteq ball (D) (g (n)) ∖ M (n)))$
19	18	expr	$⊢ (φ \land n \in ℕ) \to (g (n) \in (X \times ℝ^{+}) \to (g (n + 1) \in (n F g (n)) \leftrightarrow (g (n + 1) \in (X \times ℝ^{+}) \land 2^{nd} (g (n + 1)) < \frac{1}{n} \land cls (J) (ball (D) (g (n + 1))) \subseteq ball (D) (g (n)) ∖ M (n))))$
20	17 19	mpd	$⊢ (φ \land n \in ℕ) \to (g (n + 1) \in (n F g (n)) \leftrightarrow (g (n + 1) \in (X \times ℝ^{+}) \land 2^{nd} (g (n + 1)) < \frac{1}{n} \land cls (J) (ball (D) (g (n + 1))) \subseteq ball (D) (g (n)) ∖ M (n)))$
21	16 20	mpbid	$⊢ (φ \land n \in ℕ) \to (g (n + 1) \in (X \times ℝ^{+}) \land 2^{nd} (g (n + 1)) < \frac{1}{n} \land cls (J) (ball (D) (g (n + 1))) \subseteq ball (D) (g (n)) ∖ M (n))$
22		cmetmet	$⊢ D \in CMet (X) \to D \in Met (X)$
23	2 22	syl	$⊢ φ \to D \in Met (X)$
24		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
25	23 24	syl	$⊢ φ \to D \in ∞Met (X)$
26	1	mopntop	$⊢ D \in ∞Met (X) \to J \in Top$
27	25 26	syl	$⊢ φ \to J \in Top$
28		xp1st	$⊢ g (n + 1) \in (X \times ℝ^{+}) \to 1^{st} (g (n + 1)) \in X$
29		xp2nd	$⊢ g (n + 1) \in (X \times ℝ^{+}) \to 2^{nd} (g (n + 1)) \in ℝ^{+}$
30	29	rpxrd	$⊢ g (n + 1) \in (X \times ℝ^{+}) \to 2^{nd} (g (n + 1)) \in ℝ^{*}$
31	28 30	jca	$⊢ g (n + 1) \in (X \times ℝ^{+}) \to (1^{st} (g (n + 1)) \in X \land 2^{nd} (g (n + 1)) \in ℝ^{*})$
32		blssm	$⊢ (D \in ∞Met (X) \land 1^{st} (g (n + 1)) \in X \land 2^{nd} (g (n + 1)) \in ℝ^{*}) \to 1^{st} (g (n + 1)) ball (D) 2^{nd} (g (n + 1)) \subseteq X$
33	32	3expb	$⊢ (D \in ∞Met (X) \land (1^{st} (g (n + 1)) \in X \land 2^{nd} (g (n + 1)) \in ℝ^{*})) \to 1^{st} (g (n + 1)) ball (D) 2^{nd} (g (n + 1)) \subseteq X$
34	25 31 33	syl2an	$⊢ (φ \land g (n + 1) \in (X \times ℝ^{+})) \to 1^{st} (g (n + 1)) ball (D) 2^{nd} (g (n + 1)) \subseteq X$
35		df-ov	$⊢ 1^{st} (g (n + 1)) ball (D) 2^{nd} (g (n + 1)) = ball (D) (⟨1^{st} (g (n + 1)), 2^{nd} (g (n + 1))⟩)$
36		1st2nd2	$⊢ g (n + 1) \in (X \times ℝ^{+}) \to g (n + 1) = ⟨1^{st} (g (n + 1)), 2^{nd} (g (n + 1))⟩$
37	36	fveq2d	$⊢ g (n + 1) \in (X \times ℝ^{+}) \to ball (D) (g (n + 1)) = ball (D) (⟨1^{st} (g (n + 1)), 2^{nd} (g (n + 1))⟩)$
38	35 37	eqtr4id	$⊢ g (n + 1) \in (X \times ℝ^{+}) \to 1^{st} (g (n + 1)) ball (D) 2^{nd} (g (n + 1)) = ball (D) (g (n + 1))$
39	38	adantl	$⊢ (φ \land g (n + 1) \in (X \times ℝ^{+})) \to 1^{st} (g (n + 1)) ball (D) 2^{nd} (g (n + 1)) = ball (D) (g (n + 1))$
40	1	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
41	25 40	syl	$⊢ φ \to X = ⋃ J$
42	41	adantr	$⊢ (φ \land g (n + 1) \in (X \times ℝ^{+})) \to X = ⋃ J$
43	34 39 42	3sstr3d	$⊢ (φ \land g (n + 1) \in (X \times ℝ^{+})) \to ball (D) (g (n + 1)) \subseteq ⋃ J$
44		eqid	$⊢ ⋃ J = ⋃ J$
45	44	sscls	$⊢ (J \in Top \land ball (D) (g (n + 1)) \subseteq ⋃ J) \to ball (D) (g (n + 1)) \subseteq cls (J) (ball (D) (g (n + 1)))$
46	27 43 45	syl2an2r	$⊢ (φ \land g (n + 1) \in (X \times ℝ^{+})) \to ball (D) (g (n + 1)) \subseteq cls (J) (ball (D) (g (n + 1)))$
47		difss2	$⊢ cls (J) (ball (D) (g (n + 1))) \subseteq ball (D) (g (n)) ∖ M (n) \to cls (J) (ball (D) (g (n + 1))) \subseteq ball (D) (g (n))$
48		sstr2	$⊢ ball (D) (g (n + 1)) \subseteq cls (J) (ball (D) (g (n + 1))) \to (cls (J) (ball (D) (g (n + 1))) \subseteq ball (D) (g (n)) \to ball (D) (g (n + 1)) \subseteq ball (D) (g (n)))$
49	46 47 48	syl2im	$⊢ (φ \land g (n + 1) \in (X \times ℝ^{+})) \to (cls (J) (ball (D) (g (n + 1))) \subseteq ball (D) (g (n)) ∖ M (n) \to ball (D) (g (n + 1)) \subseteq ball (D) (g (n)))$
50	49	a1d	$⊢ (φ \land g (n + 1) \in (X \times ℝ^{+})) \to (2^{nd} (g (n + 1)) < \frac{1}{n} \to (cls (J) (ball (D) (g (n + 1))) \subseteq ball (D) (g (n)) ∖ M (n) \to ball (D) (g (n + 1)) \subseteq ball (D) (g (n))))$
51	50	ex	$⊢ φ \to (g (n + 1) \in (X \times ℝ^{+}) \to (2^{nd} (g (n + 1)) < \frac{1}{n} \to (cls (J) (ball (D) (g (n + 1))) \subseteq ball (D) (g (n)) ∖ M (n) \to ball (D) (g (n + 1)) \subseteq ball (D) (g (n)))))$
52	51	3impd	$⊢ φ \to ((g (n + 1) \in (X \times ℝ^{+}) \land 2^{nd} (g (n + 1)) < \frac{1}{n} \land cls (J) (ball (D) (g (n + 1))) \subseteq ball (D) (g (n)) ∖ M (n)) \to ball (D) (g (n + 1)) \subseteq ball (D) (g (n)))$
53	52	adantr	$⊢ (φ \land n \in ℕ) \to ((g (n + 1) \in (X \times ℝ^{+}) \land 2^{nd} (g (n + 1)) < \frac{1}{n} \land cls (J) (ball (D) (g (n + 1))) \subseteq ball (D) (g (n)) ∖ M (n)) \to ball (D) (g (n + 1)) \subseteq ball (D) (g (n)))$
54	21 53	mpd	$⊢ (φ \land n \in ℕ) \to ball (D) (g (n + 1)) \subseteq ball (D) (g (n))$
55	54	ralrimiva	$⊢ φ \to \forall n \in ℕ ball (D) (g (n + 1)) \subseteq ball (D) (g (n))$

Metamath Proof Explorer

Theorem bcthlem2

Proof