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