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 𝑀 ) β‰  βˆ… )