Metamath Proof Explorer

Theorem bcthlem4

Description: Lemma for bcth . Given any open ball ( C ( ballD ) R ) as starting point (and in particular, a ball in int ( U. ran M ) ), the limit point x of the centers of the induced sequence of balls g is outside U. ran M . Note that a set A has empty interior iff every nonempty open set U contains points outside A , i.e. ( U \ A ) =/= (/) . (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 bcthlem4 ( 𝜑 → ( ( 𝐶 ( ball ‘ 𝐷 ) 𝑅 ) ∖ ∪ ran 𝑀 ) ≠ ∅ )

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 cmetmet ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
11 2 10 syl ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
12 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
13 11 12 syl ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
14 1 2 3 4 5 6 7 8 9 bcthlem2 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑛 ) ) )
15 elrp ⊢ ( 𝑟 ∈ ℝ+ ↔ ( 𝑟 ∈ ℝ ∧ 0 < 𝑟 ) )
16 nnrecl ⊢ ( ( 𝑟 ∈ ℝ ∧ 0 < 𝑟 ) → ∃ 𝑚 ∈ ℕ ( 1 / 𝑚 ) < 𝑟 )
17 15 16 sylbi ⊢ ( 𝑟 ∈ ℝ+ → ∃ 𝑚 ∈ ℕ ( 1 / 𝑚 ) < 𝑟 )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑚 ∈ ℕ ( 1 / 𝑚 ) < 𝑟 )
19 peano2nn ⊢ ( 𝑚 ∈ ℕ → ( 𝑚 + 1 ) ∈ ℕ )
20 19 adantl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑚 ∈ ℕ ) → ( 𝑚 + 1 ) ∈ ℕ )
21 fvoveq1 ⊢ ( 𝑘 = 𝑚 → ( 𝑔 ‘ ( 𝑘 + 1 ) ) = ( 𝑔 ‘ ( 𝑚 + 1 ) ) )
22 id ⊢ ( 𝑘 = 𝑚 → 𝑘 = 𝑚 )
23 fveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝑔 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑚 ) )
24 22 23 oveq12d ⊢ ( 𝑘 = 𝑚 → ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) = ( 𝑚 𝐹 ( 𝑔 ‘ 𝑚 ) ) )
25 21 24 eleq12d ⊢ ( 𝑘 = 𝑚 → ( ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ↔ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑔 ‘ 𝑚 ) ) ) )
26 25 rspccva ⊢ ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ∧ 𝑚 ∈ ℕ ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑔 ‘ 𝑚 ) ) )
27 9 26 sylan ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑔 ‘ 𝑚 ) ) )
28 7 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑔 ‘ 𝑚 ) ∈ ( 𝑋 × ℝ+ ) )
29 1 2 3 bcthlem1 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑔 ‘ 𝑚 ) ∈ ( 𝑋 × ℝ+ ) ) ) → ( ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑔 ‘ 𝑚 ) ) ↔ ( ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) ∧ ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < ( 1 / 𝑚 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑚 ) ) ∖ ( 𝑀 ‘ 𝑚 ) ) ) ) )
30 29 expr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑔 ‘ 𝑚 ) ∈ ( 𝑋 × ℝ+ ) → ( ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑔 ‘ 𝑚 ) ) ↔ ( ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) ∧ ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < ( 1 / 𝑚 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑚 ) ) ∖ ( 𝑀 ‘ 𝑚 ) ) ) ) ) )
31 28 30 mpd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑔 ‘ 𝑚 ) ) ↔ ( ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) ∧ ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < ( 1 / 𝑚 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑚 ) ) ∖ ( 𝑀 ‘ 𝑚 ) ) ) ) )
32 27 31 mpbid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) ∧ ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < ( 1 / 𝑚 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑚 ) ) ∖ ( 𝑀 ‘ 𝑚 ) ) ) )
33 32 simp2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < ( 1 / 𝑚 ) )
34 33 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑚 ∈ ℕ ) → ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < ( 1 / 𝑚 ) )
35 32 simp1d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) )
36 xp2nd ⊢ ( ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) → ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ∈ ℝ+ )
37 35 36 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ∈ ℝ+ )
38 37 rpred ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ∈ ℝ )
39 38 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑚 ∈ ℕ ) → ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ∈ ℝ )
40 nnrecre ⊢ ( 𝑚 ∈ ℕ → ( 1 / 𝑚 ) ∈ ℝ )
41 40 adantl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑚 ∈ ℕ ) → ( 1 / 𝑚 ) ∈ ℝ )
42 rpre ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ )
43 42 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑚 ∈ ℕ ) → 𝑟 ∈ ℝ )
44 lttr ⊢ ( ( ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ∈ ℝ ∧ ( 1 / 𝑚 ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( ( ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < ( 1 / 𝑚 ) ∧ ( 1 / 𝑚 ) < 𝑟 ) → ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < 𝑟 ) )
45 39 41 43 44 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑚 ∈ ℕ ) → ( ( ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < ( 1 / 𝑚 ) ∧ ( 1 / 𝑚 ) < 𝑟 ) → ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < 𝑟 ) )
46 34 45 mpand ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑚 ∈ ℕ ) → ( ( 1 / 𝑚 ) < 𝑟 → ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < 𝑟 ) )
47 2fveq3 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) = ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) )
48 47 breq1d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) < 𝑟 ↔ ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < 𝑟 ) )
49 48 rspcev ⊢ ( ( ( 𝑚 + 1 ) ∈ ℕ ∧ ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < 𝑟 ) → ∃ 𝑛 ∈ ℕ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) < 𝑟 )
50 20 46 49 syl6an ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑚 ∈ ℕ ) → ( ( 1 / 𝑚 ) < 𝑟 → ∃ 𝑛 ∈ ℕ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) < 𝑟 ) )
51 50 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑚 ∈ ℕ ( 1 / 𝑚 ) < 𝑟 → ∃ 𝑛 ∈ ℕ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) < 𝑟 ) )
52 18 51 mpd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑛 ∈ ℕ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) < 𝑟 )
53 52 ralrimiva ⊢ ( 𝜑 → ∀ 𝑟 ∈ ℝ+ ∃ 𝑛 ∈ ℕ ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) < 𝑟 )
54 13 7 14 53 caubl ⊢ ( 𝜑 → ( 1st ∘ 𝑔 ) ∈ ( Cau ‘ 𝐷 ) )
55 1 cmetcau ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ ( 1st ∘ 𝑔 ) ∈ ( Cau ‘ 𝐷 ) ) → ( 1st ∘ 𝑔 ) ∈ dom ( ⇝𝑡 ‘ 𝐽 ) )
56 2 54 55 syl2anc ⊢ ( 𝜑 → ( 1st ∘ 𝑔 ) ∈ dom ( ⇝𝑡 ‘ 𝐽 ) )
57 fo1st ⊢ 1st : V –onto→ V
58 fofun ⊢ ( 1st : V –onto→ V → Fun 1st )
59 57 58 ax-mp ⊢ Fun 1st
60 vex ⊢ 𝑔 ∈ V
61 cofunexg ⊢ ( ( Fun 1st ∧ 𝑔 ∈ V ) → ( 1st ∘ 𝑔 ) ∈ V )
62 59 60 61 mp2an ⊢ ( 1st ∘ 𝑔 ) ∈ V
63 62 eldm ⊢ ( ( 1st ∘ 𝑔 ) ∈ dom ( ⇝𝑡 ‘ 𝐽 ) ↔ ∃ 𝑥 ( 1st ∘ 𝑔 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑥 )
64 56 63 sylib ⊢ ( 𝜑 → ∃ 𝑥 ( 1st ∘ 𝑔 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑥 )
65 1nn ⊢ 1 ∈ ℕ
66 1 2 3 4 5 6 7 8 9 bcthlem3 ⊢ ( ( 𝜑 ∧ ( 1st ∘ 𝑔 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ∧ 1 ∈ ℕ ) → 𝑥 ∈ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 1 ) ) )
67 65 66 mp3an3 ⊢ ( ( 𝜑 ∧ ( 1st ∘ 𝑔 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 1 ) ) )
68 8 fveq2d ⊢ ( 𝜑 → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 1 ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ 𝐶 , 𝑅 ⟩ ) )
69 df-ov ⊢ ( 𝐶 ( ball ‘ 𝐷 ) 𝑅 ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ 𝐶 , 𝑅 ⟩ )
70 68 69 eqtr4di ⊢ ( 𝜑 → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 1 ) ) = ( 𝐶 ( ball ‘ 𝐷 ) 𝑅 ) )
71 70 adantr ⊢ ( ( 𝜑 ∧ ( 1st ∘ 𝑔 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 1 ) ) = ( 𝐶 ( ball ‘ 𝐷 ) 𝑅 ) )
72 67 71 eleqtrd ⊢ ( ( 𝜑 ∧ ( 1st ∘ 𝑔 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ ( 𝐶 ( ball ‘ 𝐷 ) 𝑅 ) )
73 1 mopntop ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
74 13 73 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
75 74 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝐽 ∈ Top )
76 13 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
77 xp1st ⊢ ( ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) → ( 1st ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ∈ 𝑋 )
78 35 77 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 1st ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ∈ 𝑋 )
79 37 rpxrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ∈ ℝ* )
80 blssm ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 1st ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ∈ 𝑋 ∧ ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ∈ ℝ* ) → ( ( 1st ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ( ball ‘ 𝐷 ) ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ) ⊆ 𝑋 )
81 76 78 79 80 syl3anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 1st ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ( ball ‘ 𝐷 ) ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ) ⊆ 𝑋 )
82 df-ov ⊢ ( ( 1st ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ( ball ‘ 𝐷 ) ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 1st ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) , ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ⟩ )
83 1st2nd2 ⊢ ( ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑋 × ℝ+ ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) = ⟨ ( 1st ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) , ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ⟩ )
84 35 83 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) = ⟨ ( 1st ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) , ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ⟩ )
85 84 fveq2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 1st ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) , ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ⟩ ) )
86 82 85 eqtr4id ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 1st ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ( ball ‘ 𝐷 ) ( 2nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ) = ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) )
87 1 mopnuni ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
88 13 87 syl ⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
89 88 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑋 = ∪ 𝐽 )
90 81 86 89 3sstr3d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ⊆ ∪ 𝐽 )
91 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
92 91 sscls ⊢ ( ( 𝐽 ∈ Top ∧ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ⊆ ∪ 𝐽 ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ) )
93 75 90 92 syl2anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ) )
94 32 simp3d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑚 ) ) ∖ ( 𝑀 ‘ 𝑚 ) ) )
95 93 94 sstrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑚 ) ) ∖ ( 𝑀 ‘ 𝑚 ) ) )
96 95 3adant2 ⊢ ( ( 𝜑 ∧ ( 1st ∘ 𝑔 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ∧ 𝑚 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑚 ) ) ∖ ( 𝑀 ‘ 𝑚 ) ) )
97 1 2 3 4 5 6 7 8 9 bcthlem3 ⊢ ( ( 𝜑 ∧ ( 1st ∘ 𝑔 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ∧ ( 𝑚 + 1 ) ∈ ℕ ) → 𝑥 ∈ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) )
98 19 97 syl3an3 ⊢ ( ( 𝜑 ∧ ( 1st ∘ 𝑔 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ∧ 𝑚 ∈ ℕ ) → 𝑥 ∈ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) )
99 96 98 sseldd ⊢ ( ( 𝜑 ∧ ( 1st ∘ 𝑔 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ∧ 𝑚 ∈ ℕ ) → 𝑥 ∈ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑚 ) ) ∖ ( 𝑀 ‘ 𝑚 ) ) )
100 99 eldifbd ⊢ ( ( 𝜑 ∧ ( 1st ∘ 𝑔 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ∧ 𝑚 ∈ ℕ ) → ¬ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) )
101 100 3expa ⊢ ( ( ( 𝜑 ∧ ( 1st ∘ 𝑔 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑚 ∈ ℕ ) → ¬ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) )
102 101 ralrimiva ⊢ ( ( 𝜑 ∧ ( 1st ∘ 𝑔 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → ∀ 𝑚 ∈ ℕ ¬ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) )
103 eluni2 ⊢ ( 𝑥 ∈ ∪ ran 𝑀 ↔ ∃ 𝑦 ∈ ran 𝑀 𝑥 ∈ 𝑦 )
104 4 ffnd ⊢ ( 𝜑 → 𝑀 Fn ℕ )
105 eleq2 ⊢ ( 𝑦 = ( 𝑀 ‘ 𝑚 ) → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) ) )
106 105 rexrn ⊢ ( 𝑀 Fn ℕ → ( ∃ 𝑦 ∈ ran 𝑀 𝑥 ∈ 𝑦 ↔ ∃ 𝑚 ∈ ℕ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) ) )
107 104 106 syl ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ran 𝑀 𝑥 ∈ 𝑦 ↔ ∃ 𝑚 ∈ ℕ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) ) )
108 103 107 bitrid ⊢ ( 𝜑 → ( 𝑥 ∈ ∪ ran 𝑀 ↔ ∃ 𝑚 ∈ ℕ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) ) )
109 108 notbid ⊢ ( 𝜑 → ( ¬ 𝑥 ∈ ∪ ran 𝑀 ↔ ¬ ∃ 𝑚 ∈ ℕ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) ) )
110 ralnex ⊢ ( ∀ 𝑚 ∈ ℕ ¬ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) ↔ ¬ ∃ 𝑚 ∈ ℕ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) )
111 109 110 bitr4di ⊢ ( 𝜑 → ( ¬ 𝑥 ∈ ∪ ran 𝑀 ↔ ∀ 𝑚 ∈ ℕ ¬ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) ) )
112 111 biimpar ⊢ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ ¬ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) ) → ¬ 𝑥 ∈ ∪ ran 𝑀 )
113 102 112 syldan ⊢ ( ( 𝜑 ∧ ( 1st ∘ 𝑔 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → ¬ 𝑥 ∈ ∪ ran 𝑀 )
114 72 113 eldifd ⊢ ( ( 𝜑 ∧ ( 1st ∘ 𝑔 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ ( ( 𝐶 ( ball ‘ 𝐷 ) 𝑅 ) ∖ ∪ ran 𝑀 ) )
115 114 ne0d ⊢ ( ( 𝜑 ∧ ( 1st ∘ 𝑔 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → ( ( 𝐶 ( ball ‘ 𝐷 ) 𝑅 ) ∖ ∪ ran 𝑀 ) ≠ ∅ )
116 64 115 exlimddv ⊢ ( 𝜑 → ( ( 𝐶 ( ball ‘ 𝐷 ) 𝑅 ) ∖ ∪ ran 𝑀 ) ≠ ∅ )