This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iscmet3lem2

Description: Lemma for iscmet3 . (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses iscmet3.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
iscmet3.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
iscmet3.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
iscmet3.4 ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
iscmet3.6 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ 𝑋 )
iscmet3.9 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℤ ∀ 𝑢 ∈ ( 𝑆 ‘ 𝑘 ) ∀ 𝑣 ∈ ( 𝑆 ‘ 𝑘 ) ( 𝑢 𝐷 𝑣 ) < ( ( 1 / 2 ) ↑ 𝑘 ) )
iscmet3.10 ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ∀ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑛 ) )
iscmet3.7 ⊢ ( 𝜑 → 𝐺 ∈ ( Fil ‘ 𝑋 ) )
iscmet3.8 ⊢ ( 𝜑 → 𝑆 : ℤ ⟶ 𝐺 )
iscmet3.5 ⊢ ( 𝜑 → 𝐹 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) )
Assertion iscmet3lem2 ( 𝜑 → ( 𝐽 fLim 𝐺 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 iscmet3.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 iscmet3.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
3 iscmet3.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 iscmet3.4 ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
5 iscmet3.6 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ 𝑋 )
6 iscmet3.9 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℤ ∀ 𝑢 ∈ ( 𝑆 ‘ 𝑘 ) ∀ 𝑣 ∈ ( 𝑆 ‘ 𝑘 ) ( 𝑢 𝐷 𝑣 ) < ( ( 1 / 2 ) ↑ 𝑘 ) )
7 iscmet3.10 ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ∀ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑛 ) )
8 iscmet3.7 ⊢ ( 𝜑 → 𝐺 ∈ ( Fil ‘ 𝑋 ) )
9 iscmet3.8 ⊢ ( 𝜑 → 𝑆 : ℤ ⟶ 𝐺 )
10 iscmet3.5 ⊢ ( 𝜑 → 𝐹 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) )
11 eldmg ⊢ ( 𝐹 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) → ( 𝐹 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) ↔ ∃ 𝑥 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) )
12 11 ibi ⊢ ( 𝐹 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) → ∃ 𝑥 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 )
13 10 12 syl ⊢ ( 𝜑 → ∃ 𝑥 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 )
14 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
15 4 14 syl ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
16 2 mopntopon ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
17 15 16 syl ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
18 lmcl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ 𝑋 )
19 17 18 sylan ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ 𝑋 )
20 15 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
21 2 mopni2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 )
22 21 3expia ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ∈ 𝑦 → ∃ 𝑟 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 ) )
23 20 22 sylan ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ∈ 𝑦 → ∃ 𝑟 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 ) )
24 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 ) ) → 𝐺 ∈ ( Fil ‘ 𝑋 ) )
25 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) → 𝑀 ∈ ℤ )
26 rphalfcl ⊢ ( 𝑟 ∈ ℝ+ → ( 𝑟 / 2 ) ∈ ℝ+ )
27 26 adantl ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑟 / 2 ) ∈ ℝ+ )
28 1 iscmet3lem3 ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑟 / 2 ) ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) )
29 25 27 28 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) )
30 20 adantr ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
31 19 adantr ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) → 𝑥 ∈ 𝑋 )
32 blcntr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑟 / 2 ) ∈ ℝ+ ) → 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) )
33 30 31 27 32 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) → 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) )
34 simplr ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 )
35 27 rpxrd ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑟 / 2 ) ∈ ℝ* )
36 2 blopn ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑟 / 2 ) ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∈ 𝐽 )
37 30 31 35 36 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∈ 𝐽 )
38 1 33 25 34 37 lmcvg ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) )
39 1 rexanuz2 ⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ↔ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) )
40 1 r19.2uz ⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) → ∃ 𝑘 ∈ 𝑍 ( ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) )
41 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ ( ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ) ) → 𝐺 ∈ ( Fil ‘ 𝑋 ) )
42 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ ( ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ) ) → 𝑆 : ℤ ⟶ 𝐺 )
43 eluzelz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℤ )
44 43 1 eleq2s ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ )
45 44 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ ( ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ) ) → 𝑘 ∈ ℤ )
46 ffvelcdm ⊢ ( ( 𝑆 : ℤ ⟶ 𝐺 ∧ 𝑘 ∈ ℤ ) → ( 𝑆 ‘ 𝑘 ) ∈ 𝐺 )
47 42 45 46 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ ( ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ) ) → ( 𝑆 ‘ 𝑘 ) ∈ 𝐺 )
48 rpxr ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ* )
49 48 adantl ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ* )
50 blssm ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑋 )
51 30 31 49 50 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑋 )
52 51 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ ( ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑋 )
53 44 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ℤ )
54 1rp ⊢ 1 ∈ ℝ+
55 rphalfcl ⊢ ( 1 ∈ ℝ+ → ( 1 / 2 ) ∈ ℝ+ )
56 54 55 ax-mp ⊢ ( 1 / 2 ) ∈ ℝ+
57 rpexpcl ⊢ ( ( ( 1 / 2 ) ∈ ℝ+ ∧ 𝑘 ∈ ℤ ) → ( ( 1 / 2 ) ↑ 𝑘 ) ∈ ℝ+ )
58 56 57 mpan ⊢ ( 𝑘 ∈ ℤ → ( ( 1 / 2 ) ↑ 𝑘 ) ∈ ℝ+ )
59 53 58 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 1 / 2 ) ↑ 𝑘 ) ∈ ℝ+ )
60 59 rpred ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 1 / 2 ) ↑ 𝑘 ) ∈ ℝ )
61 27 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝑟 / 2 ) ∈ ℝ+ )
62 61 rpred ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝑟 / 2 ) ∈ ℝ )
63 ltle ⊢ ( ( ( ( 1 / 2 ) ↑ 𝑘 ) ∈ ℝ ∧ ( 𝑟 / 2 ) ∈ ℝ ) → ( ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) → ( ( 1 / 2 ) ↑ 𝑘 ) ≤ ( 𝑟 / 2 ) ) )
64 60 62 63 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) → ( ( 1 / 2 ) ↑ 𝑘 ) ≤ ( 𝑟 / 2 ) ) )
65 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑆 ‘ 𝑛 ) = ( 𝑆 ‘ 𝑘 ) )
66 65 eleq2d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑛 ) ↔ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑘 ) ) )
67 7 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ∀ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑛 ) )
68 eluzfz2 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ( 𝑀 ... 𝑘 ) )
69 68 1 eleq2s ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ( 𝑀 ... 𝑘 ) )
70 69 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ( 𝑀 ... 𝑘 ) )
71 66 67 70 rspcdva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑘 ) )
72 71 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑆 ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑘 ) )
73 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑆 ‘ 𝑘 ) ) → 𝑦 ∈ ( 𝑆 ‘ 𝑘 ) )
74 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑆 ‘ 𝑘 ) ) → ∀ 𝑘 ∈ ℤ ∀ 𝑢 ∈ ( 𝑆 ‘ 𝑘 ) ∀ 𝑣 ∈ ( 𝑆 ‘ 𝑘 ) ( 𝑢 𝐷 𝑣 ) < ( ( 1 / 2 ) ↑ 𝑘 ) )
75 44 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑆 ‘ 𝑘 ) ) → 𝑘 ∈ ℤ )
76 rsp ⊢ ( ∀ 𝑘 ∈ ℤ ∀ 𝑢 ∈ ( 𝑆 ‘ 𝑘 ) ∀ 𝑣 ∈ ( 𝑆 ‘ 𝑘 ) ( 𝑢 𝐷 𝑣 ) < ( ( 1 / 2 ) ↑ 𝑘 ) → ( 𝑘 ∈ ℤ → ∀ 𝑢 ∈ ( 𝑆 ‘ 𝑘 ) ∀ 𝑣 ∈ ( 𝑆 ‘ 𝑘 ) ( 𝑢 𝐷 𝑣 ) < ( ( 1 / 2 ) ↑ 𝑘 ) ) )
77 74 75 76 sylc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑆 ‘ 𝑘 ) ) → ∀ 𝑢 ∈ ( 𝑆 ‘ 𝑘 ) ∀ 𝑣 ∈ ( 𝑆 ‘ 𝑘 ) ( 𝑢 𝐷 𝑣 ) < ( ( 1 / 2 ) ↑ 𝑘 ) )
78 oveq1 ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑘 ) → ( 𝑢 𝐷 𝑣 ) = ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑣 ) )
79 78 breq1d ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑘 ) → ( ( 𝑢 𝐷 𝑣 ) < ( ( 1 / 2 ) ↑ 𝑘 ) ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑣 ) < ( ( 1 / 2 ) ↑ 𝑘 ) ) )
80 oveq2 ⊢ ( 𝑣 = 𝑦 → ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑣 ) = ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) )
81 80 breq1d ⊢ ( 𝑣 = 𝑦 → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑣 ) < ( ( 1 / 2 ) ↑ 𝑘 ) ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < ( ( 1 / 2 ) ↑ 𝑘 ) ) )
82 79 81 rspc2va ⊢ ( ( ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑘 ) ∧ 𝑦 ∈ ( 𝑆 ‘ 𝑘 ) ) ∧ ∀ 𝑢 ∈ ( 𝑆 ‘ 𝑘 ) ∀ 𝑣 ∈ ( 𝑆 ‘ 𝑘 ) ( 𝑢 𝐷 𝑣 ) < ( ( 1 / 2 ) ↑ 𝑘 ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < ( ( 1 / 2 ) ↑ 𝑘 ) )
83 72 73 77 82 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑆 ‘ 𝑘 ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < ( ( 1 / 2 ) ↑ 𝑘 ) )
84 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑆 ‘ 𝑘 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
85 44 58 syl ⊢ ( 𝑘 ∈ 𝑍 → ( ( 1 / 2 ) ↑ 𝑘 ) ∈ ℝ+ )
86 85 rpxrd ⊢ ( 𝑘 ∈ 𝑍 → ( ( 1 / 2 ) ↑ 𝑘 ) ∈ ℝ* )
87 86 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑆 ‘ 𝑘 ) ) → ( ( 1 / 2 ) ↑ 𝑘 ) ∈ ℝ* )
88 5 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
89 88 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑆 ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
90 8 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐺 ∈ ( Fil ‘ 𝑋 ) )
91 9 44 46 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑆 ‘ 𝑘 ) ∈ 𝐺 )
92 filelss ⊢ ( ( 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑆 ‘ 𝑘 ) ∈ 𝐺 ) → ( 𝑆 ‘ 𝑘 ) ⊆ 𝑋 )
93 90 91 92 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑆 ‘ 𝑘 ) ⊆ 𝑋 )
94 93 sselda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑆 ‘ 𝑘 ) ) → 𝑦 ∈ 𝑋 )
95 elbl2 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 1 / 2 ) ↑ 𝑘 ) ∈ ℝ* ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑦 ∈ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( ( 1 / 2 ) ↑ 𝑘 ) ) ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < ( ( 1 / 2 ) ↑ 𝑘 ) ) )
96 84 87 89 94 95 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑆 ‘ 𝑘 ) ) → ( 𝑦 ∈ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( ( 1 / 2 ) ↑ 𝑘 ) ) ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < ( ( 1 / 2 ) ↑ 𝑘 ) ) )
97 83 96 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑆 ‘ 𝑘 ) ) → 𝑦 ∈ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( ( 1 / 2 ) ↑ 𝑘 ) ) )
98 97 ex ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑦 ∈ ( 𝑆 ‘ 𝑘 ) → 𝑦 ∈ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( ( 1 / 2 ) ↑ 𝑘 ) ) ) )
99 98 ssrdv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑆 ‘ 𝑘 ) ⊆ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( ( 1 / 2 ) ↑ 𝑘 ) ) )
100 99 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝑆 ‘ 𝑘 ) ⊆ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( ( 1 / 2 ) ↑ 𝑘 ) ) )
101 30 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
102 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) → 𝐹 : 𝑍 ⟶ 𝑋 )
103 102 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
104 59 rpxrd ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 1 / 2 ) ↑ 𝑘 ) ∈ ℝ* )
105 35 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝑟 / 2 ) ∈ ℝ* )
106 ssbl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ( ( ( 1 / 2 ) ↑ 𝑘 ) ∈ ℝ* ∧ ( 𝑟 / 2 ) ∈ ℝ* ) ∧ ( ( 1 / 2 ) ↑ 𝑘 ) ≤ ( 𝑟 / 2 ) ) → ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( ( 1 / 2 ) ↑ 𝑘 ) ) ⊆ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) )
107 106 3expia ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ( ( ( 1 / 2 ) ↑ 𝑘 ) ∈ ℝ* ∧ ( 𝑟 / 2 ) ∈ ℝ* ) ) → ( ( ( 1 / 2 ) ↑ 𝑘 ) ≤ ( 𝑟 / 2 ) → ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( ( 1 / 2 ) ↑ 𝑘 ) ) ⊆ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) )
108 101 103 104 105 107 syl22anc ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 1 / 2 ) ↑ 𝑘 ) ≤ ( 𝑟 / 2 ) → ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( ( 1 / 2 ) ↑ 𝑘 ) ) ⊆ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) )
109 sstr ⊢ ( ( ( 𝑆 ‘ 𝑘 ) ⊆ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( ( 1 / 2 ) ↑ 𝑘 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( ( 1 / 2 ) ↑ 𝑘 ) ) ⊆ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) → ( 𝑆 ‘ 𝑘 ) ⊆ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) )
110 100 108 109 syl6an ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 1 / 2 ) ↑ 𝑘 ) ≤ ( 𝑟 / 2 ) → ( 𝑆 ‘ 𝑘 ) ⊆ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) )
111 64 110 syld ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) → ( 𝑆 ‘ 𝑘 ) ⊆ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) )
112 111 adantrd ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) → ( 𝑆 ‘ 𝑘 ) ⊆ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) )
113 112 impr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ ( ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ) ) → ( 𝑆 ‘ 𝑘 ) ⊆ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) )
114 31 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → 𝑥 ∈ 𝑋 )
115 blcom ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑟 / 2 ) ∈ ℝ* ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ↔ 𝑥 ∈ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) )
116 101 105 114 103 115 syl22anc ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ↔ 𝑥 ∈ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) )
117 rpre ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ )
118 117 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → 𝑟 ∈ ℝ )
119 blhalf ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ ∧ 𝑥 ∈ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ) → ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) )
120 119 expr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ ) → ( 𝑥 ∈ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) → ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) )
121 101 103 118 120 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝑥 ∈ ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) → ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) )
122 116 121 sylbid ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) → ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) )
123 122 adantld ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) → ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) )
124 123 impr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ ( ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ) ) → ( ( 𝐹 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) )
125 113 124 sstrd ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ ( ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ) ) → ( 𝑆 ‘ 𝑘 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) )
126 filss ⊢ ( ( 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑆 ‘ 𝑘 ) ∈ 𝐺 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑋 ∧ ( 𝑆 ‘ 𝑘 ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐺 )
127 41 47 52 125 126 syl13anc ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ ( ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐺 )
128 127 rexlimdvaa ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑘 ∈ 𝑍 ( ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐺 ) )
129 40 128 syl5 ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐺 ) )
130 39 129 biimtrrid ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) → ( ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 1 / 2 ) ↑ 𝑘 ) < ( 𝑟 / 2 ) ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐺 ) )
131 29 38 130 mp2and ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐺 )
132 131 ad2ant2r ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐺 )
133 17 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
134 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) → 𝑦 ⊆ 𝑋 )
135 133 134 sylan ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑦 ∈ 𝐽 ) → 𝑦 ⊆ 𝑋 )
136 135 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 ) ) → 𝑦 ⊆ 𝑋 )
137 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 )
138 filss ⊢ ( ( 𝐺 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐺 ∧ 𝑦 ⊆ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 ) ) → 𝑦 ∈ 𝐺 )
139 24 132 136 137 138 syl13anc ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 ) ) → 𝑦 ∈ 𝐺 )
140 139 rexlimdvaa ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑦 ∈ 𝐽 ) → ( ∃ 𝑟 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 → 𝑦 ∈ 𝐺 ) )
141 23 140 syld ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐺 ) )
142 141 ralrimiva ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐺 ) )
143 flimopn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐺 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐺 ) ) ) )
144 17 8 143 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐺 ) ) ) )
145 144 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐺 ) ) ) )
146 19 142 145 mpbir2and ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ ( 𝐽 fLim 𝐺 ) )
147 146 ne0d ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → ( 𝐽 fLim 𝐺 ) ≠ ∅ )
148 13 147 exlimddv ⊢ ( 𝜑 → ( 𝐽 fLim 𝐺 ) ≠ ∅ )