Metamath Proof Explorer

Theorem bcthlem2

Description: Lemma for bcth . The balls in the sequence form an inclusion chain. (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 bcthlem2 ( 𝜑 → ∀ 𝑛 ∈ ℕ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ⊆ ( ( 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 cmetmet ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
23 2 22 syl ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
24 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
25 23 24 syl ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
26 1 mopntop ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
27 25 26 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
28 xp1st ⊢ ( ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) → ( 1st ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∈ 𝑋 )
29 xp2nd ⊢ ( ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) → ( 2nd ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∈ ℝ+ )
30 29 rpxrd ⊢ ( ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) → ( 2nd ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∈ ℝ* )
31 28 30 jca ⊢ ( ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) → ( ( 1st ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∈ 𝑋 ∧ ( 2nd ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∈ ℝ* ) )
32 blssm ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 1st ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∈ 𝑋 ∧ ( 2nd ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∈ ℝ* ) → ( ( 1st ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ( ball ‘ 𝐷 ) ( 2nd ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ) ⊆ 𝑋 )
33 32 3expb ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 1st ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∈ 𝑋 ∧ ( 2nd ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∈ ℝ* ) ) → ( ( 1st ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ( ball ‘ 𝐷 ) ( 2nd ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ) ⊆ 𝑋 )
34 25 31 33 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) ) → ( ( 1st ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ( ball ‘ 𝐷 ) ( 2nd ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ) ⊆ 𝑋 )
35 df-ov ⊢ ( ( 1st ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ( ball ‘ 𝐷 ) ( 2nd ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 1st ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) , ( 2nd ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ⟩ )
36 1st2nd2 ⊢ ( ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) → ( 𝑔 ‘ ( 𝑛 + 1 ) ) = ⟨ ( 1st ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) , ( 2nd ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ⟩ )
37 36 fveq2d ⊢ ( ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 1st ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) , ( 2nd ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ⟩ ) )
38 35 37 eqtr4id ⊢ ( ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) → ( ( 1st ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ( ball ‘ 𝐷 ) ( 2nd ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ) = ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) )
39 38 adantl ⊢ ( ( 𝜑 ∧ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) ) → ( ( 1st ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ( ball ‘ 𝐷 ) ( 2nd ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ) = ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) )
40 1 mopnuni ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
41 25 40 syl ⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
42 41 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) ) → 𝑋 = ∪ 𝐽 )
43 34 39 42 3sstr3d ⊢ ( ( 𝜑 ∧ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ⊆ ∪ 𝐽 )
44 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
45 44 sscls ⊢ ( ( 𝐽 ∈ Top ∧ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ⊆ ∪ 𝐽 ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ) )
46 27 43 45 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ) )
47 difss2 ⊢ ( ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑛 ) ) ∖ ( 𝑀 ‘ 𝑛 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑛 ) ) )
48 sstr2 ⊢ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ) → ( ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑛 ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑛 ) ) ) )
49 46 47 48 syl2im ⊢ ( ( 𝜑 ∧ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) ) → ( ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑛 ) ) ∖ ( 𝑀 ‘ 𝑛 ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑛 ) ) ) )
50 49 a1d ⊢ ( ( 𝜑 ∧ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) ) → ( ( 2nd ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) < ( 1 / 𝑛 ) → ( ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑛 ) ) ∖ ( 𝑀 ‘ 𝑛 ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) )
51 50 ex ⊢ ( 𝜑 → ( ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) → ( ( 2nd ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) < ( 1 / 𝑛 ) → ( ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑛 ) ) ∖ ( 𝑀 ‘ 𝑛 ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) ) )
52 51 3impd ⊢ ( 𝜑 → ( ( ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) ∧ ( 2nd ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) < ( 1 / 𝑛 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑛 ) ) ∖ ( 𝑀 ‘ 𝑛 ) ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑛 ) ) ) )
53 52 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) ∧ ( 2nd ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) < ( 1 / 𝑛 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑛 ) ) ∖ ( 𝑀 ‘ 𝑛 ) ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑛 ) ) ) )
54 21 53 mpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑛 ) ) )
55 54 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑛 ) ) )