bcthlem3

Description: Lemma for bcth . The limit point of the centers in the sequence is in the intersection of every ball in the sequence. (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	bcthlem3	$⊢ (φ \land (1^{st} \circ g) \underset{t}{⇝} (J) x \land A \in ℕ) \to x \in ball (D) (g (A))$

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 = A \to g (k + 1) = g (A + 1)$
11		id	$⊢ k = A \to k = A$
12		fveq2	$⊢ k = A \to g (k) = g (A)$
13	11 12	oveq12d	$⊢ k = A \to k F g (k) = A F g (A)$
14	10 13	eleq12d	$⊢ k = A \to (g (k + 1) \in (k F g (k)) \leftrightarrow g (A + 1) \in (A F g (A)))$
15	14	rspccva	$⊢ (\forall k \in ℕ g (k + 1) \in (k F g (k)) \land A \in ℕ) \to g (A + 1) \in (A F g (A))$
16	9 15	sylan	$⊢ (φ \land A \in ℕ) \to g (A + 1) \in (A F g (A))$
17	7	ffvelrnda	$⊢ (φ \land A \in ℕ) \to g (A) \in (X \times ℝ^{+})$
18	1 2 3	bcthlem1	$⊢ (φ \land (A \in ℕ \land g (A) \in (X \times ℝ^{+}))) \to (g (A + 1) \in (A F g (A)) \leftrightarrow (g (A + 1) \in (X \times ℝ^{+}) \land 2^{nd} (g (A + 1)) < \frac{1}{A} \land cls (J) (ball (D) (g (A + 1))) \subseteq ball (D) (g (A)) ∖ M (A)))$
19	18	expr	$⊢ (φ \land A \in ℕ) \to (g (A) \in (X \times ℝ^{+}) \to (g (A + 1) \in (A F g (A)) \leftrightarrow (g (A + 1) \in (X \times ℝ^{+}) \land 2^{nd} (g (A + 1)) < \frac{1}{A} \land cls (J) (ball (D) (g (A + 1))) \subseteq ball (D) (g (A)) ∖ M (A))))$
20	17 19	mpd	$⊢ (φ \land A \in ℕ) \to (g (A + 1) \in (A F g (A)) \leftrightarrow (g (A + 1) \in (X \times ℝ^{+}) \land 2^{nd} (g (A + 1)) < \frac{1}{A} \land cls (J) (ball (D) (g (A + 1))) \subseteq ball (D) (g (A)) ∖ M (A)))$
21	16 20	mpbid	$⊢ (φ \land A \in ℕ) \to (g (A + 1) \in (X \times ℝ^{+}) \land 2^{nd} (g (A + 1)) < \frac{1}{A} \land cls (J) (ball (D) (g (A + 1))) \subseteq ball (D) (g (A)) ∖ M (A))$
22	21	simp3d	$⊢ (φ \land A \in ℕ) \to cls (J) (ball (D) (g (A + 1))) \subseteq ball (D) (g (A)) ∖ M (A)$
23	22	difss2d	$⊢ (φ \land A \in ℕ) \to cls (J) (ball (D) (g (A + 1))) \subseteq ball (D) (g (A))$
24	23	3adant2	$⊢ (φ \land (1^{st} \circ g) \underset{t}{⇝} (J) x \land A \in ℕ) \to cls (J) (ball (D) (g (A + 1))) \subseteq ball (D) (g (A))$
25		peano2nn	$⊢ A \in ℕ \to A + 1 \in ℕ$
26		cmetmet	$⊢ D \in CMet (X) \to D \in Met (X)$
27		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
28	2 26 27	3syl	$⊢ φ \to D \in ∞Met (X)$
29	1 2 3 4 5 6 7 8 9	bcthlem2	$⊢ φ \to \forall n \in ℕ ball (D) (g (n + 1)) \subseteq ball (D) (g (n))$
30	28 7 29 1	caublcls	$⊢ (φ \land (1^{st} \circ g) \underset{t}{⇝} (J) x \land A + 1 \in ℕ) \to x \in cls (J) (ball (D) (g (A + 1)))$
31	25 30	syl3an3	$⊢ (φ \land (1^{st} \circ g) \underset{t}{⇝} (J) x \land A \in ℕ) \to x \in cls (J) (ball (D) (g (A + 1)))$
32	24 31	sseldd	$⊢ (φ \land (1^{st} \circ g) \underset{t}{⇝} (J) x \land A \in ℕ) \to x \in ball (D) (g (A))$

Metamath Proof Explorer

Theorem bcthlem3

Proof