Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ulmss Structured version   Visualization version   GIF version

Theorem ulmss 24971
 Description: A uniform limit of functions is still a uniform limit if restricted to a subset. (Contributed by Mario Carneiro, 3-Mar-2015.)
Hypotheses
Ref Expression
ulmss.z 𝑍 = (ℤ𝑀)
ulmss.t (𝜑𝑇𝑆)
ulmss.a ((𝜑𝑥𝑍) → 𝐴𝑊)
ulmss.u (𝜑 → (𝑥𝑍𝐴)(⇝𝑢𝑆)𝐺)
Assertion
Ref Expression
ulmss (𝜑 → (𝑥𝑍 ↦ (𝐴𝑇))(⇝𝑢𝑇)(𝐺𝑇))
Distinct variable groups:   𝑥,𝑇   𝜑,𝑥   𝑥,𝑆   𝑥,𝑍
Allowed substitution hints:   𝐴(𝑥)   𝐺(𝑥)   𝑀(𝑥)   𝑊(𝑥)

Proof of Theorem ulmss
Dummy variables 𝑗 𝑘 𝑚 𝑟 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ulmss.u . 2 (𝜑 → (𝑥𝑍𝐴)(⇝𝑢𝑆)𝐺)
2 ulmss.z . . . . . . . . 9 𝑍 = (ℤ𝑀)
32uztrn2 12240 . . . . . . . 8 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
4 ulmss.t . . . . . . . . . . 11 (𝜑𝑇𝑆)
54adantr 484 . . . . . . . . . 10 ((𝜑𝑘𝑍) → 𝑇𝑆)
6 ssralv 4009 . . . . . . . . . 10 (𝑇𝑆 → (∀𝑧𝑆 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 → ∀𝑧𝑇 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
75, 6syl 17 . . . . . . . . 9 ((𝜑𝑘𝑍) → (∀𝑧𝑆 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 → ∀𝑧𝑇 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
8 fvres 6662 . . . . . . . . . . . . . . 15 (𝑧𝑇 → ((𝐴𝑇)‘𝑧) = (𝐴𝑧))
98ad2antll 728 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥𝑍𝑧𝑇)) → ((𝐴𝑇)‘𝑧) = (𝐴𝑧))
10 simprl 770 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥𝑍𝑧𝑇)) → 𝑥𝑍)
11 ulmss.a . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝑍) → 𝐴𝑊)
1211adantrr 716 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑥𝑍𝑧𝑇)) → 𝐴𝑊)
13 resexg 5871 . . . . . . . . . . . . . . . . 17 (𝐴𝑊 → (𝐴𝑇) ∈ V)
1412, 13syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥𝑍𝑧𝑇)) → (𝐴𝑇) ∈ V)
15 eqid 2821 . . . . . . . . . . . . . . . . 17 (𝑥𝑍 ↦ (𝐴𝑇)) = (𝑥𝑍 ↦ (𝐴𝑇))
1615fvmpt2 6752 . . . . . . . . . . . . . . . 16 ((𝑥𝑍 ∧ (𝐴𝑇) ∈ V) → ((𝑥𝑍 ↦ (𝐴𝑇))‘𝑥) = (𝐴𝑇))
1710, 14, 16syl2anc 587 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝑍𝑧𝑇)) → ((𝑥𝑍 ↦ (𝐴𝑇))‘𝑥) = (𝐴𝑇))
1817fveq1d 6645 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥𝑍𝑧𝑇)) → (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑥)‘𝑧) = ((𝐴𝑇)‘𝑧))
19 eqid 2821 . . . . . . . . . . . . . . . . 17 (𝑥𝑍𝐴) = (𝑥𝑍𝐴)
2019fvmpt2 6752 . . . . . . . . . . . . . . . 16 ((𝑥𝑍𝐴𝑊) → ((𝑥𝑍𝐴)‘𝑥) = 𝐴)
2110, 12, 20syl2anc 587 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝑍𝑧𝑇)) → ((𝑥𝑍𝐴)‘𝑥) = 𝐴)
2221fveq1d 6645 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥𝑍𝑧𝑇)) → (((𝑥𝑍𝐴)‘𝑥)‘𝑧) = (𝐴𝑧))
239, 18, 223eqtr4d 2866 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑍𝑧𝑇)) → (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑥)‘𝑧) = (((𝑥𝑍𝐴)‘𝑥)‘𝑧))
2423ralrimivva 3179 . . . . . . . . . . . 12 (𝜑 → ∀𝑥𝑍𝑧𝑇 (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑥)‘𝑧) = (((𝑥𝑍𝐴)‘𝑥)‘𝑧))
25 nfv 1916 . . . . . . . . . . . . 13 𝑘𝑧𝑇 (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑥)‘𝑧) = (((𝑥𝑍𝐴)‘𝑥)‘𝑧)
26 nfcv 2974 . . . . . . . . . . . . . 14 𝑥𝑇
27 nffvmpt1 6654 . . . . . . . . . . . . . . . 16 𝑥((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)
28 nfcv 2974 . . . . . . . . . . . . . . . 16 𝑥𝑧
2927, 28nffv 6653 . . . . . . . . . . . . . . 15 𝑥(((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧)
30 nffvmpt1 6654 . . . . . . . . . . . . . . . 16 𝑥((𝑥𝑍𝐴)‘𝑘)
3130, 28nffv 6653 . . . . . . . . . . . . . . 15 𝑥(((𝑥𝑍𝐴)‘𝑘)‘𝑧)
3229, 31nfeq 2987 . . . . . . . . . . . . . 14 𝑥(((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧)
3326, 32nfralw 3213 . . . . . . . . . . . . 13 𝑥𝑧𝑇 (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧)
34 fveq2 6643 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑘 → ((𝑥𝑍 ↦ (𝐴𝑇))‘𝑥) = ((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘))
3534fveq1d 6645 . . . . . . . . . . . . . . 15 (𝑥 = 𝑘 → (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑥)‘𝑧) = (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧))
36 fveq2 6643 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑘 → ((𝑥𝑍𝐴)‘𝑥) = ((𝑥𝑍𝐴)‘𝑘))
3736fveq1d 6645 . . . . . . . . . . . . . . 15 (𝑥 = 𝑘 → (((𝑥𝑍𝐴)‘𝑥)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧))
3835, 37eqeq12d 2837 . . . . . . . . . . . . . 14 (𝑥 = 𝑘 → ((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑥)‘𝑧) = (((𝑥𝑍𝐴)‘𝑥)‘𝑧) ↔ (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧)))
3938ralbidv 3185 . . . . . . . . . . . . 13 (𝑥 = 𝑘 → (∀𝑧𝑇 (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑥)‘𝑧) = (((𝑥𝑍𝐴)‘𝑥)‘𝑧) ↔ ∀𝑧𝑇 (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧)))
4025, 33, 39cbvralw 3418 . . . . . . . . . . . 12 (∀𝑥𝑍𝑧𝑇 (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑥)‘𝑧) = (((𝑥𝑍𝐴)‘𝑥)‘𝑧) ↔ ∀𝑘𝑍𝑧𝑇 (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧))
4124, 40sylib 221 . . . . . . . . . . 11 (𝜑 → ∀𝑘𝑍𝑧𝑇 (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧))
4241r19.21bi 3196 . . . . . . . . . 10 ((𝜑𝑘𝑍) → ∀𝑧𝑇 (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧))
43 fvoveq1 7153 . . . . . . . . . . . 12 ((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧) → (abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) = (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))))
4443breq1d 5049 . . . . . . . . . . 11 ((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧) → ((abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 ↔ (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
4544ralimi 3148 . . . . . . . . . 10 (∀𝑧𝑇 (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧) → ∀𝑧𝑇 ((abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 ↔ (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
46 ralbi 3155 . . . . . . . . . 10 (∀𝑧𝑇 ((abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 ↔ (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟) → (∀𝑧𝑇 (abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 ↔ ∀𝑧𝑇 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
4742, 45, 463syl 18 . . . . . . . . 9 ((𝜑𝑘𝑍) → (∀𝑧𝑇 (abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 ↔ ∀𝑧𝑇 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
487, 47sylibrd 262 . . . . . . . 8 ((𝜑𝑘𝑍) → (∀𝑧𝑆 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 → ∀𝑧𝑇 (abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
493, 48sylan2 595 . . . . . . 7 ((𝜑 ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → (∀𝑧𝑆 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 → ∀𝑧𝑇 (abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
5049anassrs 471 . . . . . 6 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (∀𝑧𝑆 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 → ∀𝑧𝑇 (abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
5150ralimdva 3165 . . . . 5 ((𝜑𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 → ∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑇 (abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
5251reximdva 3260 . . . 4 (𝜑 → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑇 (abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
5352ralimdv 3166 . . 3 (𝜑 → (∀𝑟 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 → ∀𝑟 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑇 (abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
54 ulmf 24956 . . . . . 6 ((𝑥𝑍𝐴)(⇝𝑢𝑆)𝐺 → ∃𝑚 ∈ ℤ (𝑥𝑍𝐴):(ℤ𝑚)⟶(ℂ ↑m 𝑆))
551, 54syl 17 . . . . 5 (𝜑 → ∃𝑚 ∈ ℤ (𝑥𝑍𝐴):(ℤ𝑚)⟶(ℂ ↑m 𝑆))
56 fdm 6495 . . . . . . . 8 ((𝑥𝑍𝐴):(ℤ𝑚)⟶(ℂ ↑m 𝑆) → dom (𝑥𝑍𝐴) = (ℤ𝑚))
5719dmmptss 6068 . . . . . . . 8 dom (𝑥𝑍𝐴) ⊆ 𝑍
5856, 57eqsstrrdi 3998 . . . . . . 7 ((𝑥𝑍𝐴):(ℤ𝑚)⟶(ℂ ↑m 𝑆) → (ℤ𝑚) ⊆ 𝑍)
59 uzid 12236 . . . . . . . 8 (𝑚 ∈ ℤ → 𝑚 ∈ (ℤ𝑚))
6059adantl 485 . . . . . . 7 ((𝜑𝑚 ∈ ℤ) → 𝑚 ∈ (ℤ𝑚))
61 ssel 3937 . . . . . . . 8 ((ℤ𝑚) ⊆ 𝑍 → (𝑚 ∈ (ℤ𝑚) → 𝑚𝑍))
62 eluzel2 12226 . . . . . . . . 9 (𝑚 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
6362, 2eleq2s 2930 . . . . . . . 8 (𝑚𝑍𝑀 ∈ ℤ)
6461, 63syl6 35 . . . . . . 7 ((ℤ𝑚) ⊆ 𝑍 → (𝑚 ∈ (ℤ𝑚) → 𝑀 ∈ ℤ))
6558, 60, 64syl2imc 41 . . . . . 6 ((𝜑𝑚 ∈ ℤ) → ((𝑥𝑍𝐴):(ℤ𝑚)⟶(ℂ ↑m 𝑆) → 𝑀 ∈ ℤ))
6665rexlimdva 3270 . . . . 5 (𝜑 → (∃𝑚 ∈ ℤ (𝑥𝑍𝐴):(ℤ𝑚)⟶(ℂ ↑m 𝑆) → 𝑀 ∈ ℤ))
6755, 66mpd 15 . . . 4 (𝜑𝑀 ∈ ℤ)
6811ralrimiva 3170 . . . . . 6 (𝜑 → ∀𝑥𝑍 𝐴𝑊)
6919fnmpt 6461 . . . . . 6 (∀𝑥𝑍 𝐴𝑊 → (𝑥𝑍𝐴) Fn 𝑍)
7068, 69syl 17 . . . . 5 (𝜑 → (𝑥𝑍𝐴) Fn 𝑍)
71 frn 6493 . . . . . . 7 ((𝑥𝑍𝐴):(ℤ𝑚)⟶(ℂ ↑m 𝑆) → ran (𝑥𝑍𝐴) ⊆ (ℂ ↑m 𝑆))
7271rexlimivw 3268 . . . . . 6 (∃𝑚 ∈ ℤ (𝑥𝑍𝐴):(ℤ𝑚)⟶(ℂ ↑m 𝑆) → ran (𝑥𝑍𝐴) ⊆ (ℂ ↑m 𝑆))
7355, 72syl 17 . . . . 5 (𝜑 → ran (𝑥𝑍𝐴) ⊆ (ℂ ↑m 𝑆))
74 df-f 6332 . . . . 5 ((𝑥𝑍𝐴):𝑍⟶(ℂ ↑m 𝑆) ↔ ((𝑥𝑍𝐴) Fn 𝑍 ∧ ran (𝑥𝑍𝐴) ⊆ (ℂ ↑m 𝑆)))
7570, 73, 74sylanbrc 586 . . . 4 (𝜑 → (𝑥𝑍𝐴):𝑍⟶(ℂ ↑m 𝑆))
76 eqidd 2822 . . . 4 ((𝜑 ∧ (𝑘𝑍𝑧𝑆)) → (((𝑥𝑍𝐴)‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧))
77 eqidd 2822 . . . 4 ((𝜑𝑧𝑆) → (𝐺𝑧) = (𝐺𝑧))
78 ulmcl 24955 . . . . 5 ((𝑥𝑍𝐴)(⇝𝑢𝑆)𝐺𝐺:𝑆⟶ℂ)
791, 78syl 17 . . . 4 (𝜑𝐺:𝑆⟶ℂ)
80 ulmscl 24953 . . . . 5 ((𝑥𝑍𝐴)(⇝𝑢𝑆)𝐺𝑆 ∈ V)
811, 80syl 17 . . . 4 (𝜑𝑆 ∈ V)
822, 67, 75, 76, 77, 79, 81ulm2 24959 . . 3 (𝜑 → ((𝑥𝑍𝐴)(⇝𝑢𝑆)𝐺 ↔ ∀𝑟 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
8375fvmptelrn 6850 . . . . . . . 8 ((𝜑𝑥𝑍) → 𝐴 ∈ (ℂ ↑m 𝑆))
84 elmapi 8403 . . . . . . . 8 (𝐴 ∈ (ℂ ↑m 𝑆) → 𝐴:𝑆⟶ℂ)
8583, 84syl 17 . . . . . . 7 ((𝜑𝑥𝑍) → 𝐴:𝑆⟶ℂ)
864adantr 484 . . . . . . 7 ((𝜑𝑥𝑍) → 𝑇𝑆)
8785, 86fssresd 6518 . . . . . 6 ((𝜑𝑥𝑍) → (𝐴𝑇):𝑇⟶ℂ)
88 cnex 10595 . . . . . . 7 ℂ ∈ V
8981, 4ssexd 5201 . . . . . . . 8 (𝜑𝑇 ∈ V)
9089adantr 484 . . . . . . 7 ((𝜑𝑥𝑍) → 𝑇 ∈ V)
91 elmapg 8394 . . . . . . 7 ((ℂ ∈ V ∧ 𝑇 ∈ V) → ((𝐴𝑇) ∈ (ℂ ↑m 𝑇) ↔ (𝐴𝑇):𝑇⟶ℂ))
9288, 90, 91sylancr 590 . . . . . 6 ((𝜑𝑥𝑍) → ((𝐴𝑇) ∈ (ℂ ↑m 𝑇) ↔ (𝐴𝑇):𝑇⟶ℂ))
9387, 92mpbird 260 . . . . 5 ((𝜑𝑥𝑍) → (𝐴𝑇) ∈ (ℂ ↑m 𝑇))
9493fmpttd 6852 . . . 4 (𝜑 → (𝑥𝑍 ↦ (𝐴𝑇)):𝑍⟶(ℂ ↑m 𝑇))
95 eqidd 2822 . . . 4 ((𝜑 ∧ (𝑘𝑍𝑧𝑇)) → (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧))
96 fvres 6662 . . . . 5 (𝑧𝑇 → ((𝐺𝑇)‘𝑧) = (𝐺𝑧))
9796adantl 485 . . . 4 ((𝜑𝑧𝑇) → ((𝐺𝑇)‘𝑧) = (𝐺𝑧))
9879, 4fssresd 6518 . . . 4 (𝜑 → (𝐺𝑇):𝑇⟶ℂ)
992, 67, 94, 95, 97, 98, 89ulm2 24959 . . 3 (𝜑 → ((𝑥𝑍 ↦ (𝐴𝑇))(⇝𝑢𝑇)(𝐺𝑇) ↔ ∀𝑟 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑇 (abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
10053, 82, 993imtr4d 297 . 2 (𝜑 → ((𝑥𝑍𝐴)(⇝𝑢𝑆)𝐺 → (𝑥𝑍 ↦ (𝐴𝑇))(⇝𝑢𝑇)(𝐺𝑇)))
1011, 100mpd 15 1 (𝜑 → (𝑥𝑍 ↦ (𝐴𝑇))(⇝𝑢𝑇)(𝐺𝑇))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2115  ∀wral 3126  ∃wrex 3127  Vcvv 3471   ⊆ wss 3910   class class class wbr 5039   ↦ cmpt 5119  dom cdm 5528  ran crn 5529   ↾ cres 5530   Fn wfn 6323  ⟶wf 6324  ‘cfv 6328  (class class class)co 7130   ↑m cmap 8381  ℂcc 10512   < clt 10652   − cmin 10847  ℤcz 11959  ℤ≥cuz 12221  ℝ+crp 12367  abscabs 14572  ⇝𝑢culm 24950 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-rep 5163  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436  ax-cnex 10570  ax-resscn 10571  ax-pre-lttri 10588  ax-pre-lttrn 10589 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-nel 3112  df-ral 3131  df-rex 3132  df-reu 3133  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-iun 4894  df-br 5040  df-opab 5102  df-mpt 5120  df-id 5433  df-po 5447  df-so 5448  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7133  df-oprab 7134  df-mpo 7135  df-1st 7664  df-2nd 7665  df-er 8264  df-map 8383  df-pm 8384  df-en 8485  df-dom 8486  df-sdom 8487  df-pnf 10654  df-mnf 10655  df-xr 10656  df-ltxr 10657  df-le 10658  df-neg 10850  df-z 11960  df-uz 12222  df-ulm 24951 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator