Metamath Proof Explorer

Theorem bcthlem3

Description: Lemma for bcth . The limit point of the centers in the sequence is in the intersection of every ball in the sequence. (Contributed by Mario Carneiro, 7-Jan-2014)

Ref Expression
Hypotheses bcth.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
bcthlem.4 ⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
bcthlem.5 ⊢ 𝐹 = ( 𝑘 ∈ ℕ , 𝑧 ∈ ( 𝑋 × ℝ+ ) ↦ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } )
bcthlem.6 ⊢ ( 𝜑 → 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) )
bcthlem.7 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
bcthlem.8 ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
bcthlem.9 ⊢ ( 𝜑 → 𝑔 : ℕ ⟶ ( 𝑋 × ℝ+ ) )
bcthlem.10 ⊢ ( 𝜑 → ( 𝑔 ‘ 1 ) = ⟨ 𝐶 , 𝑅 ⟩ )
bcthlem.11 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) )
Assertion bcthlem3 ( ( 𝜑 ∧ ( 1st ∘ 𝑔 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ∧ 𝐴 ∈ ℕ ) → 𝑥 ∈ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 bcth.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 bcthlem.4 ⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
3 bcthlem.5 ⊢ 𝐹 = ( 𝑘 ∈ ℕ , 𝑧 ∈ ( 𝑋 × ℝ+ ) ↦ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } )
4 bcthlem.6 ⊢ ( 𝜑 → 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) )
5 bcthlem.7 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
6 bcthlem.8 ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
7 bcthlem.9 ⊢ ( 𝜑 → 𝑔 : ℕ ⟶ ( 𝑋 × ℝ+ ) )
8 bcthlem.10 ⊢ ( 𝜑 → ( 𝑔 ‘ 1 ) = ⟨ 𝐶 , 𝑅 ⟩ )
9 bcthlem.11 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) )
10 fvoveq1 ⊢ ( 𝑘 = 𝐴 → ( 𝑔 ‘ ( 𝑘 + 1 ) ) = ( 𝑔 ‘ ( 𝐴 + 1 ) ) )
11 id ⊢ ( 𝑘 = 𝐴 → 𝑘 = 𝐴 )
12 fveq2 ⊢ ( 𝑘 = 𝐴 → ( 𝑔 ‘ 𝑘 ) = ( 𝑔 ‘ 𝐴 ) )
13 11 12 oveq12d ⊢ ( 𝑘 = 𝐴 → ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) = ( 𝐴 𝐹 ( 𝑔 ‘ 𝐴 ) ) )
14 10 13 eleq12d ⊢ ( 𝑘 = 𝐴 → ( ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ↔ ( 𝑔 ‘ ( 𝐴 + 1 ) ) ∈ ( 𝐴 𝐹 ( 𝑔 ‘ 𝐴 ) ) ) )
15 14 rspccva ⊢ ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ∧ 𝐴 ∈ ℕ ) → ( 𝑔 ‘ ( 𝐴 + 1 ) ) ∈ ( 𝐴 𝐹 ( 𝑔 ‘ 𝐴 ) ) )
16 9 15 sylan ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ( 𝑔 ‘ ( 𝐴 + 1 ) ) ∈ ( 𝐴 𝐹 ( 𝑔 ‘ 𝐴 ) ) )
17 7 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ( 𝑔 ‘ 𝐴 ) ∈ ( 𝑋 × ℝ+ ) )
18 1 2 3 bcthlem1 ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ℕ ∧ ( 𝑔 ‘ 𝐴 ) ∈ ( 𝑋 × ℝ+ ) ) ) → ( ( 𝑔 ‘ ( 𝐴 + 1 ) ) ∈ ( 𝐴 𝐹 ( 𝑔 ‘ 𝐴 ) ) ↔ ( ( 𝑔 ‘ ( 𝐴 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) ∧ ( 2nd ‘ ( 𝑔 ‘ ( 𝐴 + 1 ) ) ) < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝐴 + 1 ) ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝐴 ) ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) )
19 18 expr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ( ( 𝑔 ‘ 𝐴 ) ∈ ( 𝑋 × ℝ+ ) → ( ( 𝑔 ‘ ( 𝐴 + 1 ) ) ∈ ( 𝐴 𝐹 ( 𝑔 ‘ 𝐴 ) ) ↔ ( ( 𝑔 ‘ ( 𝐴 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) ∧ ( 2nd ‘ ( 𝑔 ‘ ( 𝐴 + 1 ) ) ) < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝐴 + 1 ) ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝐴 ) ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) ) )
20 17 19 mpd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ( ( 𝑔 ‘ ( 𝐴 + 1 ) ) ∈ ( 𝐴 𝐹 ( 𝑔 ‘ 𝐴 ) ) ↔ ( ( 𝑔 ‘ ( 𝐴 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) ∧ ( 2nd ‘ ( 𝑔 ‘ ( 𝐴 + 1 ) ) ) < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝐴 + 1 ) ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝐴 ) ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) )
21 16 20 mpbid ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ( ( 𝑔 ‘ ( 𝐴 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) ∧ ( 2nd ‘ ( 𝑔 ‘ ( 𝐴 + 1 ) ) ) < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝐴 + 1 ) ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝐴 ) ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) )
22 21 simp3d ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝐴 + 1 ) ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝐴 ) ) ∖ ( 𝑀 ‘ 𝐴 ) ) )
23 22 difss2d ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝐴 + 1 ) ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝐴 ) ) )
24 23 3adant2 ⊢ ( ( 𝜑 ∧ ( 1st ∘ 𝑔 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ∧ 𝐴 ∈ ℕ ) → ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝐴 + 1 ) ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝐴 ) ) )
25 peano2nn ⊢ ( 𝐴 ∈ ℕ → ( 𝐴 + 1 ) ∈ ℕ )
26 cmetmet ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
27 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
28 2 26 27 3syl ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
29 1 2 3 4 5 6 7 8 9 bcthlem2 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑛 ) ) )
30 28 7 29 1 caublcls ⊢ ( ( 𝜑 ∧ ( 1st ∘ 𝑔 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ∧ ( 𝐴 + 1 ) ∈ ℕ ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝐴 + 1 ) ) ) ) )
31 25 30 syl3an3 ⊢ ( ( 𝜑 ∧ ( 1st ∘ 𝑔 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ∧ 𝐴 ∈ ℕ ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝐴 + 1 ) ) ) ) )
32 24 31 sseldd ⊢ ( ( 𝜑 ∧ ( 1st ∘ 𝑔 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ∧ 𝐴 ∈ ℕ ) → 𝑥 ∈ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝐴 ) ) )