bcthlem5

Description: Lemma for bcth . The proof makes essential use of the Axiom of Dependent Choice axdc4uz , which in the form used here accepts a "selection" function F from each element of K to a nonempty subset of K , and the result function g maps g ( n + 1 ) to an element of F ( n , g ( n ) ) . The trick here is thus in the choice of F and K : we let K be the set of all tagged nonempty open sets (tagged here meaning that we have a point and an open set, in an ordered pair), and F ( k , <. x , z >. ) gives the set of all balls of size less than 1 / k , tagged by their centers, whose closures fit within the given open set z and miss M ( k ) .

Since M ( k ) is closed, z \ M ( k ) is open and also nonempty, since z is nonempty and M ( k ) has empty interior. Then there is some ball contained in it, and hence our function F is valid (it never maps to the empty set). Now starting at a point in the interior of U. ran M , DC gives us the function g all whose elements are constrained by F acting on the previous value. (This is all proven in this lemma.) Now g is a sequence of tagged open balls, forming an inclusion chain (see bcthlem2 ) and whose sizes tend to zero, since they are bounded above by 1 / k . Thus, the centers of these balls form a Cauchy sequence, and converge to a point x (see bcthlem4 ). Since the inclusion chain also ensures the closure of each ball is in the previous ball, the point x must be in all these balls (see bcthlem3 ) and hence misses each M ( k ) , contradicting the fact that x is in the interior of U. ran M (which was the starting point). (Contributed by Mario Carneiro, 6-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)$
	bcthlem5.7	$⊢ φ \to \forall k \in ℕ int (J) (M (k)) = \emptyset$
