bcthlem4

Description: Lemma for bcth . Given any open ball ( C ( ballD ) R ) as starting point (and in particular, a ball in int ( U. ran M ) ), the limit point x of the centers of the induced sequence of balls g is outside U. ran M . Note that a set A has empty interior iff every nonempty open set U contains points outside A , i.e. ( U \ A ) =/= (/) . (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	bcthlem4	$⊢ φ \to (C ball (D) R) ∖ ⋃ ran M \neq \emptyset$

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		cmetmet	$⊢ D \in CMet (X) \to D \in Met (X)$
11	2 10	syl	$⊢ φ \to D \in Met (X)$
12		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
13	11 12	syl	$⊢ φ \to D \in ∞Met (X)$
14	1 2 3 4 5 6 7 8 9	bcthlem2	$⊢ φ \to \forall n \in ℕ ball (D) (g (n + 1)) \subseteq ball (D) (g (n))$
15		elrp	$⊢ r \in ℝ^{+} \leftrightarrow (r \in ℝ \land 0 < r)$
16		nnrecl	$⊢ (r \in ℝ \land 0 < r) \to \exists m \in ℕ \frac{1}{m} < r$
17	15 16	sylbi	$⊢ r \in ℝ^{+} \to \exists m \in ℕ \frac{1}{m} < r$
18	17	adantl	$⊢ (φ \land r \in ℝ^{+}) \to \exists m \in ℕ \frac{1}{m} < r$
19		peano2nn	$⊢ m \in ℕ \to m + 1 \in ℕ$
20	19	adantl	$⊢ ((φ \land r \in ℝ^{+}) \land m \in ℕ) \to m + 1 \in ℕ$
21		fvoveq1	$⊢ k = m \to g (k + 1) = g (m + 1)$
22		id	$⊢ k = m \to k = m$
23		fveq2	$⊢ k = m \to g (k) = g (m)$
24	22 23	oveq12d	$⊢ k = m \to k F g (k) = m F g (m)$
25	21 24	eleq12d	$⊢ k = m \to (g (k + 1) \in (k F g (k)) \leftrightarrow g (m + 1) \in (m F g (m)))$
26	25	rspccva	$⊢ (\forall k \in ℕ g (k + 1) \in (k F g (k)) \land m \in ℕ) \to g (m + 1) \in (m F g (m))$
27	9 26	sylan	$⊢ (φ \land m \in ℕ) \to g (m + 1) \in (m F g (m))$
28	7	ffvelcdmda	$⊢ (φ \land m \in ℕ) \to g (m) \in (X \times ℝ^{+})$
29	1 2 3	bcthlem1	$⊢ (φ \land (m \in ℕ \land g (m) \in (X \times ℝ^{+}))) \to (g (m + 1) \in (m F g (m)) \leftrightarrow (g (m + 1) \in (X \times ℝ^{+}) \land 2^{nd} (g (m + 1)) < \frac{1}{m} \land cls (J) (ball (D) (g (m + 1))) \subseteq ball (D) (g (m)) ∖ M (m)))$
30	29	expr	$⊢ (φ \land m \in ℕ) \to (g (m) \in (X \times ℝ^{+}) \to (g (m + 1) \in (m F g (m)) \leftrightarrow (g (m + 1) \in (X \times ℝ^{+}) \land 2^{nd} (g (m + 1)) < \frac{1}{m} \land cls (J) (ball (D) (g (m + 1))) \subseteq ball (D) (g (m)) ∖ M (m))))$
31	28 30	mpd	$⊢ (φ \land m \in ℕ) \to (g (m + 1) \in (m F g (m)) \leftrightarrow (g (m + 1) \in (X \times ℝ^{+}) \land 2^{nd} (g (m + 1)) < \frac{1}{m} \land cls (J) (ball (D) (g (m + 1))) \subseteq ball (D) (g (m)) ∖ M (m)))$
32	27 31	mpbid	$⊢ (φ \land m \in ℕ) \to (g (m + 1) \in (X \times ℝ^{+}) \land 2^{nd} (g (m + 1)) < \frac{1}{m} \land cls (J) (ball (D) (g (m + 1))) \subseteq ball (D) (g (m)) ∖ M (m))$
33	32	simp2d	$⊢ (φ \land m \in ℕ) \to 2^{nd} (g (m + 1)) < \frac{1}{m}$
34	33	adantlr	$⊢ ((φ \land r \in ℝ^{+}) \land m \in ℕ) \to 2^{nd} (g (m + 1)) < \frac{1}{m}$
35	32	simp1d	$⊢ (φ \land m \in ℕ) \to g (m + 1) \in (X \times ℝ^{+})$
36		xp2nd	$⊢ g (m + 1) \in (X \times ℝ^{+}) \to 2^{nd} (g (m + 1)) \in ℝ^{+}$
37	35 36	syl	$⊢ (φ \land m \in ℕ) \to 2^{nd} (g (m + 1)) \in ℝ^{+}$
38	37	rpred	$⊢ (φ \land m \in ℕ) \to 2^{nd} (g (m + 1)) \in ℝ$
39	38	adantlr	$⊢ ((φ \land r \in ℝ^{+}) \land m \in ℕ) \to 2^{nd} (g (m + 1)) \in ℝ$
40		nnrecre	$⊢ m \in ℕ \to \frac{1}{m} \in ℝ$
41	40	adantl	$⊢ ((φ \land r \in ℝ^{+}) \land m \in ℕ) \to \frac{1}{m} \in ℝ$
42		rpre	$⊢ r \in ℝ^{+} \to r \in ℝ$
43	42	ad2antlr	$⊢ ((φ \land r \in ℝ^{+}) \land m \in ℕ) \to r \in ℝ$
44		lttr	$⊢ (2^{nd} (g (m + 1)) \in ℝ \land \frac{1}{m} \in ℝ \land r \in ℝ) \to ((2^{nd} (g (m + 1)) < \frac{1}{m} \land \frac{1}{m} < r) \to 2^{nd} (g (m + 1)) < r)$
45	39 41 43 44	syl3anc	$⊢ ((φ \land r \in ℝ^{+}) \land m \in ℕ) \to ((2^{nd} (g (m + 1)) < \frac{1}{m} \land \frac{1}{m} < r) \to 2^{nd} (g (m + 1)) < r)$
46	34 45	mpand	$⊢ ((φ \land r \in ℝ^{+}) \land m \in ℕ) \to (\frac{1}{m} < r \to 2^{nd} (g (m + 1)) < r)$
47		2fveq3	$⊢ n = m + 1 \to 2^{nd} (g (n)) = 2^{nd} (g (m + 1))$
48	47	breq1d	$⊢ n = m + 1 \to (2^{nd} (g (n)) < r \leftrightarrow 2^{nd} (g (m + 1)) < r)$
49	48	rspcev	$⊢ (m + 1 \in ℕ \land 2^{nd} (g (m + 1)) < r) \to \exists n \in ℕ 2^{nd} (g (n)) < r$
50	20 46 49	syl6an	$⊢ ((φ \land r \in ℝ^{+}) \land m \in ℕ) \to (\frac{1}{m} < r \to \exists n \in ℕ 2^{nd} (g (n)) < r)$
51	50	rexlimdva	$⊢ (φ \land r \in ℝ^{+}) \to (\exists m \in ℕ \frac{1}{m} < r \to \exists n \in ℕ 2^{nd} (g (n)) < r)$
52	18 51	mpd	$⊢ (φ \land r \in ℝ^{+}) \to \exists n \in ℕ 2^{nd} (g (n)) < r$
53	52	ralrimiva	$⊢ φ \to \forall r \in ℝ^{+} \exists n \in ℕ 2^{nd} (g (n)) < r$
54	13 7 14 53	caubl	$⊢ φ \to 1^{st} \circ g \in Cau (D)$
55	1	cmetcau	$⊢ (D \in CMet (X) \land 1^{st} \circ g \in Cau (D)) \to 1^{st} \circ g \in dom \underset{t}{⇝} (J)$
56	2 54 55	syl2anc	$⊢ φ \to 1^{st} \circ g \in dom \underset{t}{⇝} (J)$
57		fo1st	$⊢ 1^{st} : V \underset{onto}{⟶} V$
58		fofun	$⊢ 1^{st} : V \underset{onto}{⟶} V \to Fun 1^{st}$
59	57 58	ax-mp	$⊢ Fun 1^{st}$
60		vex	$⊢ g \in V$
61		cofunexg	$⊢ (Fun 1^{st} \land g \in V) \to 1^{st} \circ g \in V$
62	59 60 61	mp2an	$⊢ 1^{st} \circ g \in V$
63	62	eldm	$⊢ 1^{st} \circ g \in dom \underset{t}{⇝} (J) \leftrightarrow \exists x (1^{st} \circ g) \underset{t}{⇝} (J) x$
64	56 63	sylib	$⊢ φ \to \exists x (1^{st} \circ g) \underset{t}{⇝} (J) x$
65		1nn	$⊢ 1 \in ℕ$
66	1 2 3 4 5 6 7 8 9	bcthlem3	$⊢ (φ \land (1^{st} \circ g) \underset{t}{⇝} (J) x \land 1 \in ℕ) \to x \in ball (D) (g (1))$
67	65 66	mp3an3	$⊢ (φ \land (1^{st} \circ g) \underset{t}{⇝} (J) x) \to x \in ball (D) (g (1))$
68	8	fveq2d	$⊢ φ \to ball (D) (g (1)) = ball (D) (⟨C, R⟩)$
69		df-ov	$⊢ C ball (D) R = ball (D) (⟨C, R⟩)$
70	68 69	eqtr4di	$⊢ φ \to ball (D) (g (1)) = C ball (D) R$
71	70	adantr	$⊢ (φ \land (1^{st} \circ g) \underset{t}{⇝} (J) x) \to ball (D) (g (1)) = C ball (D) R$
72	67 71	eleqtrd	$⊢ (φ \land (1^{st} \circ g) \underset{t}{⇝} (J) x) \to x \in (C ball (D) R)$
73	1	mopntop	$⊢ D \in ∞Met (X) \to J \in Top$
74	13 73	syl	$⊢ φ \to J \in Top$
75	74	adantr	$⊢ (φ \land m \in ℕ) \to J \in Top$
76	13	adantr	$⊢ (φ \land m \in ℕ) \to D \in ∞Met (X)$
77		xp1st	$⊢ g (m + 1) \in (X \times ℝ^{+}) \to 1^{st} (g (m + 1)) \in X$
78	35 77	syl	$⊢ (φ \land m \in ℕ) \to 1^{st} (g (m + 1)) \in X$
79	37	rpxrd	$⊢ (φ \land m \in ℕ) \to 2^{nd} (g (m + 1)) \in ℝ^{*}$
80		blssm	$⊢ (D \in ∞Met (X) \land 1^{st} (g (m + 1)) \in X \land 2^{nd} (g (m + 1)) \in ℝ^{*}) \to 1^{st} (g (m + 1)) ball (D) 2^{nd} (g (m + 1)) \subseteq X$
81	76 78 79 80	syl3anc	$⊢ (φ \land m \in ℕ) \to 1^{st} (g (m + 1)) ball (D) 2^{nd} (g (m + 1)) \subseteq X$
82		df-ov	$⊢ 1^{st} (g (m + 1)) ball (D) 2^{nd} (g (m + 1)) = ball (D) (⟨1^{st} (g (m + 1)), 2^{nd} (g (m + 1))⟩)$
83		1st2nd2	$⊢ g (m + 1) \in (X \times ℝ^{+}) \to g (m + 1) = ⟨1^{st} (g (m + 1)), 2^{nd} (g (m + 1))⟩$
84	35 83	syl	$⊢ (φ \land m \in ℕ) \to g (m + 1) = ⟨1^{st} (g (m + 1)), 2^{nd} (g (m + 1))⟩$
85	84	fveq2d	$⊢ (φ \land m \in ℕ) \to ball (D) (g (m + 1)) = ball (D) (⟨1^{st} (g (m + 1)), 2^{nd} (g (m + 1))⟩)$
86	82 85	eqtr4id	$⊢ (φ \land m \in ℕ) \to 1^{st} (g (m + 1)) ball (D) 2^{nd} (g (m + 1)) = ball (D) (g (m + 1))$
87	1	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
88	13 87	syl	$⊢ φ \to X = ⋃ J$
89	88	adantr	$⊢ (φ \land m \in ℕ) \to X = ⋃ J$
90	81 86 89	3sstr3d	$⊢ (φ \land m \in ℕ) \to ball (D) (g (m + 1)) \subseteq ⋃ J$
91		eqid	$⊢ ⋃ J = ⋃ J$
92	91	sscls	$⊢ (J \in Top \land ball (D) (g (m + 1)) \subseteq ⋃ J) \to ball (D) (g (m + 1)) \subseteq cls (J) (ball (D) (g (m + 1)))$
93	75 90 92	syl2anc	$⊢ (φ \land m \in ℕ) \to ball (D) (g (m + 1)) \subseteq cls (J) (ball (D) (g (m + 1)))$
94	32	simp3d	$⊢ (φ \land m \in ℕ) \to cls (J) (ball (D) (g (m + 1))) \subseteq ball (D) (g (m)) ∖ M (m)$
95	93 94	sstrd	$⊢ (φ \land m \in ℕ) \to ball (D) (g (m + 1)) \subseteq ball (D) (g (m)) ∖ M (m)$
96	95	3adant2	$⊢ (φ \land (1^{st} \circ g) \underset{t}{⇝} (J) x \land m \in ℕ) \to ball (D) (g (m + 1)) \subseteq ball (D) (g (m)) ∖ M (m)$
97	1 2 3 4 5 6 7 8 9	bcthlem3	$⊢ (φ \land (1^{st} \circ g) \underset{t}{⇝} (J) x \land m + 1 \in ℕ) \to x \in ball (D) (g (m + 1))$
98	19 97	syl3an3	$⊢ (φ \land (1^{st} \circ g) \underset{t}{⇝} (J) x \land m \in ℕ) \to x \in ball (D) (g (m + 1))$
99	96 98	sseldd	$⊢ (φ \land (1^{st} \circ g) \underset{t}{⇝} (J) x \land m \in ℕ) \to x \in (ball (D) (g (m)) ∖ M (m))$
100	99	eldifbd	$⊢ (φ \land (1^{st} \circ g) \underset{t}{⇝} (J) x \land m \in ℕ) \to \neg x \in M (m)$
101	100	3expa	$⊢ ((φ \land (1^{st} \circ g) \underset{t}{⇝} (J) x) \land m \in ℕ) \to \neg x \in M (m)$
102	101	ralrimiva	$⊢ (φ \land (1^{st} \circ g) \underset{t}{⇝} (J) x) \to \forall m \in ℕ \neg x \in M (m)$
103		eluni2	$⊢ x \in ⋃ ran M \leftrightarrow \exists y \in ran M x \in y$
104	4	ffnd	$⊢ φ \to M Fn ℕ$
105		eleq2	$⊢ y = M (m) \to (x \in y \leftrightarrow x \in M (m))$
106	105	rexrn	$⊢ M Fn ℕ \to (\exists y \in ran M x \in y \leftrightarrow \exists m \in ℕ x \in M (m))$
107	104 106	syl	$⊢ φ \to (\exists y \in ran M x \in y \leftrightarrow \exists m \in ℕ x \in M (m))$
108	103 107	bitrid	$⊢ φ \to (x \in ⋃ ran M \leftrightarrow \exists m \in ℕ x \in M (m))$
109	108	notbid	$⊢ φ \to (\neg x \in ⋃ ran M \leftrightarrow \neg \exists m \in ℕ x \in M (m))$
110		ralnex	$⊢ \forall m \in ℕ \neg x \in M (m) \leftrightarrow \neg \exists m \in ℕ x \in M (m)$
111	109 110	bitr4di	$⊢ φ \to (\neg x \in ⋃ ran M \leftrightarrow \forall m \in ℕ \neg x \in M (m))$
112	111	biimpar	$⊢ (φ \land \forall m \in ℕ \neg x \in M (m)) \to \neg x \in ⋃ ran M$
113	102 112	syldan	$⊢ (φ \land (1^{st} \circ g) \underset{t}{⇝} (J) x) \to \neg x \in ⋃ ran M$
114	72 113	eldifd	$⊢ (φ \land (1^{st} \circ g) \underset{t}{⇝} (J) x) \to x \in ((C ball (D) R) ∖ ⋃ ran M)$
115	114	ne0d	$⊢ (φ \land (1^{st} \circ g) \underset{t}{⇝} (J) x) \to (C ball (D) R) ∖ ⋃ ran M \neq \emptyset$
116	64 115	exlimddv	$⊢ φ \to (C ball (D) R) ∖ ⋃ ran M \neq \emptyset$

Metamath Proof Explorer

Theorem bcthlem4

Proof