caublcls

Description: The convergent point of a sequence of nested balls is in the closures of any of the balls (i.e. it is in the intersection of the closures). Indeed, it is the only point in the intersection because a metric space is Hausdorff, but we don't prove this here. (Contributed by Mario Carneiro, 21-Jan-2014) (Revised by Mario Carneiro, 1-May-2014)

	Ref	Expression
Hypotheses	caubl.2	$⊢ φ \to D \in ∞Met (X)$
	caubl.3	$⊢ φ \to F : ℕ ⟶ X \times ℝ^{+}$
	caubl.4	$⊢ φ \to \forall n \in ℕ ball (D) (F (n + 1)) \subseteq ball (D) (F (n))$
	caublcls.6	$⊢ J = MetOpen (D)$
Assertion	caublcls	$⊢ (φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \to P \in cls (J) (ball (D) (F (A)))$

Proof

Step	Hyp	Ref	Expression
1		caubl.2	$⊢ φ \to D \in ∞Met (X)$
2		caubl.3	$⊢ φ \to F : ℕ ⟶ X \times ℝ^{+}$
3		caubl.4	$⊢ φ \to \forall n \in ℕ ball (D) (F (n + 1)) \subseteq ball (D) (F (n))$
4		caublcls.6	$⊢ J = MetOpen (D)$
5		eqid	$⊢ ℤ_{\geq A} = ℤ_{\geq A}$
6	1	3ad2ant1	$⊢ (φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \to D \in ∞Met (X)$
7	4	mopntopon	$⊢ D \in ∞Met (X) \to J \in TopOn (X)$
8	6 7	syl	$⊢ (φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \to J \in TopOn (X)$
9		simp3	$⊢ (φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \to A \in ℕ$
10	9	nnzd	$⊢ (φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \to A \in ℤ$
11		simp2	$⊢ (φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \to (1^{st} \circ F) \underset{t}{⇝} (J) P$
12		2fveq3	$⊢ r = A \to ball (D) (F (r)) = ball (D) (F (A))$
13	12	sseq1d	$⊢ r = A \to (ball (D) (F (r)) \subseteq ball (D) (F (A)) \leftrightarrow ball (D) (F (A)) \subseteq ball (D) (F (A)))$
14	13	imbi2d	$⊢ r = A \to (((φ \land A \in ℕ) \to ball (D) (F (r)) \subseteq ball (D) (F (A))) \leftrightarrow ((φ \land A \in ℕ) \to ball (D) (F (A)) \subseteq ball (D) (F (A))))$
15		2fveq3	$⊢ r = k \to ball (D) (F (r)) = ball (D) (F (k))$
16	15	sseq1d	$⊢ r = k \to (ball (D) (F (r)) \subseteq ball (D) (F (A)) \leftrightarrow ball (D) (F (k)) \subseteq ball (D) (F (A)))$
17	16	imbi2d	$⊢ r = k \to (((φ \land A \in ℕ) \to ball (D) (F (r)) \subseteq ball (D) (F (A))) \leftrightarrow ((φ \land A \in ℕ) \to ball (D) (F (k)) \subseteq ball (D) (F (A))))$
18		2fveq3	$⊢ r = k + 1 \to ball (D) (F (r)) = ball (D) (F (k + 1))$
19	18	sseq1d	$⊢ r = k + 1 \to (ball (D) (F (r)) \subseteq ball (D) (F (A)) \leftrightarrow ball (D) (F (k + 1)) \subseteq ball (D) (F (A)))$
20	19	imbi2d	$⊢ r = k + 1 \to (((φ \land A \in ℕ) \to ball (D) (F (r)) \subseteq ball (D) (F (A))) \leftrightarrow ((φ \land A \in ℕ) \to ball (D) (F (k + 1)) \subseteq ball (D) (F (A))))$
21		ssid	$⊢ ball (D) (F (A)) \subseteq ball (D) (F (A))$
22	21	2a1i	$⊢ A \in ℤ \to ((φ \land A \in ℕ) \to ball (D) (F (A)) \subseteq ball (D) (F (A)))$
23		eluznn	$⊢ (A \in ℕ \land k \in ℤ_{\geq A}) \to k \in ℕ$
24		fvoveq1	$⊢ n = k \to F (n + 1) = F (k + 1)$
25	24	fveq2d	$⊢ n = k \to ball (D) (F (n + 1)) = ball (D) (F (k + 1))$
26		2fveq3	$⊢ n = k \to ball (D) (F (n)) = ball (D) (F (k))$
27	25 26	sseq12d	$⊢ n = k \to (ball (D) (F (n + 1)) \subseteq ball (D) (F (n)) \leftrightarrow ball (D) (F (k + 1)) \subseteq ball (D) (F (k)))$
28	27	rspccva	$⊢ (\forall n \in ℕ ball (D) (F (n + 1)) \subseteq ball (D) (F (n)) \land k \in ℕ) \to ball (D) (F (k + 1)) \subseteq ball (D) (F (k))$
29	3 23 28	syl2an	$⊢ (φ \land (A \in ℕ \land k \in ℤ_{\geq A})) \to ball (D) (F (k + 1)) \subseteq ball (D) (F (k))$
30	29	anassrs	$⊢ ((φ \land A \in ℕ) \land k \in ℤ_{\geq A}) \to ball (D) (F (k + 1)) \subseteq ball (D) (F (k))$
31		sstr2	$⊢ ball (D) (F (k + 1)) \subseteq ball (D) (F (k)) \to (ball (D) (F (k)) \subseteq ball (D) (F (A)) \to ball (D) (F (k + 1)) \subseteq ball (D) (F (A)))$
32	30 31	syl	$⊢ ((φ \land A \in ℕ) \land k \in ℤ_{\geq A}) \to (ball (D) (F (k)) \subseteq ball (D) (F (A)) \to ball (D) (F (k + 1)) \subseteq ball (D) (F (A)))$
33	32	expcom	$⊢ k \in ℤ_{\geq A} \to ((φ \land A \in ℕ) \to (ball (D) (F (k)) \subseteq ball (D) (F (A)) \to ball (D) (F (k + 1)) \subseteq ball (D) (F (A))))$
34	33	a2d	$⊢ k \in ℤ_{\geq A} \to (((φ \land A \in ℕ) \to ball (D) (F (k)) \subseteq ball (D) (F (A))) \to ((φ \land A \in ℕ) \to ball (D) (F (k + 1)) \subseteq ball (D) (F (A))))$
35	14 17 20 17 22 34	uzind4	$⊢ k \in ℤ_{\geq A} \to ((φ \land A \in ℕ) \to ball (D) (F (k)) \subseteq ball (D) (F (A)))$
36	35	impcom	$⊢ ((φ \land A \in ℕ) \land k \in ℤ_{\geq A}) \to ball (D) (F (k)) \subseteq ball (D) (F (A))$
37	36	3adantl2	$⊢ ((φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \land k \in ℤ_{\geq A}) \to ball (D) (F (k)) \subseteq ball (D) (F (A))$
38	6	adantr	$⊢ ((φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \land k \in ℤ_{\geq A}) \to D \in ∞Met (X)$
39		simpl1	$⊢ ((φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \land k \in ℤ_{\geq A}) \to φ$
40	39 2	syl	$⊢ ((φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \land k \in ℤ_{\geq A}) \to F : ℕ ⟶ X \times ℝ^{+}$
41	23	3ad2antl3	$⊢ ((φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \land k \in ℤ_{\geq A}) \to k \in ℕ$
42	40 41	ffvelcdmd	$⊢ ((φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \land k \in ℤ_{\geq A}) \to F (k) \in (X \times ℝ^{+})$
43		xp1st	$⊢ F (k) \in (X \times ℝ^{+}) \to 1^{st} (F (k)) \in X$
44	42 43	syl	$⊢ ((φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \land k \in ℤ_{\geq A}) \to 1^{st} (F (k)) \in X$
45		xp2nd	$⊢ F (k) \in (X \times ℝ^{+}) \to 2^{nd} (F (k)) \in ℝ^{+}$
46	42 45	syl	$⊢ ((φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \land k \in ℤ_{\geq A}) \to 2^{nd} (F (k)) \in ℝ^{+}$
47		blcntr	$⊢ (D \in ∞Met (X) \land 1^{st} (F (k)) \in X \land 2^{nd} (F (k)) \in ℝ^{+}) \to 1^{st} (F (k)) \in (1^{st} (F (k)) ball (D) 2^{nd} (F (k)))$
48	38 44 46 47	syl3anc	$⊢ ((φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \land k \in ℤ_{\geq A}) \to 1^{st} (F (k)) \in (1^{st} (F (k)) ball (D) 2^{nd} (F (k)))$
49		fvco3	$⊢ (F : ℕ ⟶ X \times ℝ^{+} \land k \in ℕ) \to (1^{st} \circ F) (k) = 1^{st} (F (k))$
50	40 41 49	syl2anc	$⊢ ((φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \land k \in ℤ_{\geq A}) \to (1^{st} \circ F) (k) = 1^{st} (F (k))$
51		1st2nd2	$⊢ F (k) \in (X \times ℝ^{+}) \to F (k) = ⟨1^{st} (F (k)), 2^{nd} (F (k))⟩$
52	42 51	syl	$⊢ ((φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \land k \in ℤ_{\geq A}) \to F (k) = ⟨1^{st} (F (k)), 2^{nd} (F (k))⟩$
53	52	fveq2d	$⊢ ((φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \land k \in ℤ_{\geq A}) \to ball (D) (F (k)) = ball (D) (⟨1^{st} (F (k)), 2^{nd} (F (k))⟩)$
54		df-ov	$⊢ 1^{st} (F (k)) ball (D) 2^{nd} (F (k)) = ball (D) (⟨1^{st} (F (k)), 2^{nd} (F (k))⟩)$
55	53 54	eqtr4di	$⊢ ((φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \land k \in ℤ_{\geq A}) \to ball (D) (F (k)) = 1^{st} (F (k)) ball (D) 2^{nd} (F (k))$
56	48 50 55	3eltr4d	$⊢ ((φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \land k \in ℤ_{\geq A}) \to (1^{st} \circ F) (k) \in ball (D) (F (k))$
57	37 56	sseldd	$⊢ ((φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \land k \in ℤ_{\geq A}) \to (1^{st} \circ F) (k) \in ball (D) (F (A))$
58	2	ffvelcdmda	$⊢ (φ \land A \in ℕ) \to F (A) \in (X \times ℝ^{+})$
59	58	3adant2	$⊢ (φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \to F (A) \in (X \times ℝ^{+})$
60		1st2nd2	$⊢ F (A) \in (X \times ℝ^{+}) \to F (A) = ⟨1^{st} (F (A)), 2^{nd} (F (A))⟩$
61	59 60	syl	$⊢ (φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \to F (A) = ⟨1^{st} (F (A)), 2^{nd} (F (A))⟩$
62	61	fveq2d	$⊢ (φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \to ball (D) (F (A)) = ball (D) (⟨1^{st} (F (A)), 2^{nd} (F (A))⟩)$
63		df-ov	$⊢ 1^{st} (F (A)) ball (D) 2^{nd} (F (A)) = ball (D) (⟨1^{st} (F (A)), 2^{nd} (F (A))⟩)$
64	62 63	eqtr4di	$⊢ (φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \to ball (D) (F (A)) = 1^{st} (F (A)) ball (D) 2^{nd} (F (A))$
65		xp1st	$⊢ F (A) \in (X \times ℝ^{+}) \to 1^{st} (F (A)) \in X$
66	59 65	syl	$⊢ (φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \to 1^{st} (F (A)) \in X$
67		xp2nd	$⊢ F (A) \in (X \times ℝ^{+}) \to 2^{nd} (F (A)) \in ℝ^{+}$
68	59 67	syl	$⊢ (φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \to 2^{nd} (F (A)) \in ℝ^{+}$
69	68	rpxrd	$⊢ (φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \to 2^{nd} (F (A)) \in ℝ^{*}$
70		blssm	$⊢ (D \in ∞Met (X) \land 1^{st} (F (A)) \in X \land 2^{nd} (F (A)) \in ℝ^{*}) \to 1^{st} (F (A)) ball (D) 2^{nd} (F (A)) \subseteq X$
71	6 66 69 70	syl3anc	$⊢ (φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \to 1^{st} (F (A)) ball (D) 2^{nd} (F (A)) \subseteq X$
72	64 71	eqsstrd	$⊢ (φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \to ball (D) (F (A)) \subseteq X$
73	5 8 10 11 57 72	lmcls	$⊢ (φ \land (1^{st} \circ F) \underset{t}{⇝} (J) P \land A \in ℕ) \to P \in cls (J) (ball (D) (F (A)))$

Metamath Proof Explorer

Theorem caublcls

Proof