Assertion	bcthlem5	$⊢ φ \to int (J) (⋃ ran M) = \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		bcthlem5.7	$⊢ φ \to \forall k \in ℕ int (J) (M (k)) = \emptyset$
6		cmetmet	$⊢ D \in CMet (X) \to D \in Met (X)$
7		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
8	2 6 7	3syl	$⊢ φ \to D \in ∞Met (X)$
9	1	mopntop	$⊢ D \in ∞Met (X) \to J \in Top$
10	8 9	syl	$⊢ φ \to J \in Top$
11	4	frnd	$⊢ φ \to ran M \subseteq Clsd (J)$
12		eqid	$⊢ ⋃ J = ⋃ J$
13	12	cldss2	$⊢ Clsd (J) \subseteq 𝒫 ⋃ J$
14	11 13	sstrdi	$⊢ φ \to ran M \subseteq 𝒫 ⋃ J$
15		sspwuni	$⊢ ran M \subseteq 𝒫 ⋃ J \leftrightarrow ⋃ ran M \subseteq ⋃ J$
16	14 15	sylib	$⊢ φ \to ⋃ ran M \subseteq ⋃ J$
17	12	ntropn	$⊢ (J \in Top \land ⋃ ran M \subseteq ⋃ J) \to int (J) (⋃ ran M) \in J$
18	10 16 17	syl2anc	$⊢ φ \to int (J) (⋃ ran M) \in J$
19	8 18	jca	$⊢ φ \to (D \in ∞Met (X) \land int (J) (⋃ ran M) \in J)$
20	1	mopni2	$⊢ (D \in ∞Met (X) \land int (J) (⋃ ran M) \in J \land n \in int (J) (⋃ ran M)) \to \exists m \in ℝ^{+} n ball (D) m \subseteq int (J) (⋃ ran M)$
21	20	3expa	$⊢ ((D \in ∞Met (X) \land int (J) (⋃ ran M) \in J) \land n \in int (J) (⋃ ran M)) \to \exists m \in ℝ^{+} n ball (D) m \subseteq int (J) (⋃ ran M)$
22	19 21	sylan	$⊢ (φ \land n \in int (J) (⋃ ran M)) \to \exists m \in ℝ^{+} n ball (D) m \subseteq int (J) (⋃ ran M)$
23	1	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
24	8 23	syl	$⊢ φ \to X = ⋃ J$
25	12	topopn	$⊢ J \in Top \to ⋃ J \in J$
26	10 25	syl	$⊢ φ \to ⋃ J \in J$
27	24 26	eqeltrd	$⊢ φ \to X \in J$
28		reex	$⊢ ℝ \in V$
29		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
30	28 29	ssexi	$⊢ ℝ^{+} \in V$
31		xpexg	$⊢ (X \in J \land ℝ^{+} \in V) \to X \times ℝ^{+} \in V$
32	27 30 31	sylancl	$⊢ φ \to X \times ℝ^{+} \in V$
33	32	3ad2ant1	$⊢ (φ \land n \in int (J) (⋃ ran M) \land m \in ℝ^{+}) \to X \times ℝ^{+} \in V$
34	12	ntrss3	$⊢ (J \in Top \land ⋃ ran M \subseteq ⋃ J) \to int (J) (⋃ ran M) \subseteq ⋃ J$
35	10 16 34	syl2anc	$⊢ φ \to int (J) (⋃ ran M) \subseteq ⋃ J$
36	35 24	sseqtrrd	$⊢ φ \to int (J) (⋃ ran M) \subseteq X$
37	36	3ad2ant1	$⊢ (φ \land n \in int (J) (⋃ ran M) \land m \in ℝ^{+}) \to int (J) (⋃ ran M) \subseteq X$
38		simp2	$⊢ (φ \land n \in int (J) (⋃ ran M) \land m \in ℝ^{+}) \to n \in int (J) (⋃ ran M)$
39	37 38	sseldd	$⊢ (φ \land n \in int (J) (⋃ ran M) \land m \in ℝ^{+}) \to n \in X$
40		simp3	$⊢ (φ \land n \in int (J) (⋃ ran M) \land m \in ℝ^{+}) \to m \in ℝ^{+}$
41	39 40	opelxpd	$⊢ (φ \land n \in int (J) (⋃ ran M) \land m \in ℝ^{+}) \to ⟨n, m⟩ \in (X \times ℝ^{+})$
42		opabssxp	$⊢ \{⟨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)))\} \subseteq X \times ℝ^{+}$
43		elpw2g	$⊢ X \times ℝ^{+} \in V \to (\{⟨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)))\} \in 𝒫 (X \times ℝ^{+}) \leftrightarrow \{⟨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)))\} \subseteq X \times ℝ^{+})$
44	32 43	syl	$⊢ φ \to (\{⟨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)))\} \in 𝒫 (X \times ℝ^{+}) \leftrightarrow \{⟨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)))\} \subseteq X \times ℝ^{+})$
45	44	adantr	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to (\{⟨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)))\} \in 𝒫 (X \times ℝ^{+}) \leftrightarrow \{⟨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)))\} \subseteq X \times ℝ^{+})$
46	42 45	mpbiri	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to \{⟨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)))\} \in 𝒫 (X \times ℝ^{+})$
47		simpl	$⊢ (k \in ℕ \land z \in (X \times ℝ^{+})) \to k \in ℕ$
48		rspa	$⊢ (\forall k \in ℕ int (J) (M (k)) = \emptyset \land k \in ℕ) \to int (J) (M (k)) = \emptyset$
49	5 47 48	syl2an	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to int (J) (M (k)) = \emptyset$
50		ssdif0	$⊢ ball (D) (z) \subseteq M (k) \leftrightarrow ball (D) (z) ∖ M (k) = \emptyset$
51		1st2nd2	$⊢ z \in (X \times ℝ^{+}) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
52	51	ad2antll	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
53	52	fveq2d	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to ball (D) (z) = ball (D) (⟨1^{st} (z), 2^{nd} (z)⟩)$
54		df-ov	$⊢ 1^{st} (z) ball (D) 2^{nd} (z) = ball (D) (⟨1^{st} (z), 2^{nd} (z)⟩)$
55	53 54	eqtr4di	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to ball (D) (z) = 1^{st} (z) ball (D) 2^{nd} (z)$
56	8	adantr	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to D \in ∞Met (X)$
57		xp1st	$⊢ z \in (X \times ℝ^{+}) \to 1^{st} (z) \in X$
58	57	ad2antll	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to 1^{st} (z) \in X$
59		xp2nd	$⊢ z \in (X \times ℝ^{+}) \to 2^{nd} (z) \in ℝ^{+}$
60	59	ad2antll	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to 2^{nd} (z) \in ℝ^{+}$
61		bln0	$⊢ (D \in ∞Met (X) \land 1^{st} (z) \in X \land 2^{nd} (z) \in ℝ^{+}) \to 1^{st} (z) ball (D) 2^{nd} (z) \neq \emptyset$
62	56 58 60 61	syl3anc	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to 1^{st} (z) ball (D) 2^{nd} (z) \neq \emptyset$
63	55 62	eqnetrd	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to ball (D) (z) \neq \emptyset$
64	10	adantr	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to J \in Top$
65		ffvelrn	$⊢ (M : ℕ ⟶ Clsd (J) \land k \in ℕ) \to M (k) \in Clsd (J)$
66	4 47 65	syl2an	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to M (k) \in Clsd (J)$
67	12	cldss	$⊢ M (k) \in Clsd (J) \to M (k) \subseteq ⋃ J$
68	66 67	syl	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to M (k) \subseteq ⋃ J$
69	60	rpxrd	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to 2^{nd} (z) \in ℝ^{*}$
70	1	blopn	$⊢ (D \in ∞Met (X) \land 1^{st} (z) \in X \land 2^{nd} (z) \in ℝ^{*}) \to 1^{st} (z) ball (D) 2^{nd} (z) \in J$
71	56 58 69 70	syl3anc	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to 1^{st} (z) ball (D) 2^{nd} (z) \in J$
72	55 71	eqeltrd	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to ball (D) (z) \in J$
73	12	ssntr	$⊢ ((J \in Top \land M (k) \subseteq ⋃ J) \land (ball (D) (z) \in J \land ball (D) (z) \subseteq M (k))) \to ball (D) (z) \subseteq int (J) (M (k))$
74	73	expr	$⊢ ((J \in Top \land M (k) \subseteq ⋃ J) \land ball (D) (z) \in J) \to (ball (D) (z) \subseteq M (k) \to ball (D) (z) \subseteq int (J) (M (k)))$
75	64 68 72 74	syl21anc	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to (ball (D) (z) \subseteq M (k) \to ball (D) (z) \subseteq int (J) (M (k)))$
76		ssn0	$⊢ (ball (D) (z) \subseteq int (J) (M (k)) \land ball (D) (z) \neq \emptyset) \to int (J) (M (k)) \neq \emptyset$
77	76	expcom	$⊢ ball (D) (z) \neq \emptyset \to (ball (D) (z) \subseteq int (J) (M (k)) \to int (J) (M (k)) \neq \emptyset)$
78	63 75 77	sylsyld	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to (ball (D) (z) \subseteq M (k) \to int (J) (M (k)) \neq \emptyset)$
79	50 78	syl5bir	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to (ball (D) (z) ∖ M (k) = \emptyset \to int (J) (M (k)) \neq \emptyset)$
80	79	necon2d	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to (int (J) (M (k)) = \emptyset \to ball (D) (z) ∖ M (k) \neq \emptyset)$
81	49 80	mpd	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to ball (D) (z) ∖ M (k) \neq \emptyset$
82		n0	$⊢ ball (D) (z) ∖ M (k) \neq \emptyset \leftrightarrow \exists x x \in (ball (D) (z) ∖ M (k))$
83	8	3ad2ant1	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+})) \land x \in (ball (D) (z) ∖ M (k))) \to D \in ∞Met (X)$
84	12	difopn	$⊢ (ball (D) (z) \in J \land M (k) \in Clsd (J)) \to ball (D) (z) ∖ M (k) \in J$
85	72 66 84	syl2anc	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to ball (D) (z) ∖ M (k) \in J$
86	85	3adant3	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+})) \land x \in (ball (D) (z) ∖ M (k))) \to ball (D) (z) ∖ M (k) \in J$
87		simp3	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+})) \land x \in (ball (D) (z) ∖ M (k))) \to x \in (ball (D) (z) ∖ M (k))$
88		simp2l	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+})) \land x \in (ball (D) (z) ∖ M (k))) \to k \in ℕ$
89		nnrp	$⊢ k \in ℕ \to k \in ℝ^{+}$
90	89	rpreccld	$⊢ k \in ℕ \to \frac{1}{k} \in ℝ^{+}$
91	88 90	syl	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+})) \land x \in (ball (D) (z) ∖ M (k))) \to \frac{1}{k} \in ℝ^{+}$
92	1	mopni3	$⊢ ((D \in ∞Met (X) \land ball (D) (z) ∖ M (k) \in J \land x \in (ball (D) (z) ∖ M (k))) \land \frac{1}{k} \in ℝ^{+}) \to \exists n \in ℝ^{+} (n < \frac{1}{k} \land x ball (D) n \subseteq ball (D) (z) ∖ M (k))$
93	83 86 87 91 92	syl31anc	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+})) \land x \in (ball (D) (z) ∖ M (k))) \to \exists n \in ℝ^{+} (n < \frac{1}{k} \land x ball (D) n \subseteq ball (D) (z) ∖ M (k))$
94		simp1	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+})) \land x \in (ball (D) (z) ∖ M (k))) \to φ$
95		elssuni	$⊢ ball (D) (z) \in J \to ball (D) (z) \subseteq ⋃ J$
96	72 95	syl	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to ball (D) (z) \subseteq ⋃ J$
97	24	adantr	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to X = ⋃ J$
98	96 97	sseqtrrd	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to ball (D) (z) \subseteq X$
99	98	ssdifssd	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to ball (D) (z) ∖ M (k) \subseteq X$
100	99	sseld	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to (x \in (ball (D) (z) ∖ M (k)) \to x \in X)$
101	100	3impia	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+})) \land x \in (ball (D) (z) ∖ M (k))) \to x \in X$
102		simp2	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+})) \land x \in (ball (D) (z) ∖ M (k))) \to (k \in ℕ \land z \in (X \times ℝ^{+}))$
103		rphalfcl	$⊢ n \in ℝ^{+} \to \frac{n}{2} \in ℝ^{+}$
104		rphalflt	$⊢ n \in ℝ^{+} \to \frac{n}{2} < n$
105		breq1	$⊢ r = \frac{n}{2} \to (r < n \leftrightarrow \frac{n}{2} < n)$
106	105	rspcev	$⊢ (\frac{n}{2} \in ℝ^{+} \land \frac{n}{2} < n) \to \exists r \in ℝ^{+} r < n$
107	103 104 106	syl2anc	$⊢ n \in ℝ^{+} \to \exists r \in ℝ^{+} r < n$
108	107	ad2antlr	$⊢ ((((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \land n \in ℝ^{+}) \land (n < \frac{1}{k} \land x ball (D) n \subseteq ball (D) (z) ∖ M (k))) \to \exists r \in ℝ^{+} r < n$
109		df-rex	$⊢ \exists r \in ℝ^{+} r < n \leftrightarrow \exists r (r \in ℝ^{+} \land r < n)$
110		simpr3	$⊢ (((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \land (n \in ℝ^{+} \land r < n \land r \in ℝ^{+})) \to r \in ℝ^{+}$
111	110	rpred	$⊢ (((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \land (n \in ℝ^{+} \land r < n \land r \in ℝ^{+})) \to r \in ℝ$
112		simpr1	$⊢ (((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \land (n \in ℝ^{+} \land r < n \land r \in ℝ^{+})) \to n \in ℝ^{+}$
113	112	rpred	$⊢ (((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \land (n \in ℝ^{+} \land r < n \land r \in ℝ^{+})) \to n \in ℝ$
114		simplrl	$⊢ (((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \land (n \in ℝ^{+} \land r < n \land r \in ℝ^{+})) \to k \in ℕ$
115	114	nnrecred	$⊢ (((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \land (n \in ℝ^{+} \land r < n \land r \in ℝ^{+})) \to \frac{1}{k} \in ℝ$
116		simpr2	$⊢ (((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \land (n \in ℝ^{+} \land r < n \land r \in ℝ^{+})) \to r < n$
117		lttr	$⊢ (r \in ℝ \land n \in ℝ \land \frac{1}{k} \in ℝ) \to ((r < n \land n < \frac{1}{k}) \to r < \frac{1}{k})$
118	117	expdimp	$⊢ ((r \in ℝ \land n \in ℝ \land \frac{1}{k} \in ℝ) \land r < n) \to (n < \frac{1}{k} \to r < \frac{1}{k})$
119	111 113 115 116 118	syl31anc	$⊢ (((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \land (n \in ℝ^{+} \land r < n \land r \in ℝ^{+})) \to (n < \frac{1}{k} \to r < \frac{1}{k})$
120	8	anim1i	$⊢ (φ \land x \in X) \to (D \in ∞Met (X) \land x \in X)$
121	120	adantr	$⊢ ((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to (D \in ∞Met (X) \land x \in X)$
122		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
123		rpxr	$⊢ n \in ℝ^{+} \to n \in ℝ^{*}$
124		id	$⊢ r < n \to r < n$
125	122 123 124	3anim123i	$⊢ (r \in ℝ^{+} \land n \in ℝ^{+} \land r < n) \to (r \in ℝ^{} \land n \in ℝ^{} \land r < n)$
126	125	3coml	$⊢ (n \in ℝ^{+} \land r < n \land r \in ℝ^{+}) \to (r \in ℝ^{} \land n \in ℝ^{} \land r < n)$
127	1	blsscls	$⊢ ((D \in ∞Met (X) \land x \in X) \land (r \in ℝ^{} \land n \in ℝ^{} \land r < n)) \to cls (J) (x ball (D) r) \subseteq x ball (D) n$
128	121 126 127	syl2an	$⊢ (((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \land (n \in ℝ^{+} \land r < n \land r \in ℝ^{+})) \to cls (J) (x ball (D) r) \subseteq x ball (D) n$
129		sstr2	$⊢ cls (J) (x ball (D) r) \subseteq x ball (D) n \to (x ball (D) n \subseteq ball (D) (z) ∖ M (k) \to cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (k))$
130	128 129	syl	$⊢ (((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \land (n \in ℝ^{+} \land r < n \land r \in ℝ^{+})) \to (x ball (D) n \subseteq ball (D) (z) ∖ M (k) \to cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (k))$
131	119 130	anim12d	$⊢ (((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \land (n \in ℝ^{+} \land r < n \land r \in ℝ^{+})) \to ((n < \frac{1}{k} \land x ball (D) n \subseteq ball (D) (z) ∖ M (k)) \to (r < \frac{1}{k} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (k)))$
132		simpllr	$⊢ (((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \land (n \in ℝ^{+} \land r < n \land r \in ℝ^{+})) \to x \in X$
133	132 110	jca	$⊢ (((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \land (n \in ℝ^{+} \land r < n \land r \in ℝ^{+})) \to (x \in X \land r \in ℝ^{+})$
134	131 133	jctild	$⊢ (((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \land (n \in ℝ^{+} \land r < n \land r \in ℝ^{+})) \to ((n < \frac{1}{k} \land x ball (D) n \subseteq ball (D) (z) ∖ M (k)) \to ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{k} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (k))))$
135	134	3exp2	$⊢ ((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to (n \in ℝ^{+} \to (r < n \to (r \in ℝ^{+} \to ((n < \frac{1}{k} \land x ball (D) n \subseteq ball (D) (z) ∖ M (k)) \to ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{k} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (k)))))))$
136	135	com35	$⊢ ((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to (n \in ℝ^{+} \to ((n < \frac{1}{k} \land x ball (D) n \subseteq ball (D) (z) ∖ M (k)) \to (r \in ℝ^{+} \to (r < n \to ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{k} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (k)))))))$
137	136	imp5d	$⊢ ((((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \land n \in ℝ^{+}) \land (n < \frac{1}{k} \land x ball (D) n \subseteq ball (D) (z) ∖ M (k))) \to ((r \in ℝ^{+} \land r < n) \to ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{k} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (k))))$
138	137	eximdv	$⊢ ((((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \land n \in ℝ^{+}) \land (n < \frac{1}{k} \land x ball (D) n \subseteq ball (D) (z) ∖ M (k))) \to (\exists r (r \in ℝ^{+} \land r < n) \to \exists 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))))$
139	109 138	syl5bi	$⊢ ((((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \land n \in ℝ^{+}) \land (n < \frac{1}{k} \land x ball (D) n \subseteq ball (D) (z) ∖ M (k))) \to (\exists r \in ℝ^{+} r < n \to \exists 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))))$
140	108 139	mpd	$⊢ ((((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \land n \in ℝ^{+}) \land (n < \frac{1}{k} \land x ball (D) n \subseteq ball (D) (z) ∖ M (k))) \to \exists 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)))$
141	140	rexlimdva2	$⊢ ((φ \land x \in X) \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to (\exists n \in ℝ^{+} (n < \frac{1}{k} \land x ball (D) n \subseteq ball (D) (z) ∖ M (k)) \to \exists 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))))$
142	94 101 102 141	syl21anc	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+})) \land x \in (ball (D) (z) ∖ M (k))) \to (\exists n \in ℝ^{+} (n < \frac{1}{k} \land x ball (D) n \subseteq ball (D) (z) ∖ M (k)) \to \exists 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))))$
143	93 142	mpd	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+})) \land x \in (ball (D) (z) ∖ M (k))) \to \exists 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)))$
144	143	3expia	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to (x \in (ball (D) (z) ∖ M (k)) \to \exists 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))))$
145	144	eximdv	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to (\exists x x \in (ball (D) (z) ∖ M (k)) \to \exists x \exists 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))))$
146	82 145	syl5bi	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to (ball (D) (z) ∖ M (k) \neq \emptyset \to \exists x \exists 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))))$
147	81 146	mpd	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to \exists x \exists 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)))$
148		opabn0	$⊢ \{⟨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)))\} \neq \emptyset \leftrightarrow \exists x \exists 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)))$
149	147 148	sylibr	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to \{⟨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)))\} \neq \emptyset$
150		eldifsn	$⊢ \{⟨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)))\} \in (𝒫 (X \times ℝ^{+}) ∖ \{\emptyset\}) \leftrightarrow (\{⟨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)))\} \in 𝒫 (X \times ℝ^{+}) \land \{⟨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)))\} \neq \emptyset)$
151	46 149 150	sylanbrc	$⊢ (φ \land (k \in ℕ \land z \in (X \times ℝ^{+}))) \to \{⟨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)))\} \in (𝒫 (X \times ℝ^{+}) ∖ \{\emptyset\})$
152	151	ralrimivva	$⊢ φ \to \forall k \in ℕ \forall 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)))\} \in (𝒫 (X \times ℝ^{+}) ∖ \{\emptyset\})$
153	3	fmpo	$⊢ \forall k \in ℕ \forall 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)))\} \in (𝒫 (X \times ℝ^{+}) ∖ \{\emptyset\}) \leftrightarrow F : ℕ \times (X \times ℝ^{+}) ⟶ 𝒫 (X \times ℝ^{+}) ∖ \{\emptyset\}$
154	152 153	sylib	$⊢ φ \to F : ℕ \times (X \times ℝ^{+}) ⟶ 𝒫 (X \times ℝ^{+}) ∖ \{\emptyset\}$
155	154	3ad2ant1	$⊢ (φ \land n \in int (J) (⋃ ran M) \land m \in ℝ^{+}) \to F : ℕ \times (X \times ℝ^{+}) ⟶ 𝒫 (X \times ℝ^{+}) ∖ \{\emptyset\}$
156		1z	$⊢ 1 \in ℤ$
157		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
158	156 157	axdc4uz	$⊢ (X \times ℝ^{+} \in V \land ⟨n, m⟩ \in (X \times ℝ^{+}) \land F : ℕ \times (X \times ℝ^{+}) ⟶ 𝒫 (X \times ℝ^{+}) ∖ \{\emptyset\}) \to \exists g (g : ℕ ⟶ X \times ℝ^{+} \land g (1) = ⟨n, m⟩ \land \forall n \in ℕ g (n + 1) \in (n F g (n)))$
159	33 41 155 158	syl3anc	$⊢ (φ \land n \in int (J) (⋃ ran M) \land m \in ℝ^{+}) \to \exists g (g : ℕ ⟶ X \times ℝ^{+} \land g (1) = ⟨n, m⟩ \land \forall n \in ℕ g (n + 1) \in (n F g (n)))$
160		simpl1	$⊢ ((φ \land n \in int (J) (⋃ ran M) \land m \in ℝ^{+}) \land (g : ℕ ⟶ X \times ℝ^{+} \land g (1) = ⟨n, m⟩ \land \forall n \in ℕ g (n + 1) \in (n F g (n)))) \to φ$
161	160 2	syl	$⊢ ((φ \land n \in int (J) (⋃ ran M) \land m \in ℝ^{+}) \land (g : ℕ ⟶ X \times ℝ^{+} \land g (1) = ⟨n, m⟩ \land \forall n \in ℕ g (n + 1) \in (n F g (n)))) \to D \in CMet (X)$
162	160 4	syl	$⊢ ((φ \land n \in int (J) (⋃ ran M) \land m \in ℝ^{+}) \land (g : ℕ ⟶ X \times ℝ^{+} \land g (1) = ⟨n, m⟩ \land \forall n \in ℕ g (n + 1) \in (n F g (n)))) \to M : ℕ ⟶ Clsd (J)$
163		simpl3	$⊢ ((φ \land n \in int (J) (⋃ ran M) \land m \in ℝ^{+}) \land (g : ℕ ⟶ X \times ℝ^{+} \land g (1) = ⟨n, m⟩ \land \forall n \in ℕ g (n + 1) \in (n F g (n)))) \to m \in ℝ^{+}$
164	39	adantr	$⊢ ((φ \land n \in int (J) (⋃ ran M) \land m \in ℝ^{+}) \land (g : ℕ ⟶ X \times ℝ^{+} \land g (1) = ⟨n, m⟩ \land \forall n \in ℕ g (n + 1) \in (n F g (n)))) \to n \in X$
165		simpr1	$⊢ ((φ \land n \in int (J) (⋃ ran M) \land m \in ℝ^{+}) \land (g : ℕ ⟶ X \times ℝ^{+} \land g (1) = ⟨n, m⟩ \land \forall n \in ℕ g (n + 1) \in (n F g (n)))) \to g : ℕ ⟶ X \times ℝ^{+}$
166		simpr2	$⊢ ((φ \land n \in int (J) (⋃ ran M) \land m \in ℝ^{+}) \land (g : ℕ ⟶ X \times ℝ^{+} \land g (1) = ⟨n, m⟩ \land \forall n \in ℕ g (n + 1) \in (n F g (n)))) \to g (1) = ⟨n, m⟩$
167		simpr3	$⊢ ((φ \land n \in int (J) (⋃ ran M) \land m \in ℝ^{+}) \land (g : ℕ ⟶ X \times ℝ^{+} \land g (1) = ⟨n, m⟩ \land \forall n \in ℕ g (n + 1) \in (n F g (n)))) \to \forall n \in ℕ g (n + 1) \in (n F g (n))$
168		fvoveq1	$⊢ n = k \to g (n + 1) = g (k + 1)$
169		id	$⊢ n = k \to n = k$
170		fveq2	$⊢ n = k \to g (n) = g (k)$
171	169 170	oveq12d	$⊢ n = k \to n F g (n) = k F g (k)$
172	168 171	eleq12d	$⊢ n = k \to (g (n + 1) \in (n F g (n)) \leftrightarrow g (k + 1) \in (k F g (k)))$
173	172	cbvralvw	$⊢ \forall n \in ℕ g (n + 1) \in (n F g (n)) \leftrightarrow \forall k \in ℕ g (k + 1) \in (k F g (k))$
174	167 173	sylib	$⊢ ((φ \land n \in int (J) (⋃ ran M) \land m \in ℝ^{+}) \land (g : ℕ ⟶ X \times ℝ^{+} \land g (1) = ⟨n, m⟩ \land \forall n \in ℕ g (n + 1) \in (n F g (n)))) \to \forall k \in ℕ g (k + 1) \in (k F g (k))$
175	1 161 3 162 163 164 165 166 174	bcthlem4	$⊢ ((φ \land n \in int (J) (⋃ ran M) \land m \in ℝ^{+}) \land (g : ℕ ⟶ X \times ℝ^{+} \land g (1) = ⟨n, m⟩ \land \forall n \in ℕ g (n + 1) \in (n F g (n)))) \to (n ball (D) m) ∖ ⋃ ran M \neq \emptyset$
176	159 175	exlimddv	$⊢ (φ \land n \in int (J) (⋃ ran M) \land m \in ℝ^{+}) \to (n ball (D) m) ∖ ⋃ ran M \neq \emptyset$
177	12	ntrss2	$⊢ (J \in Top \land ⋃ ran M \subseteq ⋃ J) \to int (J) (⋃ ran M) \subseteq ⋃ ran M$
178	10 16 177	syl2anc	$⊢ φ \to int (J) (⋃ ran M) \subseteq ⋃ ran M$
179		sstr2	$⊢ n ball (D) m \subseteq int (J) (⋃ ran M) \to (int (J) (⋃ ran M) \subseteq ⋃ ran M \to n ball (D) m \subseteq ⋃ ran M)$
180	178 179	syl5com	$⊢ φ \to (n ball (D) m \subseteq int (J) (⋃ ran M) \to n ball (D) m \subseteq ⋃ ran M)$
181		ssdif0	$⊢ n ball (D) m \subseteq ⋃ ran M \leftrightarrow (n ball (D) m) ∖ ⋃ ran M = \emptyset$
182	180 181	syl6ib	$⊢ φ \to (n ball (D) m \subseteq int (J) (⋃ ran M) \to (n ball (D) m) ∖ ⋃ ran M = \emptyset)$
183	182	necon3ad	$⊢ φ \to ((n ball (D) m) ∖ ⋃ ran M \neq \emptyset \to \neg n ball (D) m \subseteq int (J) (⋃ ran M))$
184	183	3ad2ant1	$⊢ (φ \land n \in int (J) (⋃ ran M) \land m \in ℝ^{+}) \to ((n ball (D) m) ∖ ⋃ ran M \neq \emptyset \to \neg n ball (D) m \subseteq int (J) (⋃ ran M))$
185	176 184	mpd	$⊢ (φ \land n \in int (J) (⋃ ran M) \land m \in ℝ^{+}) \to \neg n ball (D) m \subseteq int (J) (⋃ ran M)$
186	185	3expa	$⊢ ((φ \land n \in int (J) (⋃ ran M)) \land m \in ℝ^{+}) \to \neg n ball (D) m \subseteq int (J) (⋃ ran M)$
187	186	nrexdv	$⊢ (φ \land n \in int (J) (⋃ ran M)) \to \neg \exists m \in ℝ^{+} n ball (D) m \subseteq int (J) (⋃ ran M)$
188	22 187	pm2.65da	$⊢ φ \to \neg n \in int (J) (⋃ ran M)$
189	188	eq0rdv	$⊢ φ \to int (J) (⋃ ran M) = \emptyset$

Metamath Proof Explorer

Theorem bcthlem5

Proof