Metamath Proof Explorer

Theorem ulmss

Description: A uniform limit of functions is still a uniform limit if restricted to a subset. (Contributed by Mario Carneiro, 3-Mar-2015)

Ref Expression
Hypotheses ulmss.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
ulmss.t ⊢ ( 𝜑 → 𝑇 ⊆ 𝑆 )
ulmss.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐴 ∈ 𝑊 )
ulmss.u ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
Assertion ulmss ( 𝜑 → ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ( ⇝𝑢 ‘ 𝑇 ) ( 𝐺 ↾ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 ulmss.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 ulmss.t ⊢ ( 𝜑 → 𝑇 ⊆ 𝑆 )
3 ulmss.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐴 ∈ 𝑊 )
4 ulmss.u ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
5 1 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
6 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑇 ⊆ 𝑆 )
7 ssralv ⊢ ( 𝑇 ⊆ 𝑆 → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 → ∀ 𝑧 ∈ 𝑇 ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 ) )
8 6 7 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 → ∀ 𝑧 ∈ 𝑇 ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 ) )
9 fvres ⊢ ( 𝑧 ∈ 𝑇 → ( ( 𝐴 ↾ 𝑇 ) ‘ 𝑧 ) = ( 𝐴 ‘ 𝑧 ) )
10 9 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝐴 ↾ 𝑇 ) ‘ 𝑧 ) = ( 𝐴 ‘ 𝑧 ) )
11 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇 ) ) → 𝑥 ∈ 𝑍 )
12 3 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇 ) ) → 𝐴 ∈ 𝑊 )
13 12 resexd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇 ) ) → ( 𝐴 ↾ 𝑇 ) ∈ V )
14 eqid ⊢ ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) = ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) )
15 14 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝑍 ∧ ( 𝐴 ↾ 𝑇 ) ∈ V ) → ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑥 ) = ( 𝐴 ↾ 𝑇 ) )
16 11 13 15 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑥 ) = ( 𝐴 ↾ 𝑇 ) )
17 16 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑥 ) ‘ 𝑧 ) = ( ( 𝐴 ↾ 𝑇 ) ‘ 𝑧 ) )
18 eqid ⊢ ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑍 ↦ 𝐴 )
19 18 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝑍 ∧ 𝐴 ∈ 𝑊 ) → ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 )
20 11 12 19 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 )
21 20 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑥 ) ‘ 𝑧 ) = ( 𝐴 ‘ 𝑧 ) )
22 10 17 21 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑥 ) ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑥 ) ‘ 𝑧 ) )
23 22 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑍 ∀ 𝑧 ∈ 𝑇 ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑥 ) ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑥 ) ‘ 𝑧 ) )
24 nfv ⊢ Ⅎ 𝑘 ∀ 𝑧 ∈ 𝑇 ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑥 ) ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑥 ) ‘ 𝑧 )
25 nfcv ⊢ Ⅎ 𝑥 𝑇
26 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 )
27 nfcv ⊢ Ⅎ 𝑥 𝑧
28 26 27 nffv ⊢ Ⅎ 𝑥 ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 )
29 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 )
30 29 27 nffv ⊢ Ⅎ 𝑥 ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 )
31 28 30 nfeq ⊢ Ⅎ 𝑥 ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 )
32 25 31 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑧 ∈ 𝑇 ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 )
33 fveq2 ⊢ ( 𝑥 = 𝑘 → ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) )
34 33 fveq1d ⊢ ( 𝑥 = 𝑘 → ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑥 ) ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) )
35 fveq2 ⊢ ( 𝑥 = 𝑘 → ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) )
36 35 fveq1d ⊢ ( 𝑥 = 𝑘 → ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑥 ) ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) )
37 34 36 eqeq12d ⊢ ( 𝑥 = 𝑘 → ( ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑥 ) ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑥 ) ‘ 𝑧 ) ↔ ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) ) )
38 37 ralbidv ⊢ ( 𝑥 = 𝑘 → ( ∀ 𝑧 ∈ 𝑇 ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑥 ) ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑥 ) ‘ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝑇 ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) ) )
39 24 32 38 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝑍 ∀ 𝑧 ∈ 𝑇 ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑥 ) ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑥 ) ‘ 𝑧 ) ↔ ∀ 𝑘 ∈ 𝑍 ∀ 𝑧 ∈ 𝑇 ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) )
40 23 39 sylib ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ∀ 𝑧 ∈ 𝑇 ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) )
41 40 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ∀ 𝑧 ∈ 𝑇 ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) )
42 fvoveq1 ⊢ ( ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) → ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) = ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) )
43 42 breq1d ⊢ ( ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) → ( ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 ↔ ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 ) )
44 43 ralimi ⊢ ( ∀ 𝑧 ∈ 𝑇 ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) → ∀ 𝑧 ∈ 𝑇 ( ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 ↔ ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 ) )
45 ralbi ⊢ ( ∀ 𝑧 ∈ 𝑇 ( ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 ↔ ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 ) → ( ∀ 𝑧 ∈ 𝑇 ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 ↔ ∀ 𝑧 ∈ 𝑇 ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 ) )
46 41 44 45 3syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ∀ 𝑧 ∈ 𝑇 ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 ↔ ∀ 𝑧 ∈ 𝑇 ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 ) )
47 8 46 sylibrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 → ∀ 𝑧 ∈ 𝑇 ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 ) )
48 5 47 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 → ∀ 𝑧 ∈ 𝑇 ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 ) )
49 48 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 → ∀ 𝑧 ∈ 𝑇 ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 ) )
50 49 ralimdva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑇 ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 ) )
51 50 reximdva ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑇 ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 ) )
52 51 ralimdv ⊢ ( 𝜑 → ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 → ∀ 𝑟 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑇 ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 ) )
53 ulmf ⊢ ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → ∃ 𝑚 ∈ ℤ ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) : ( ℤ≥ ‘ 𝑚 ) ⟶ ( ℂ ↑m 𝑆 ) )
54 4 53 syl ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℤ ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) : ( ℤ≥ ‘ 𝑚 ) ⟶ ( ℂ ↑m 𝑆 ) )
55 fdm ⊢ ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) : ( ℤ≥ ‘ 𝑚 ) ⟶ ( ℂ ↑m 𝑆 ) → dom ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) = ( ℤ≥ ‘ 𝑚 ) )
56 18 dmmptss ⊢ dom ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ⊆ 𝑍
57 55 56 eqsstrrdi ⊢ ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) : ( ℤ≥ ‘ 𝑚 ) ⟶ ( ℂ ↑m 𝑆 ) → ( ℤ≥ ‘ 𝑚 ) ⊆ 𝑍 )
58 uzid ⊢ ( 𝑚 ∈ ℤ → 𝑚 ∈ ( ℤ≥ ‘ 𝑚 ) )
59 58 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑚 ) )
60 ssel ⊢ ( ( ℤ≥ ‘ 𝑚 ) ⊆ 𝑍 → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑚 ) → 𝑚 ∈ 𝑍 ) )
61 eluzel2 ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
62 61 1 eleq2s ⊢ ( 𝑚 ∈ 𝑍 → 𝑀 ∈ ℤ )
63 60 62 syl6 ⊢ ( ( ℤ≥ ‘ 𝑚 ) ⊆ 𝑍 → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑚 ) → 𝑀 ∈ ℤ ) )
64 57 59 63 syl2imc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) : ( ℤ≥ ‘ 𝑚 ) ⟶ ( ℂ ↑m 𝑆 ) → 𝑀 ∈ ℤ ) )
65 64 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ℤ ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) : ( ℤ≥ ‘ 𝑚 ) ⟶ ( ℂ ↑m 𝑆 ) → 𝑀 ∈ ℤ ) )
66 54 65 mpd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
67 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑍 𝐴 ∈ 𝑊 )
68 18 fnmpt ⊢ ( ∀ 𝑥 ∈ 𝑍 𝐴 ∈ 𝑊 → ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) Fn 𝑍 )
69 67 68 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) Fn 𝑍 )
70 frn ⊢ ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) : ( ℤ≥ ‘ 𝑚 ) ⟶ ( ℂ ↑m 𝑆 ) → ran ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ⊆ ( ℂ ↑m 𝑆 ) )
71 70 rexlimivw ⊢ ( ∃ 𝑚 ∈ ℤ ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) : ( ℤ≥ ‘ 𝑚 ) ⟶ ( ℂ ↑m 𝑆 ) → ran ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ⊆ ( ℂ ↑m 𝑆 ) )
72 54 71 syl ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ⊆ ( ℂ ↑m 𝑆 ) )
73 df-f ⊢ ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) ↔ ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) Fn 𝑍 ∧ ran ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ⊆ ( ℂ ↑m 𝑆 ) ) )
74 69 72 73 sylanbrc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
75 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) )
76 eqidd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
77 ulmcl ⊢ ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝐺 : 𝑆 ⟶ ℂ )
78 4 77 syl ⊢ ( 𝜑 → 𝐺 : 𝑆 ⟶ ℂ )
79 ulmscl ⊢ ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝑆 ∈ V )
80 4 79 syl ⊢ ( 𝜑 → 𝑆 ∈ V )
81 1 66 74 75 76 78 80 ulm2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ↔ ∀ 𝑟 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 ) )
82 74 fvmptelcdm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐴 ∈ ( ℂ ↑m 𝑆 ) )
83 elmapi ⊢ ( 𝐴 ∈ ( ℂ ↑m 𝑆 ) → 𝐴 : 𝑆 ⟶ ℂ )
84 82 83 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐴 : 𝑆 ⟶ ℂ )
85 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝑇 ⊆ 𝑆 )
86 84 85 fssresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → ( 𝐴 ↾ 𝑇 ) : 𝑇 ⟶ ℂ )
87 cnex ⊢ ℂ ∈ V
88 80 2 ssexd ⊢ ( 𝜑 → 𝑇 ∈ V )
89 88 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝑇 ∈ V )
90 elmapg ⊢ ( ( ℂ ∈ V ∧ 𝑇 ∈ V ) → ( ( 𝐴 ↾ 𝑇 ) ∈ ( ℂ ↑m 𝑇 ) ↔ ( 𝐴 ↾ 𝑇 ) : 𝑇 ⟶ ℂ ) )
91 87 89 90 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → ( ( 𝐴 ↾ 𝑇 ) ∈ ( ℂ ↑m 𝑇 ) ↔ ( 𝐴 ↾ 𝑇 ) : 𝑇 ⟶ ℂ ) )
92 86 91 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → ( 𝐴 ↾ 𝑇 ) ∈ ( ℂ ↑m 𝑇 ) )
93 92 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) : 𝑍 ⟶ ( ℂ ↑m 𝑇 ) )
94 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇 ) ) → ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) )
95 fvres ⊢ ( 𝑧 ∈ 𝑇 → ( ( 𝐺 ↾ 𝑇 ) ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
96 95 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑇 ) → ( ( 𝐺 ↾ 𝑇 ) ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
97 78 2 fssresd ⊢ ( 𝜑 → ( 𝐺 ↾ 𝑇 ) : 𝑇 ⟶ ℂ )
98 1 66 93 94 96 97 88 ulm2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ( ⇝𝑢 ‘ 𝑇 ) ( 𝐺 ↾ 𝑇 ) ↔ ∀ 𝑟 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑇 ( abs ‘ ( ( ( ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑟 ) )
99 52 81 98 3imtr4d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ( ⇝𝑢 ‘ 𝑇 ) ( 𝐺 ↾ 𝑇 ) ) )
100 4 99 mpd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 ↾ 𝑇 ) ) ( ⇝𝑢 ‘ 𝑇 ) ( 𝐺 ↾ 𝑇 ) )