Metamath Proof Explorer

Theorem heiborlem6

Description: Lemma for heibor . Since the sequence of balls connected by the function T ensures that each ball nontrivially intersects with the next (since the empty set has a finite subcover, the intersection of any two successive balls in the sequence is nonempty), and each ball is half the size of the previous one, the distance between the centers is at most 3 / 2 times the size of the larger, and so if we expand each ball by a factor of 3 we get a nested sequence of balls. (Contributed by Jeff Madsen, 23-Jan-2014)

Ref Expression
Hypotheses heibor.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
heibor.3 ⊢ 𝐾 = { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 }
heibor.4 ⊢ 𝐺 = { ⟨ 𝑦 , 𝑛 ⟩ ∣ ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝑦 𝐵 𝑛 ) ∈ 𝐾 ) }
heibor.5 ⊢ 𝐵 = ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
heibor.6 ⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
heibor.7 ⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) )
heibor.8 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) )
heibor.9 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐺 ( ( 𝑇 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
heibor.10 ⊢ ( 𝜑 → 𝐶 𝐺 0 )
heibor.11 ⊢ 𝑆 = seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) )
heibor.12 ⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ⟨ ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) ⟩ )
Assertion heiborlem6 ( 𝜑 → ∀ 𝑘 ∈ ℕ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ ( 𝑘 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 heibor.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 heibor.3 ⊢ 𝐾 = { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 }
3 heibor.4 ⊢ 𝐺 = { ⟨ 𝑦 , 𝑛 ⟩ ∣ ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝑦 𝐵 𝑛 ) ∈ 𝐾 ) }
4 heibor.5 ⊢ 𝐵 = ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
5 heibor.6 ⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
6 heibor.7 ⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) )
7 heibor.8 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) )
8 heibor.9 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐺 ( ( 𝑇 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
9 heibor.10 ⊢ ( 𝜑 → 𝐶 𝐺 0 )
10 heibor.11 ⊢ 𝑆 = seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) )
11 heibor.12 ⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ⟨ ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) ⟩ )
12 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
13 cmetmet ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
14 5 13 syl ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
15 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
16 14 15 syl ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
18 inss1 ⊢ ( 𝒫 𝑋 ∩ Fin ) ⊆ 𝒫 𝑋
19 fss ⊢ ( ( 𝐹 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) ∧ ( 𝒫 𝑋 ∩ Fin ) ⊆ 𝒫 𝑋 ) → 𝐹 : ℕ0 ⟶ 𝒫 𝑋 )
20 6 18 19 sylancl ⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ 𝒫 𝑋 )
21 peano2nn0 ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ0 )
22 ffvelcdm ⊢ ( ( 𝐹 : ℕ0 ⟶ 𝒫 𝑋 ∧ ( 𝑘 + 1 ) ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ 𝒫 𝑋 )
23 20 21 22 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ 𝒫 𝑋 )
24 23 elpwid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ⊆ 𝑋 )
25 1 2 3 4 5 6 7 8 9 10 heiborlem4 ⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ℕ0 ) → ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐺 ( 𝑘 + 1 ) )
26 21 25 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐺 ( 𝑘 + 1 ) )
27 fvex ⊢ ( 𝑆 ‘ ( 𝑘 + 1 ) ) ∈ V
28 ovex ⊢ ( 𝑘 + 1 ) ∈ V
29 1 2 3 27 28 heiborlem2 ⊢ ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐺 ( 𝑘 + 1 ) ↔ ( ( 𝑘 + 1 ) ∈ ℕ0 ∧ ( 𝑆 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∧ ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐵 ( 𝑘 + 1 ) ) ∈ 𝐾 ) )
30 29 simp2bi ⊢ ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐺 ( 𝑘 + 1 ) → ( 𝑆 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
31 26 30 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑆 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
32 24 31 sseldd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑆 ‘ ( 𝑘 + 1 ) ) ∈ 𝑋 )
33 20 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝒫 𝑋 )
34 33 elpwid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ⊆ 𝑋 )
35 1 2 3 4 5 6 7 8 9 10 heiborlem4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 )
36 fvex ⊢ ( 𝑆 ‘ 𝑘 ) ∈ V
37 vex ⊢ 𝑘 ∈ V
38 1 2 3 36 37 heiborlem2 ⊢ ( ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 ↔ ( 𝑘 ∈ ℕ0 ∧ ( 𝑆 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) ∧ ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∈ 𝐾 ) )
39 38 simp2bi ⊢ ( ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 → ( 𝑆 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) )
40 35 39 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑆 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) )
41 34 40 sseldd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑆 ‘ 𝑘 ) ∈ 𝑋 )
42 3re ⊢ 3 ∈ ℝ
43 2nn ⊢ 2 ∈ ℕ
44 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ ( 𝑘 + 1 ) ∈ ℕ0 ) → ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℕ )
45 43 21 44 sylancr ⊢ ( 𝑘 ∈ ℕ0 → ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℕ )
46 45 nnrpd ⊢ ( 𝑘 ∈ ℕ0 → ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℝ+ )
47 46 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℝ+ )
48 rerpdivcl ⊢ ( ( 3 ∈ ℝ ∧ ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℝ+ ) → ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ )
49 42 47 48 sylancr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ )
50 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 2 ↑ 𝑘 ) ∈ ℕ )
51 43 50 mpan ⊢ ( 𝑘 ∈ ℕ0 → ( 2 ↑ 𝑘 ) ∈ ℕ )
52 51 nnrpd ⊢ ( 𝑘 ∈ ℕ0 → ( 2 ↑ 𝑘 ) ∈ ℝ+ )
53 52 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 2 ↑ 𝑘 ) ∈ ℝ+ )
54 rerpdivcl ⊢ ( ( 3 ∈ ℝ ∧ ( 2 ↑ 𝑘 ) ∈ ℝ+ ) → ( 3 / ( 2 ↑ 𝑘 ) ) ∈ ℝ )
55 42 53 54 sylancr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 3 / ( 2 ↑ 𝑘 ) ) ∈ ℝ )
56 oveq1 ⊢ ( 𝑧 = ( 𝑆 ‘ 𝑘 ) → ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) = ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
57 oveq2 ⊢ ( 𝑚 = 𝑘 → ( 2 ↑ 𝑚 ) = ( 2 ↑ 𝑘 ) )
58 57 oveq2d ⊢ ( 𝑚 = 𝑘 → ( 1 / ( 2 ↑ 𝑚 ) ) = ( 1 / ( 2 ↑ 𝑘 ) ) )
59 58 oveq2d ⊢ ( 𝑚 = 𝑘 → ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) = ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) )
60 ovex ⊢ ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ∈ V
61 56 59 4 60 ovmpo ⊢ ( ( ( 𝑆 ‘ 𝑘 ) ∈ 𝑋 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) = ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) )
62 41 61 sylancom ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) = ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) )
63 df-br ⊢ ( ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 ↔ ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ ∈ 𝐺 )
64 fveq2 ⊢ ( 𝑥 = ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ ) )
65 df-ov ⊢ ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) = ( 𝑇 ‘ ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ )
66 64 65 eqtr4di ⊢ ( 𝑥 = ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ → ( 𝑇 ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) )
67 36 37 op2ndd ⊢ ( 𝑥 = ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ → ( 2nd ‘ 𝑥 ) = 𝑘 )
68 67 oveq1d ⊢ ( 𝑥 = ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ → ( ( 2nd ‘ 𝑥 ) + 1 ) = ( 𝑘 + 1 ) )
69 66 68 breq12d ⊢ ( 𝑥 = ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ → ( ( 𝑇 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ↔ ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ) )
70 fveq2 ⊢ ( 𝑥 = ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ → ( 𝐵 ‘ 𝑥 ) = ( 𝐵 ‘ ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ ) )
71 df-ov ⊢ ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) = ( 𝐵 ‘ ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ )
72 70 71 eqtr4di ⊢ ( 𝑥 = ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ → ( 𝐵 ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) )
73 66 68 oveq12d ⊢ ( 𝑥 = ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ → ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) = ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) )
74 72 73 ineq12d ⊢ ( 𝑥 = ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ → ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) = ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) )
75 74 eleq1d ⊢ ( 𝑥 = ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ → ( ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ↔ ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ) )
76 69 75 anbi12d ⊢ ( 𝑥 = ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ → ( ( ( 𝑇 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ↔ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ∧ ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ) ) )
77 76 rspccv ⊢ ( ∀ 𝑥 ∈ 𝐺 ( ( 𝑇 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) → ( ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ ∈ 𝐺 → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ∧ ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ) ) )
78 8 77 syl ⊢ ( 𝜑 → ( ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ ∈ 𝐺 → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ∧ ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ) ) )
79 63 78 biimtrid ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ∧ ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ) ) )
80 79 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ∧ ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ) ) )
81 35 80 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ∧ ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ) )
82 81 simpld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) )
83 ovex ⊢ ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ∈ V
84 1 2 3 83 28 heiborlem2 ⊢ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ↔ ( ( 𝑘 + 1 ) ∈ ℕ0 ∧ ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∧ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ∈ 𝐾 ) )
85 84 simp2bi ⊢ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) → ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
86 82 85 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
87 24 86 sseldd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ∈ 𝑋 )
88 21 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 + 1 ) ∈ ℕ0 )
89 oveq1 ⊢ ( 𝑧 = ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) → ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) = ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
90 oveq2 ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( 2 ↑ 𝑚 ) = ( 2 ↑ ( 𝑘 + 1 ) ) )
91 90 oveq2d ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( 1 / ( 2 ↑ 𝑚 ) ) = ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) )
92 91 oveq2d ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) = ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) )
93 ovex ⊢ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ∈ V
94 89 92 4 93 ovmpo ⊢ ( ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ∈ 𝑋 ∧ ( 𝑘 + 1 ) ∈ ℕ0 ) → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) = ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) )
95 87 88 94 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) = ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) )
96 62 95 ineq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) = ( ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) )
97 81 simprd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 )
98 0elpw ⊢ ∅ ∈ 𝒫 𝑈
99 0fi ⊢ ∅ ∈ Fin
100 elin ⊢ ( ∅ ∈ ( 𝒫 𝑈 ∩ Fin ) ↔ ( ∅ ∈ 𝒫 𝑈 ∧ ∅ ∈ Fin ) )
101 98 99 100 mpbir2an ⊢ ∅ ∈ ( 𝒫 𝑈 ∩ Fin )
102 0ss ⊢ ∅ ⊆ ∪ ∅
103 unieq ⊢ ( 𝑣 = ∅ → ∪ 𝑣 = ∪ ∅ )
104 103 sseq2d ⊢ ( 𝑣 = ∅ → ( ∅ ⊆ ∪ 𝑣 ↔ ∅ ⊆ ∪ ∅ ) )
105 104 rspcev ⊢ ( ( ∅ ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∅ ⊆ ∪ ∅ ) → ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ∅ ⊆ ∪ 𝑣 )
106 101 102 105 mp2an ⊢ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ∅ ⊆ ∪ 𝑣
107 0ex ⊢ ∅ ∈ V
108 sseq1 ⊢ ( 𝑢 = ∅ → ( 𝑢 ⊆ ∪ 𝑣 ↔ ∅ ⊆ ∪ 𝑣 ) )
109 108 rexbidv ⊢ ( 𝑢 = ∅ → ( ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 ↔ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ∅ ⊆ ∪ 𝑣 ) )
110 109 notbid ⊢ ( 𝑢 = ∅ → ( ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 ↔ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ∅ ⊆ ∪ 𝑣 ) )
111 107 110 2 elab2 ⊢ ( ∅ ∈ 𝐾 ↔ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ∅ ⊆ ∪ 𝑣 )
112 111 con2bii ⊢ ( ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ∅ ⊆ ∪ 𝑣 ↔ ¬ ∅ ∈ 𝐾 )
113 106 112 mpbi ⊢ ¬ ∅ ∈ 𝐾
114 nelne2 ⊢ ( ( ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ∧ ¬ ∅ ∈ 𝐾 ) → ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ≠ ∅ )
115 97 113 114 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ≠ ∅ )
116 96 115 eqnetrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) ≠ ∅ )
117 52 rpreccld ⊢ ( 𝑘 ∈ ℕ0 → ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ+ )
118 117 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ+ )
119 118 rpred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ )
120 46 rpreccld ⊢ ( 𝑘 ∈ ℕ0 → ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ+ )
121 120 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ+ )
122 121 rpred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ )
123 rexadd ⊢ ( ( ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ ∧ ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ ) → ( ( 1 / ( 2 ↑ 𝑘 ) ) +𝑒 ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) = ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) )
124 119 122 123 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 / ( 2 ↑ 𝑘 ) ) +𝑒 ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) = ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) )
125 124 breq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 1 / ( 2 ↑ 𝑘 ) ) +𝑒 ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ↔ ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ) )
126 118 rpxrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ* )
127 121 rpxrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ* )
128 bldisj ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑆 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ∈ 𝑋 ) ∧ ( ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ* ∧ ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ* ∧ ( ( 1 / ( 2 ↑ 𝑘 ) ) +𝑒 ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ) ) → ( ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) = ∅ )
129 128 3exp2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑆 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ∈ 𝑋 ) → ( ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ* → ( ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ* → ( ( ( 1 / ( 2 ↑ 𝑘 ) ) +𝑒 ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) → ( ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) = ∅ ) ) ) )
130 129 imp32 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑆 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ∈ 𝑋 ) ∧ ( ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ* ∧ ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ* ) ) → ( ( ( 1 / ( 2 ↑ 𝑘 ) ) +𝑒 ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) → ( ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) = ∅ ) )
131 17 41 87 126 127 130 syl32anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 1 / ( 2 ↑ 𝑘 ) ) +𝑒 ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) → ( ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) = ∅ ) )
132 125 131 sylbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) → ( ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) = ∅ ) )
133 132 necon3ad ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) ≠ ∅ → ¬ ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ) )
134 116 133 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ¬ ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) )
135 118 121 rpaddcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ∈ ℝ+ )
136 135 rpred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ∈ ℝ )
137 14 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
138 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑆 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ∈ 𝑋 ) → ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ∈ ℝ )
139 137 41 87 138 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ∈ ℝ )
140 136 139 letrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ∨ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ≤ ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) )
141 140 ord ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ¬ ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) → ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ≤ ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) )
142 134 141 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ≤ ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) )
143 seqp1 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 0 ) → ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ 𝑘 ) 𝑇 ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) ) )
144 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
145 143 144 eleq2s ⊢ ( 𝑘 ∈ ℕ0 → ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ 𝑘 ) 𝑇 ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) ) )
146 10 fveq1i ⊢ ( 𝑆 ‘ ( 𝑘 + 1 ) ) = ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) )
147 10 fveq1i ⊢ ( 𝑆 ‘ 𝑘 ) = ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ 𝑘 )
148 147 oveq1i ⊢ ( ( 𝑆 ‘ 𝑘 ) 𝑇 ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) ) = ( ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ 𝑘 ) 𝑇 ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) )
149 145 146 148 3eqtr4g ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑆 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑆 ‘ 𝑘 ) 𝑇 ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) ) )
150 eqid ⊢ ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) = ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) )
151 eqeq1 ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( 𝑚 = 0 ↔ ( 𝑘 + 1 ) = 0 ) )
152 oveq1 ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( 𝑚 − 1 ) = ( ( 𝑘 + 1 ) − 1 ) )
153 151 152 ifbieq2d ⊢ ( 𝑚 = ( 𝑘 + 1 ) → if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) = if ( ( 𝑘 + 1 ) = 0 , 𝐶 , ( ( 𝑘 + 1 ) − 1 ) ) )
154 nn0p1nn ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ )
155 nnne0 ⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ( 𝑘 + 1 ) ≠ 0 )
156 155 neneqd ⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ¬ ( 𝑘 + 1 ) = 0 )
157 154 156 syl ⊢ ( 𝑘 ∈ ℕ0 → ¬ ( 𝑘 + 1 ) = 0 )
158 157 iffalsed ⊢ ( 𝑘 ∈ ℕ0 → if ( ( 𝑘 + 1 ) = 0 , 𝐶 , ( ( 𝑘 + 1 ) − 1 ) ) = ( ( 𝑘 + 1 ) − 1 ) )
159 ovex ⊢ ( ( 𝑘 + 1 ) − 1 ) ∈ V
160 158 159 eqeltrdi ⊢ ( 𝑘 ∈ ℕ0 → if ( ( 𝑘 + 1 ) = 0 , 𝐶 , ( ( 𝑘 + 1 ) − 1 ) ) ∈ V )
161 150 153 21 160 fvmptd3 ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) = if ( ( 𝑘 + 1 ) = 0 , 𝐶 , ( ( 𝑘 + 1 ) − 1 ) ) )
162 nn0cn ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ )
163 ax-1cn ⊢ 1 ∈ ℂ
164 pncan ⊢ ( ( 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 )
165 162 163 164 sylancl ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 )
166 161 158 165 3eqtrd ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) = 𝑘 )
167 166 oveq2d ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑆 ‘ 𝑘 ) 𝑇 ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) ) = ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) )
168 149 167 eqtrd ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑆 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) )
169 168 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑆 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) )
170 169 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐷 ( 𝑆 ‘ 𝑘 ) ) = ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐷 ( 𝑆 ‘ 𝑘 ) ) )
171 metsym ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ∈ 𝑋 ∧ ( 𝑆 ‘ 𝑘 ) ∈ 𝑋 ) → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐷 ( 𝑆 ‘ 𝑘 ) ) = ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) )
172 137 87 41 171 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐷 ( 𝑆 ‘ 𝑘 ) ) = ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) )
173 170 172 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐷 ( 𝑆 ‘ 𝑘 ) ) = ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) )
174 3cn ⊢ 3 ∈ ℂ
175 174 2timesi ⊢ ( 2 · 3 ) = ( 3 + 3 )
176 175 oveq1i ⊢ ( ( 2 · 3 ) − 3 ) = ( ( 3 + 3 ) − 3 )
177 174 174 pncan3oi ⊢ ( ( 3 + 3 ) − 3 ) = 3
178 df-3 ⊢ 3 = ( 2 + 1 )
179 176 177 178 3eqtri ⊢ ( ( 2 · 3 ) − 3 ) = ( 2 + 1 )
180 179 oveq1i ⊢ ( ( ( 2 · 3 ) − 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( ( 2 + 1 ) / ( 2 ↑ ( 𝑘 + 1 ) ) )
181 rpcn ⊢ ( ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℝ+ → ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℂ )
182 rpne0 ⊢ ( ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℝ+ → ( 2 ↑ ( 𝑘 + 1 ) ) ≠ 0 )
183 2cn ⊢ 2 ∈ ℂ
184 183 174 mulcli ⊢ ( 2 · 3 ) ∈ ℂ
185 divsubdir ⊢ ( ( ( 2 · 3 ) ∈ ℂ ∧ 3 ∈ ℂ ∧ ( ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℂ ∧ ( 2 ↑ ( 𝑘 + 1 ) ) ≠ 0 ) ) → ( ( ( 2 · 3 ) − 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( ( ( 2 · 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) − ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) )
186 184 174 185 mp3an12 ⊢ ( ( ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℂ ∧ ( 2 ↑ ( 𝑘 + 1 ) ) ≠ 0 ) → ( ( ( 2 · 3 ) − 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( ( ( 2 · 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) − ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) )
187 181 182 186 syl2anc ⊢ ( ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℝ+ → ( ( ( 2 · 3 ) − 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( ( ( 2 · 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) − ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) )
188 46 187 syl ⊢ ( 𝑘 ∈ ℕ0 → ( ( ( 2 · 3 ) − 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( ( ( 2 · 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) − ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) )
189 divdir ⊢ ( ( 2 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℂ ∧ ( 2 ↑ ( 𝑘 + 1 ) ) ≠ 0 ) ) → ( ( 2 + 1 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( ( 2 / ( 2 ↑ ( 𝑘 + 1 ) ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) )
190 183 163 189 mp3an12 ⊢ ( ( ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℂ ∧ ( 2 ↑ ( 𝑘 + 1 ) ) ≠ 0 ) → ( ( 2 + 1 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( ( 2 / ( 2 ↑ ( 𝑘 + 1 ) ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) )
191 181 182 190 syl2anc ⊢ ( ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℝ+ → ( ( 2 + 1 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( ( 2 / ( 2 ↑ ( 𝑘 + 1 ) ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) )
192 46 191 syl ⊢ ( 𝑘 ∈ ℕ0 → ( ( 2 + 1 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( ( 2 / ( 2 ↑ ( 𝑘 + 1 ) ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) )
193 180 188 192 3eqtr3a ⊢ ( 𝑘 ∈ ℕ0 → ( ( ( 2 · 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) − ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) = ( ( 2 / ( 2 ↑ ( 𝑘 + 1 ) ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) )
194 rpcn ⊢ ( ( 2 ↑ 𝑘 ) ∈ ℝ+ → ( 2 ↑ 𝑘 ) ∈ ℂ )
195 rpne0 ⊢ ( ( 2 ↑ 𝑘 ) ∈ ℝ+ → ( 2 ↑ 𝑘 ) ≠ 0 )
196 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
197 divcan5 ⊢ ( ( 3 ∈ ℂ ∧ ( ( 2 ↑ 𝑘 ) ∈ ℂ ∧ ( 2 ↑ 𝑘 ) ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 2 · 3 ) / ( 2 · ( 2 ↑ 𝑘 ) ) ) = ( 3 / ( 2 ↑ 𝑘 ) ) )
198 174 196 197 mp3an13 ⊢ ( ( ( 2 ↑ 𝑘 ) ∈ ℂ ∧ ( 2 ↑ 𝑘 ) ≠ 0 ) → ( ( 2 · 3 ) / ( 2 · ( 2 ↑ 𝑘 ) ) ) = ( 3 / ( 2 ↑ 𝑘 ) ) )
199 194 195 198 syl2anc ⊢ ( ( 2 ↑ 𝑘 ) ∈ ℝ+ → ( ( 2 · 3 ) / ( 2 · ( 2 ↑ 𝑘 ) ) ) = ( 3 / ( 2 ↑ 𝑘 ) ) )
200 52 199 syl ⊢ ( 𝑘 ∈ ℕ0 → ( ( 2 · 3 ) / ( 2 · ( 2 ↑ 𝑘 ) ) ) = ( 3 / ( 2 ↑ 𝑘 ) ) )
201 52 194 syl ⊢ ( 𝑘 ∈ ℕ0 → ( 2 ↑ 𝑘 ) ∈ ℂ )
202 mulcom ⊢ ( ( 2 ∈ ℂ ∧ ( 2 ↑ 𝑘 ) ∈ ℂ ) → ( 2 · ( 2 ↑ 𝑘 ) ) = ( ( 2 ↑ 𝑘 ) · 2 ) )
203 183 201 202 sylancr ⊢ ( 𝑘 ∈ ℕ0 → ( 2 · ( 2 ↑ 𝑘 ) ) = ( ( 2 ↑ 𝑘 ) · 2 ) )
204 expp1 ⊢ ( ( 2 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 2 ↑ ( 𝑘 + 1 ) ) = ( ( 2 ↑ 𝑘 ) · 2 ) )
205 183 204 mpan ⊢ ( 𝑘 ∈ ℕ0 → ( 2 ↑ ( 𝑘 + 1 ) ) = ( ( 2 ↑ 𝑘 ) · 2 ) )
206 203 205 eqtr4d ⊢ ( 𝑘 ∈ ℕ0 → ( 2 · ( 2 ↑ 𝑘 ) ) = ( 2 ↑ ( 𝑘 + 1 ) ) )
207 206 oveq2d ⊢ ( 𝑘 ∈ ℕ0 → ( ( 2 · 3 ) / ( 2 · ( 2 ↑ 𝑘 ) ) ) = ( ( 2 · 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) )
208 200 207 eqtr3d ⊢ ( 𝑘 ∈ ℕ0 → ( 3 / ( 2 ↑ 𝑘 ) ) = ( ( 2 · 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) )
209 208 oveq1d ⊢ ( 𝑘 ∈ ℕ0 → ( ( 3 / ( 2 ↑ 𝑘 ) ) − ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) = ( ( ( 2 · 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) − ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) )
210 divcan5 ⊢ ( ( 1 ∈ ℂ ∧ ( ( 2 ↑ 𝑘 ) ∈ ℂ ∧ ( 2 ↑ 𝑘 ) ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 2 · 1 ) / ( 2 · ( 2 ↑ 𝑘 ) ) ) = ( 1 / ( 2 ↑ 𝑘 ) ) )
211 163 196 210 mp3an13 ⊢ ( ( ( 2 ↑ 𝑘 ) ∈ ℂ ∧ ( 2 ↑ 𝑘 ) ≠ 0 ) → ( ( 2 · 1 ) / ( 2 · ( 2 ↑ 𝑘 ) ) ) = ( 1 / ( 2 ↑ 𝑘 ) ) )
212 194 195 211 syl2anc ⊢ ( ( 2 ↑ 𝑘 ) ∈ ℝ+ → ( ( 2 · 1 ) / ( 2 · ( 2 ↑ 𝑘 ) ) ) = ( 1 / ( 2 ↑ 𝑘 ) ) )
213 52 212 syl ⊢ ( 𝑘 ∈ ℕ0 → ( ( 2 · 1 ) / ( 2 · ( 2 ↑ 𝑘 ) ) ) = ( 1 / ( 2 ↑ 𝑘 ) ) )
214 2t1e2 ⊢ ( 2 · 1 ) = 2
215 214 a1i ⊢ ( 𝑘 ∈ ℕ0 → ( 2 · 1 ) = 2 )
216 215 206 oveq12d ⊢ ( 𝑘 ∈ ℕ0 → ( ( 2 · 1 ) / ( 2 · ( 2 ↑ 𝑘 ) ) ) = ( 2 / ( 2 ↑ ( 𝑘 + 1 ) ) ) )
217 213 216 eqtr3d ⊢ ( 𝑘 ∈ ℕ0 → ( 1 / ( 2 ↑ 𝑘 ) ) = ( 2 / ( 2 ↑ ( 𝑘 + 1 ) ) ) )
218 217 oveq1d ⊢ ( 𝑘 ∈ ℕ0 → ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) = ( ( 2 / ( 2 ↑ ( 𝑘 + 1 ) ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) )
219 193 209 218 3eqtr4d ⊢ ( 𝑘 ∈ ℕ0 → ( ( 3 / ( 2 ↑ 𝑘 ) ) − ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) = ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) )
220 219 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 3 / ( 2 ↑ 𝑘 ) ) − ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) = ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) )
221 142 173 220 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐷 ( 𝑆 ‘ 𝑘 ) ) ≤ ( ( 3 / ( 2 ↑ 𝑘 ) ) − ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) )
222 blss2 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑆 ‘ ( 𝑘 + 1 ) ) ∈ 𝑋 ∧ ( 𝑆 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ( ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ ∧ ( 3 / ( 2 ↑ 𝑘 ) ) ∈ ℝ ∧ ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐷 ( 𝑆 ‘ 𝑘 ) ) ≤ ( ( 3 / ( 2 ↑ 𝑘 ) ) − ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) ) → ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) ( ball ‘ 𝐷 ) ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ⊆ ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 3 / ( 2 ↑ 𝑘 ) ) ) )
223 17 32 41 49 55 221 222 syl33anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) ( ball ‘ 𝐷 ) ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ⊆ ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 3 / ( 2 ↑ 𝑘 ) ) ) )
224 12 223 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) ( ball ‘ 𝐷 ) ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ⊆ ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 3 / ( 2 ↑ 𝑘 ) ) ) )
225 peano2nn ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
226 fveq2 ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑆 ‘ 𝑛 ) = ( 𝑆 ‘ ( 𝑘 + 1 ) ) )
227 oveq2 ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 2 ↑ 𝑛 ) = ( 2 ↑ ( 𝑘 + 1 ) ) )
228 227 oveq2d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 3 / ( 2 ↑ 𝑛 ) ) = ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) )
229 226 228 opeq12d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ⟨ ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) ⟩ = ⟨ ( 𝑆 ‘ ( 𝑘 + 1 ) ) , ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ⟩ )
230 opex ⊢ ⟨ ( 𝑆 ‘ ( 𝑘 + 1 ) ) , ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ⟩ ∈ V
231 229 11 230 fvmpt ⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ( 𝑀 ‘ ( 𝑘 + 1 ) ) = ⟨ ( 𝑆 ‘ ( 𝑘 + 1 ) ) , ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ⟩ )
232 225 231 syl ⊢ ( 𝑘 ∈ ℕ → ( 𝑀 ‘ ( 𝑘 + 1 ) ) = ⟨ ( 𝑆 ‘ ( 𝑘 + 1 ) ) , ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ⟩ )
233 232 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑀 ‘ ( 𝑘 + 1 ) ) = ⟨ ( 𝑆 ‘ ( 𝑘 + 1 ) ) , ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ⟩ )
234 233 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ ( 𝑘 + 1 ) ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 𝑆 ‘ ( 𝑘 + 1 ) ) , ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ⟩ ) )
235 df-ov ⊢ ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) ( ball ‘ 𝐷 ) ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 𝑆 ‘ ( 𝑘 + 1 ) ) , ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ⟩ )
236 234 235 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ ( 𝑘 + 1 ) ) ) = ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) ( ball ‘ 𝐷 ) ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) )
237 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑆 ‘ 𝑛 ) = ( 𝑆 ‘ 𝑘 ) )
238 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 2 ↑ 𝑛 ) = ( 2 ↑ 𝑘 ) )
239 238 oveq2d ⊢ ( 𝑛 = 𝑘 → ( 3 / ( 2 ↑ 𝑛 ) ) = ( 3 / ( 2 ↑ 𝑘 ) ) )
240 237 239 opeq12d ⊢ ( 𝑛 = 𝑘 → ⟨ ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) ⟩ = ⟨ ( 𝑆 ‘ 𝑘 ) , ( 3 / ( 2 ↑ 𝑘 ) ) ⟩ )
241 opex ⊢ ⟨ ( 𝑆 ‘ 𝑘 ) , ( 3 / ( 2 ↑ 𝑘 ) ) ⟩ ∈ V
242 240 11 241 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( 𝑀 ‘ 𝑘 ) = ⟨ ( 𝑆 ‘ 𝑘 ) , ( 3 / ( 2 ↑ 𝑘 ) ) ⟩ )
243 242 fveq2d ⊢ ( 𝑘 ∈ ℕ → ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 𝑆 ‘ 𝑘 ) , ( 3 / ( 2 ↑ 𝑘 ) ) ⟩ ) )
244 df-ov ⊢ ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 3 / ( 2 ↑ 𝑘 ) ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 𝑆 ‘ 𝑘 ) , ( 3 / ( 2 ↑ 𝑘 ) ) ⟩ )
245 243 244 eqtr4di ⊢ ( 𝑘 ∈ ℕ → ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 3 / ( 2 ↑ 𝑘 ) ) ) )
246 245 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 3 / ( 2 ↑ 𝑘 ) ) ) )
247 224 236 246 3sstr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ ( 𝑘 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) )
248 247 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ ( 𝑘 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) )