Theorem bcthlem5 22933

Description: Lemma for bcth 22934. The proof makes essential use of the Axiom of Dependent Choice axdc4uz 12645, which in the form used here accepts a "selection" function 𝐹 from each element of 𝐾 to a nonempty subset of 𝐾, and the result function 𝑔 maps 𝑔(𝑛 + 1) to an element of 𝐹(𝑛, 𝑔(𝑛)). The trick here is thus in the choice of 𝐹 and 𝐾: we let 𝐾 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 𝐹(𝑘, ⟨𝑥, 𝑧⟩) gives the set of all balls of size less than 1 / 𝑘, tagged by their centers, whose closures fit within the given open set 𝑧 and miss 𝑀(𝑘).

Since 𝑀(𝑘) is closed, 𝑧 ∖ 𝑀(𝑘) is open and also nonempty, since 𝑧 is nonempty and 𝑀(𝑘) has empty interior. Then there is some ball contained in it, and hence our function 𝐹 is valid (it never maps to the empty set). Now starting at a point in the interior of ∪ ran 𝑀, DC gives us the function 𝑔 all whose elements are constrained by 𝐹 acting on the previous value. (This is all proven in this lemma.) Now 𝑔 is a sequence of tagged open balls, forming an inclusion chain (see bcthlem2 22930) and whose sizes tend to zero, since they are bounded above by 1 / 𝑘. Thus, the centers of these balls form a Cauchy sequence, and converge to a point 𝑥 (see bcthlem4 22932). Since the inclusion chain also ensures the closure of each ball is in the previous ball, the point 𝑥 must be in all these balls (see bcthlem3 22931) and hence misses each 𝑀(𝑘), contradicting the fact that 𝑥 is in the interior of ∪ ran 𝑀 (which was the starting point). (Contributed by Mario Carneiro, 6-Jan-2014.)

Hypotheses

Ref	Expression
bcth.2	⊢ 𝐽 = (MetOpen‘𝐷)
bcthlem.4	⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
bcthlem.5	⊢ 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦ {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))})
bcthlem.6	⊢ (𝜑 → 𝑀:ℕ⟶(Clsd‘𝐽))
bcthlem5.7	⊢ (𝜑 → ∀𝑘 ∈ ℕ ((int‘𝐽)‘(𝑀‘𝑘)) = ∅)

Assertion

Ref	Expression
bcthlem5	⊢ (𝜑 → ((int‘𝐽)‘∪ ran 𝑀) = ∅)

Distinct variable groups:   𝑘,𝑟,𝑥,𝑧,𝐷   𝑘,𝐹,𝑟,𝑥,𝑧   𝑘,𝐽,𝑟,𝑥,𝑧   𝑘,𝑀,𝑟,𝑥,𝑧   𝜑,𝑘,𝑟,𝑥,𝑧   𝑘,𝑋,𝑟,𝑥,𝑧

Proof of Theorem bcthlem5

Dummy variables 𝑛 𝑔 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		bcthlem.4	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
2		cmetmet 22892	. . . . . 6 ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
3		metxmet 21949	. . . . . 6 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
4	1, 2, 3	3syl 18	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
5		bcth.2	. . . . . . . 8 ⊢ 𝐽 = (MetOpen‘𝐷)
6	5	mopntop 22055	. . . . . . 7 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
7	4, 6	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ Top)
8		bcthlem.6	. . . . . . . . 9 ⊢ (𝜑 → 𝑀:ℕ⟶(Clsd‘𝐽))
9		frn 5966	. . . . . . . . 9 ⊢ (𝑀:ℕ⟶(Clsd‘𝐽) → ran 𝑀 ⊆ (Clsd‘𝐽))
10	8, 9	syl 17	. . . . . . . 8 ⊢ (𝜑 → ran 𝑀 ⊆ (Clsd‘𝐽))
11		eqid 2610	. . . . . . . . 9 ⊢ ∪ 𝐽 = ∪ 𝐽
12	11	cldss2 20644	. . . . . . . 8 ⊢ (Clsd‘𝐽) ⊆ 𝒫 ∪ 𝐽
13	10, 12	syl6ss 3580	. . . . . . 7 ⊢ (𝜑 → ran 𝑀 ⊆ 𝒫 ∪ 𝐽)
14		sspwuni 4547	. . . . . . 7 ⊢ (ran 𝑀 ⊆ 𝒫 ∪ 𝐽 ↔ ∪ ran 𝑀 ⊆ ∪ 𝐽)
15	13, 14	sylib 207	. . . . . 6 ⊢ (𝜑 → ∪ ran 𝑀 ⊆ ∪ 𝐽)
16	11	ntropn 20663	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ ∪ ran 𝑀 ⊆ ∪ 𝐽) → ((int‘𝐽)‘∪ ran 𝑀) ∈ 𝐽)
17	7, 15, 16	syl2anc 691	. . . . 5 ⊢ (𝜑 → ((int‘𝐽)‘∪ ran 𝑀) ∈ 𝐽)
18	4, 17	jca 553	. . . 4 ⊢ (𝜑 → (𝐷 ∈ (∞Met‘𝑋) ∧ ((int‘𝐽)‘∪ ran 𝑀) ∈ 𝐽))
19	5	mopni2 22108	. . . . 5 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((int‘𝐽)‘∪ ran 𝑀) ∈ 𝐽 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀)) → ∃𝑚 ∈ ℝ+ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘∪ ran 𝑀))
20	19	3expa 1257	. . . 4 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ ((int‘𝐽)‘∪ ran 𝑀) ∈ 𝐽) ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀)) → ∃𝑚 ∈ ℝ+ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘∪ ran 𝑀))
21	18, 20	sylan 487	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀)) → ∃𝑚 ∈ ℝ+ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘∪ ran 𝑀))
22	5	mopnuni 22056	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽)
23	4, 22	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
24	11	topopn 20536	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
25	7, 24	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ 𝐽 ∈ 𝐽)
26	23, 25	eqeltrd 2688	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ 𝐽)
27		reex 9906	. . . . . . . . . . 11 ⊢ ℝ ∈ V
28		rpssre 11719	. . . . . . . . . . 11 ⊢ ℝ+ ⊆ ℝ
29	27, 28	ssexi 4731	. . . . . . . . . 10 ⊢ ℝ+ ∈ V
30		xpexg 6858	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝐽 ∧ ℝ+ ∈ V) → (𝑋 × ℝ+) ∈ V)
31	26, 29, 30	sylancl 693	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 × ℝ+) ∈ V)
32	31	3ad2ant1 1075	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → (𝑋 × ℝ+) ∈ V)
33	11	ntrss3 20674	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ∪ ran 𝑀 ⊆ ∪ 𝐽) → ((int‘𝐽)‘∪ ran 𝑀) ⊆ ∪ 𝐽)
34	7, 15, 33	syl2anc 691	. . . . . . . . . . . 12 ⊢ (𝜑 → ((int‘𝐽)‘∪ ran 𝑀) ⊆ ∪ 𝐽)
35	34, 23	sseqtr4d 3605	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘𝐽)‘∪ ran 𝑀) ⊆ 𝑋)
36	35	3ad2ant1 1075	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → ((int‘𝐽)‘∪ ran 𝑀) ⊆ 𝑋)
37		simp2 1055	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀))
38	36, 37	sseldd 3569	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → 𝑛 ∈ 𝑋)
39		simp3 1056	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → 𝑚 ∈ ℝ+)
40		opelxpi 5072	. . . . . . . . 9 ⊢ ((𝑛 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+) → ⟨𝑛, 𝑚⟩ ∈ (𝑋 × ℝ+))
41	38, 39, 40	syl2anc 691	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → ⟨𝑛, 𝑚⟩ ∈ (𝑋 × ℝ+))
42		opabssxp 5116	. . . . . . . . . . . . 13 ⊢ {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ⊆ (𝑋 × ℝ+)
43		elpw2g 4754	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 × ℝ+) ∈ V → ({⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ∈ 𝒫 (𝑋 × ℝ+) ↔ {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ⊆ (𝑋 × ℝ+)))
44	31, 43	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ({⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ∈ 𝒫 (𝑋 × ℝ+) ↔ {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ⊆ (𝑋 × ℝ+)))
45	44	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ({⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ∈ 𝒫 (𝑋 × ℝ+) ↔ {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ⊆ (𝑋 × ℝ+)))
46	42, 45	mpbiri 247	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ∈ 𝒫 (𝑋 × ℝ+))
47		bcthlem5.7	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑘 ∈ ℕ ((int‘𝐽)‘(𝑀‘𝑘)) = ∅)
48		simpl 472	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) → 𝑘 ∈ ℕ)
49		rspa 2914	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑘 ∈ ℕ ((int‘𝐽)‘(𝑀‘𝑘)) = ∅ ∧ 𝑘 ∈ ℕ) → ((int‘𝐽)‘(𝑀‘𝑘)) = ∅)
50	47, 48, 49	syl2an 493	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((int‘𝐽)‘(𝑀‘𝑘)) = ∅)
51		ssdif0 3896	. . . . . . . . . . . . . . . . 17 ⊢ (((ball‘𝐷)‘𝑧) ⊆ (𝑀‘𝑘) ↔ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) = ∅)
52		1st2nd2 7096	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ (𝑋 × ℝ+) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
53	52	ad2antll 761	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
54	53	fveq2d 6107	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((ball‘𝐷)‘𝑧) = ((ball‘𝐷)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
55		df-ov 6552	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1st ‘𝑧)(ball‘𝐷)(2nd ‘𝑧)) = ((ball‘𝐷)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
56	54, 55	syl6eqr 2662	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((ball‘𝐷)‘𝑧) = ((1st ‘𝑧)(ball‘𝐷)(2nd ‘𝑧)))
57	4	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → 𝐷 ∈ (∞Met‘𝑋))
58		xp1st 7089	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ (𝑋 × ℝ+) → (1st ‘𝑧) ∈ 𝑋)
59	58	ad2antll 761	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (1st ‘𝑧) ∈ 𝑋)
60		xp2nd 7090	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ (𝑋 × ℝ+) → (2nd ‘𝑧) ∈ ℝ+)
61	60	ad2antll 761	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (2nd ‘𝑧) ∈ ℝ+)
62		bln0 22030	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (1st ‘𝑧) ∈ 𝑋 ∧ (2nd ‘𝑧) ∈ ℝ+) → ((1st ‘𝑧)(ball‘𝐷)(2nd ‘𝑧)) ≠ ∅)
63	57, 59, 61, 62	syl3anc 1318	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((1st ‘𝑧)(ball‘𝐷)(2nd ‘𝑧)) ≠ ∅)
64	56, 63	eqnetrd 2849	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((ball‘𝐷)‘𝑧) ≠ ∅)
65	7	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → 𝐽 ∈ Top)
66		ffvelrn 6265	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀:ℕ⟶(Clsd‘𝐽) ∧ 𝑘 ∈ ℕ) → (𝑀‘𝑘) ∈ (Clsd‘𝐽))
67	8, 48, 66	syl2an 493	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (𝑀‘𝑘) ∈ (Clsd‘𝐽))
68	11	cldss 20643	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀‘𝑘) ∈ (Clsd‘𝐽) → (𝑀‘𝑘) ⊆ ∪ 𝐽)
69	67, 68	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (𝑀‘𝑘) ⊆ ∪ 𝐽)
70	61	rpxrd 11749	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (2nd ‘𝑧) ∈ ℝ*)
71	5	blopn 22115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (1st ‘𝑧) ∈ 𝑋 ∧ (2nd ‘𝑧) ∈ ℝ*) → ((1st ‘𝑧)(ball‘𝐷)(2nd ‘𝑧)) ∈ 𝐽)
72	57, 59, 70, 71	syl3anc 1318	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((1st ‘𝑧)(ball‘𝐷)(2nd ‘𝑧)) ∈ 𝐽)
73	56, 72	eqeltrd 2688	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((ball‘𝐷)‘𝑧) ∈ 𝐽)
74	11	ssntr 20672	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 ∈ Top ∧ (𝑀‘𝑘) ⊆ ∪ 𝐽) ∧ (((ball‘𝐷)‘𝑧) ∈ 𝐽 ∧ ((ball‘𝐷)‘𝑧) ⊆ (𝑀‘𝑘))) → ((ball‘𝐷)‘𝑧) ⊆ ((int‘𝐽)‘(𝑀‘𝑘)))
75	74	expr 641	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ (𝑀‘𝑘) ⊆ ∪ 𝐽) ∧ ((ball‘𝐷)‘𝑧) ∈ 𝐽) → (((ball‘𝐷)‘𝑧) ⊆ (𝑀‘𝑘) → ((ball‘𝐷)‘𝑧) ⊆ ((int‘𝐽)‘(𝑀‘𝑘))))
76	65, 69, 73, 75	syl21anc 1317	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (((ball‘𝐷)‘𝑧) ⊆ (𝑀‘𝑘) → ((ball‘𝐷)‘𝑧) ⊆ ((int‘𝐽)‘(𝑀‘𝑘))))
77		ssn0 3928	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((ball‘𝐷)‘𝑧) ⊆ ((int‘𝐽)‘(𝑀‘𝑘)) ∧ ((ball‘𝐷)‘𝑧) ≠ ∅) → ((int‘𝐽)‘(𝑀‘𝑘)) ≠ ∅)
78	77	expcom 450	. . . . . . . . . . . . . . . . . 18 ⊢ (((ball‘𝐷)‘𝑧) ≠ ∅ → (((ball‘𝐷)‘𝑧) ⊆ ((int‘𝐽)‘(𝑀‘𝑘)) → ((int‘𝐽)‘(𝑀‘𝑘)) ≠ ∅))
79	64, 76, 78	sylsyld 59	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (((ball‘𝐷)‘𝑧) ⊆ (𝑀‘𝑘) → ((int‘𝐽)‘(𝑀‘𝑘)) ≠ ∅))
80	51, 79	syl5bir 232	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) = ∅ → ((int‘𝐽)‘(𝑀‘𝑘)) ≠ ∅))
81	80	necon2d 2805	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (((int‘𝐽)‘(𝑀‘𝑘)) = ∅ → (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) ≠ ∅))
82	50, 81	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) ≠ ∅)
83		n0 3890	. . . . . . . . . . . . . . 15 ⊢ ((((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))
84	4	3ad2ant1 1075	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → 𝐷 ∈ (∞Met‘𝑋))
85	11	difopn 20648	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((ball‘𝐷)‘𝑧) ∈ 𝐽 ∧ (𝑀‘𝑘) ∈ (Clsd‘𝐽)) → (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) ∈ 𝐽)
86	73, 67, 85	syl2anc 691	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) ∈ 𝐽)
87	86	3adant3 1074	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) ∈ 𝐽)
88		simp3 1056	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))
89		simp2l 1080	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → 𝑘 ∈ ℕ)
90		nnrp 11718	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
91	90	rpreccld 11758	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
92	89, 91	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → (1 / 𝑘) ∈ ℝ+)
93	5	mopni3 22109	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) ∈ 𝐽 ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) ∧ (1 / 𝑘) ∈ ℝ+) → ∃𝑛 ∈ ℝ+ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))
94	84, 87, 88, 92, 93	syl31anc 1321	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → ∃𝑛 ∈ ℝ+ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))
95		simp1 1054	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → 𝜑)
96		elssuni 4403	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ball‘𝐷)‘𝑧) ∈ 𝐽 → ((ball‘𝐷)‘𝑧) ⊆ ∪ 𝐽)
97	73, 96	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((ball‘𝐷)‘𝑧) ⊆ ∪ 𝐽)
98	23	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → 𝑋 = ∪ 𝐽)
99	97, 98	sseqtr4d 3605	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((ball‘𝐷)‘𝑧) ⊆ 𝑋)
100	99	ssdifssd 3710	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) ⊆ 𝑋)
101	100	sseld 3567	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) → 𝑥 ∈ 𝑋))
102	101	3impia 1253	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → 𝑥 ∈ 𝑋)
103		simp2 1055	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)))
104		rphalfcl 11734	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ℝ+ → (𝑛 / 2) ∈ ℝ+)
105		rphalflt 11736	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ℝ+ → (𝑛 / 2) < 𝑛)
106		breq1 4586	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑟 = (𝑛 / 2) → (𝑟 < 𝑛 ↔ (𝑛 / 2) < 𝑛))
107	106	rspcev 3282	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 / 2) ∈ ℝ+ ∧ (𝑛 / 2) < 𝑛) → ∃𝑟 ∈ ℝ+ 𝑟 < 𝑛)
108	104, 105, 107	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ℝ+ → ∃𝑟 ∈ ℝ+ 𝑟 < 𝑛)
109	108	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+) ∧ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))) → ∃𝑟 ∈ ℝ+ 𝑟 < 𝑛)
110		df-rex 2902	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃𝑟 ∈ ℝ+ 𝑟 < 𝑛 ↔ ∃𝑟(𝑟 ∈ ℝ+ ∧ 𝑟 < 𝑛))
111		simpr3 1062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈ ℝ+)
112	111	rpred 11748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈ ℝ)
113		simpr1 1060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → 𝑛 ∈ ℝ+)
114	113	rpred 11748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → 𝑛 ∈ ℝ)
115		simplrl 796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → 𝑘 ∈ ℕ)
116	115	nnrecred 10943	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → (1 / 𝑘) ∈ ℝ)
117		simpr2 1061	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → 𝑟 < 𝑛)
118		lttr 9993	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑟 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (1 / 𝑘) ∈ ℝ) → ((𝑟 < 𝑛 ∧ 𝑛 < (1 / 𝑘)) → 𝑟 < (1 / 𝑘)))
119	118	expdimp 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑟 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (1 / 𝑘) ∈ ℝ) ∧ 𝑟 < 𝑛) → (𝑛 < (1 / 𝑘) → 𝑟 < (1 / 𝑘)))
120	112, 114, 116, 117, 119	syl31anc 1321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → (𝑛 < (1 / 𝑘) → 𝑟 < (1 / 𝑘)))
121	4	anim1i 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋))
122	121	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋))
123		rpxr 11716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ*)
124		rpxr 11716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑛 ∈ ℝ+ → 𝑛 ∈ ℝ*)
125		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑟 < 𝑛 → 𝑟 < 𝑛)
126	123, 124, 125	3anim123i 1240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑟 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛) → (𝑟 ∈ ℝ* ∧ 𝑛 ∈ ℝ* ∧ 𝑟 < 𝑛))
127	126	3coml 1264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+) → (𝑟 ∈ ℝ* ∧ 𝑛 ∈ ℝ* ∧ 𝑟 < 𝑛))
128	5	blsscls 22122	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 ∈ ℝ* ∧ 𝑛 ∈ ℝ* ∧ 𝑟 < 𝑛)) → ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (𝑥(ball‘𝐷)𝑛))
129	122, 127, 128	syl2an 493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (𝑥(ball‘𝐷)𝑛))
130		sstr2 3575	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (𝑥(ball‘𝐷)𝑛) → ((𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) → ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))
131	129, 130	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → ((𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) → ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))
132	120, 131	anim12d 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → ((𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))))
133		simpllr 795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → 𝑥 ∈ 𝑋)
134	133, 111	jca 553	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+))
135	132, 134	jctild 564	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → ((𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))))
136	135	3exp2 1277	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (𝑛 ∈ ℝ+ → (𝑟 < 𝑛 → (𝑟 ∈ ℝ+ → ((𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))))))))
137	136	com35 96	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (𝑛 ∈ ℝ+ → ((𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → (𝑟 ∈ ℝ+ → (𝑟 < 𝑛 → ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))))))))
138	137	imp5d 623	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+) ∧ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))) → ((𝑟 ∈ ℝ+ ∧ 𝑟 < 𝑛) → ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))))
139	138	eximdv 1833	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+) ∧ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))) → (∃𝑟(𝑟 ∈ ℝ+ ∧ 𝑟 < 𝑛) → ∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))))
140	110, 139	syl5bi 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+) ∧ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))) → (∃𝑟 ∈ ℝ+ 𝑟 < 𝑛 → ∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))))
141	109, 140	mpd 15	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+) ∧ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))) → ∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))))
142	141	ex 449	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+) → ((𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → ∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))))
143	142	rexlimdva 3013	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (∃𝑛 ∈ ℝ+ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → ∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))))
144	95, 102, 103, 143	syl21anc 1317	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → (∃𝑛 ∈ ℝ+ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → ∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))))
145	94, 144	mpd 15	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → ∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))))
146	145	3expia 1259	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) → ∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))))
147	146	eximdv 1833	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (∃𝑥 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) → ∃𝑥∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))))
148	83, 147	syl5bi 231	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) ≠ ∅ → ∃𝑥∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))))
149	82, 148	mpd 15	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ∃𝑥∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))))
150		opabn0 4931	. . . . . . . . . . . . 13 ⊢ ({⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ≠ ∅ ↔ ∃𝑥∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))))
151	149, 150	sylibr 223	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ≠ ∅)
152		eldifsn 4260	. . . . . . . . . . . 12 ⊢ ({⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ∈ (𝒫 (𝑋 × ℝ+) ∖ {∅}) ↔ ({⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ∈ 𝒫 (𝑋 × ℝ+) ∧ {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ≠ ∅))
153	46, 151, 152	sylanbrc 695	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ∈ (𝒫 (𝑋 × ℝ+) ∖ {∅}))
154	153	ralrimivva 2954	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑘 ∈ ℕ ∀𝑧 ∈ (𝑋 × ℝ+){⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ∈ (𝒫 (𝑋 × ℝ+) ∖ {∅}))
155		bcthlem.5	. . . . . . . . . . 11 ⊢ 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦ {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))})
156	155	fmpt2 7126	. . . . . . . . . 10 ⊢ (∀𝑘 ∈ ℕ ∀𝑧 ∈ (𝑋 × ℝ+){⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ∈ (𝒫 (𝑋 × ℝ+) ∖ {∅}) ↔ 𝐹:(ℕ × (𝑋 × ℝ+))⟶(𝒫 (𝑋 × ℝ+) ∖ {∅}))
157	154, 156	sylib 207	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:(ℕ × (𝑋 × ℝ+))⟶(𝒫 (𝑋 × ℝ+) ∖ {∅}))
158	157	3ad2ant1 1075	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → 𝐹:(ℕ × (𝑋 × ℝ+))⟶(𝒫 (𝑋 × ℝ+) ∖ {∅}))
159		1z 11284	. . . . . . . . 9 ⊢ 1 ∈ ℤ
160		nnuz 11599	. . . . . . . . 9 ⊢ ℕ = (ℤ≥‘1)
161	159, 160	axdc4uz 12645	. . . . . . . 8 ⊢ (((𝑋 × ℝ+) ∈ V ∧ ⟨𝑛, 𝑚⟩ ∈ (𝑋 × ℝ+) ∧ 𝐹:(ℕ × (𝑋 × ℝ+))⟶(𝒫 (𝑋 × ℝ+) ∖ {∅})) → ∃𝑔(𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛))))
162	32, 41, 158, 161	syl3anc 1318	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → ∃𝑔(𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛))))
163		simpl1 1057	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))) → 𝜑)
164	163, 1	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))) → 𝐷 ∈ (CMet‘𝑋))
165	163, 8	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))) → 𝑀:ℕ⟶(Clsd‘𝐽))
166		simpl3 1059	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))) → 𝑚 ∈ ℝ+)
167	38	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))) → 𝑛 ∈ 𝑋)
168		simpr1 1060	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))) → 𝑔:ℕ⟶(𝑋 × ℝ+))
169		simpr2 1061	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))) → (𝑔‘1) = ⟨𝑛, 𝑚⟩)
170		simpr3 1062	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))) → ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))
171		oveq1 6556	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝑛 + 1) = (𝑘 + 1))
172	171	fveq2d 6107	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → (𝑔‘(𝑛 + 1)) = (𝑔‘(𝑘 + 1)))
173		id 22	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘)
174		fveq2 6103	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝑔‘𝑛) = (𝑔‘𝑘))
175	173, 174	oveq12d 6567	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → (𝑛𝐹(𝑔‘𝑛)) = (𝑘𝐹(𝑔‘𝑘)))
176	172, 175	eleq12d 2682	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → ((𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)) ↔ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘))))
177	176	cbvralv 3147	. . . . . . . . 9 ⊢ (∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)) ↔ ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘)))
178	170, 177	sylib 207	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))) → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘)))
179	5, 164, 155, 165, 166, 167, 168, 169, 178	bcthlem4 22932	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))) → ((𝑛(ball‘𝐷)𝑚) ∖ ∪ ran 𝑀) ≠ ∅)
180	162, 179	exlimddv 1850	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → ((𝑛(ball‘𝐷)𝑚) ∖ ∪ ran 𝑀) ≠ ∅)
181	11	ntrss2 20671	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ ∪ ran 𝑀 ⊆ ∪ 𝐽) → ((int‘𝐽)‘∪ ran 𝑀) ⊆ ∪ ran 𝑀)
182	7, 15, 181	syl2anc 691	. . . . . . . . . 10 ⊢ (𝜑 → ((int‘𝐽)‘∪ ran 𝑀) ⊆ ∪ ran 𝑀)
183		sstr2 3575	. . . . . . . . . 10 ⊢ ((𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘∪ ran 𝑀) → (((int‘𝐽)‘∪ ran 𝑀) ⊆ ∪ ran 𝑀 → (𝑛(ball‘𝐷)𝑚) ⊆ ∪ ran 𝑀))
184	182, 183	syl5com 31	. . . . . . . . 9 ⊢ (𝜑 → ((𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘∪ ran 𝑀) → (𝑛(ball‘𝐷)𝑚) ⊆ ∪ ran 𝑀))
185		ssdif0 3896	. . . . . . . . 9 ⊢ ((𝑛(ball‘𝐷)𝑚) ⊆ ∪ ran 𝑀 ↔ ((𝑛(ball‘𝐷)𝑚) ∖ ∪ ran 𝑀) = ∅)
186	184, 185	syl6ib 240	. . . . . . . 8 ⊢ (𝜑 → ((𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘∪ ran 𝑀) → ((𝑛(ball‘𝐷)𝑚) ∖ ∪ ran 𝑀) = ∅))
187	186	necon3ad 2795	. . . . . . 7 ⊢ (𝜑 → (((𝑛(ball‘𝐷)𝑚) ∖ ∪ ran 𝑀) ≠ ∅ → ¬ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘∪ ran 𝑀)))
188	187	3ad2ant1 1075	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → (((𝑛(ball‘𝐷)𝑚) ∖ ∪ ran 𝑀) ≠ ∅ → ¬ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘∪ ran 𝑀)))
189	180, 188	mpd 15	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → ¬ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘∪ ran 𝑀))
190	189	3expa 1257	. . . 4 ⊢ (((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀)) ∧ 𝑚 ∈ ℝ+) → ¬ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘∪ ran 𝑀))
191	190	nrexdv 2984	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀)) → ¬ ∃𝑚 ∈ ℝ+ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘∪ ran 𝑀))
192	21, 191	pm2.65da 598	. 2 ⊢ (𝜑 → ¬ 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀))
193	192	eq0rdv 3931	1 ⊢ (𝜑 → ((int‘𝐽)‘∪ ran 𝑀) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∖ cdif 3537   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {csn 4125  ⟨cop 4131  ∪ cuni 4372   class class class wbr 4583  {copab 4642   × cxp 5036  ran crn 5039  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  1^st c1st 7057  2^nd c2nd 7058  ℝcr 9814  1c1 9816   + caddc 9818  ℝ^*cxr 9952   < clt 9953   / cdiv 10563  ℕcn 10897  2c2 10947  ℝ⁺crp 11708  ∞Metcxmt 19552  Metcme 19553  ballcbl 19554  MetOpencmopn 19557  Topctop 20517  Clsdccld 20630  intcnt 20631  clsccl 20632  CMetcms 22860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-dc 9151  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ico 12052  df-rest 15906  df-topgen 15927  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-fbas 19564  df-fg 19565  df-top 20521  df-bases 20522  df-topon 20523  df-cld 20633  df-ntr 20634  df-cls 20635  df-nei 20712  df-lm 20843  df-fil 21460  df-fm 21552  df-flim 21553  df-flf 21554  df-cfil 22861  df-cau 22862  df-cmet 22863

This theorem is referenced by:  bcth  22934