Metamath Proof Explorer

Theorem ulmval

Description: Express the predicate: The sequence of functions F converges uniformly to G on S . (Contributed by Mario Carneiro, 26-Feb-2015)

Ref Expression
Assertion ulmval ( 𝑆 ∈ 𝑉 → ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ↔ ∃ 𝑛 ∈ ℤ ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 ulmrel ⊢ Rel ( ⇝𝑢 ‘ 𝑆 )
2 1 brrelex12i ⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
3 2 a1i ⊢ ( 𝑆 ∈ 𝑉 → ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ) )
4 3simpa ⊢ ( ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) → ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ) )
5 fvex ⊢ ( ℤ≥ ‘ 𝑛 ) ∈ V
6 fex ⊢ ( ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ ( ℤ≥ ‘ 𝑛 ) ∈ V ) → 𝐹 ∈ V )
7 5 6 mpan2 ⊢ ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) → 𝐹 ∈ V )
8 7 a1i ⊢ ( 𝑆 ∈ 𝑉 → ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) → 𝐹 ∈ V ) )
9 fex ⊢ ( ( 𝐺 : 𝑆 ⟶ ℂ ∧ 𝑆 ∈ 𝑉 ) → 𝐺 ∈ V )
10 9 expcom ⊢ ( 𝑆 ∈ 𝑉 → ( 𝐺 : 𝑆 ⟶ ℂ → 𝐺 ∈ V ) )
11 8 10 anim12d ⊢ ( 𝑆 ∈ 𝑉 → ( ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ) → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ) )
12 4 11 syl5 ⊢ ( 𝑆 ∈ 𝑉 → ( ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ) )
13 12 rexlimdvw ⊢ ( 𝑆 ∈ 𝑉 → ( ∃ 𝑛 ∈ ℤ ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ) )
14 df-ulm ⊢ ⇝𝑢 = ( 𝑠 ∈ V ↦ { ⟨ 𝑓 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑠 ) ∧ 𝑦 : 𝑠 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑠 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) } )
15 oveq2 ⊢ ( 𝑠 = 𝑆 → ( ℂ ↑m 𝑠 ) = ( ℂ ↑m 𝑆 ) )
16 15 feq3d ⊢ ( 𝑠 = 𝑆 → ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑠 ) ↔ 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) )
17 feq2 ⊢ ( 𝑠 = 𝑆 → ( 𝑦 : 𝑠 ⟶ ℂ ↔ 𝑦 : 𝑆 ⟶ ℂ ) )
18 raleq ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑧 ∈ 𝑠 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) )
19 18 rexralbidv ⊢ ( 𝑠 = 𝑆 → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑠 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) )
20 19 ralbidv ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑠 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) )
21 16 17 20 3anbi123d ⊢ ( 𝑠 = 𝑆 → ( ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑠 ) ∧ 𝑦 : 𝑠 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑠 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) ↔ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) ) )
22 21 rexbidv ⊢ ( 𝑠 = 𝑆 → ( ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑠 ) ∧ 𝑦 : 𝑠 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑠 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) ↔ ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) ) )
23 22 opabbidv ⊢ ( 𝑠 = 𝑆 → { ⟨ 𝑓 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑠 ) ∧ 𝑦 : 𝑠 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑠 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) } = { ⟨ 𝑓 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) } )
24 elex ⊢ ( 𝑆 ∈ 𝑉 → 𝑆 ∈ V )
25 simpr1 ⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) ) → 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) )
26 uzssz ⊢ ( ℤ≥ ‘ 𝑛 ) ⊆ ℤ
27 ovex ⊢ ( ℂ ↑m 𝑆 ) ∈ V
28 zex ⊢ ℤ ∈ V
29 elpm2r ⊢ ( ( ( ( ℂ ↑m 𝑆 ) ∈ V ∧ ℤ ∈ V ) ∧ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ ( ℤ≥ ‘ 𝑛 ) ⊆ ℤ ) ) → 𝑓 ∈ ( ( ℂ ↑m 𝑆 ) ↑pm ℤ ) )
30 27 28 29 mpanl12 ⊢ ( ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ ( ℤ≥ ‘ 𝑛 ) ⊆ ℤ ) → 𝑓 ∈ ( ( ℂ ↑m 𝑆 ) ↑pm ℤ ) )
31 25 26 30 sylancl ⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) ) → 𝑓 ∈ ( ( ℂ ↑m 𝑆 ) ↑pm ℤ ) )
32 simpr2 ⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) ) → 𝑦 : 𝑆 ⟶ ℂ )
33 cnex ⊢ ℂ ∈ V
34 simpl ⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) ) → 𝑆 ∈ 𝑉 )
35 elmapg ⊢ ( ( ℂ ∈ V ∧ 𝑆 ∈ 𝑉 ) → ( 𝑦 ∈ ( ℂ ↑m 𝑆 ) ↔ 𝑦 : 𝑆 ⟶ ℂ ) )
36 33 34 35 sylancr ⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) ) → ( 𝑦 ∈ ( ℂ ↑m 𝑆 ) ↔ 𝑦 : 𝑆 ⟶ ℂ ) )
37 32 36 mpbird ⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) ) → 𝑦 ∈ ( ℂ ↑m 𝑆 ) )
38 31 37 jca ⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) ) → ( 𝑓 ∈ ( ( ℂ ↑m 𝑆 ) ↑pm ℤ ) ∧ 𝑦 ∈ ( ℂ ↑m 𝑆 ) ) )
39 38 ex ⊢ ( 𝑆 ∈ 𝑉 → ( ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) → ( 𝑓 ∈ ( ( ℂ ↑m 𝑆 ) ↑pm ℤ ) ∧ 𝑦 ∈ ( ℂ ↑m 𝑆 ) ) ) )
40 39 rexlimdvw ⊢ ( 𝑆 ∈ 𝑉 → ( ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) → ( 𝑓 ∈ ( ( ℂ ↑m 𝑆 ) ↑pm ℤ ) ∧ 𝑦 ∈ ( ℂ ↑m 𝑆 ) ) ) )
41 40 ssopab2dv ⊢ ( 𝑆 ∈ 𝑉 → { ⟨ 𝑓 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) } ⊆ { ⟨ 𝑓 , 𝑦 ⟩ ∣ ( 𝑓 ∈ ( ( ℂ ↑m 𝑆 ) ↑pm ℤ ) ∧ 𝑦 ∈ ( ℂ ↑m 𝑆 ) ) } )
42 df-xp ⊢ ( ( ( ℂ ↑m 𝑆 ) ↑pm ℤ ) × ( ℂ ↑m 𝑆 ) ) = { ⟨ 𝑓 , 𝑦 ⟩ ∣ ( 𝑓 ∈ ( ( ℂ ↑m 𝑆 ) ↑pm ℤ ) ∧ 𝑦 ∈ ( ℂ ↑m 𝑆 ) ) }
43 41 42 sseqtrrdi ⊢ ( 𝑆 ∈ 𝑉 → { ⟨ 𝑓 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) } ⊆ ( ( ( ℂ ↑m 𝑆 ) ↑pm ℤ ) × ( ℂ ↑m 𝑆 ) ) )
44 ovex ⊢ ( ( ℂ ↑m 𝑆 ) ↑pm ℤ ) ∈ V
45 44 27 xpex ⊢ ( ( ( ℂ ↑m 𝑆 ) ↑pm ℤ ) × ( ℂ ↑m 𝑆 ) ) ∈ V
46 45 ssex ⊢ ( { ⟨ 𝑓 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) } ⊆ ( ( ( ℂ ↑m 𝑆 ) ↑pm ℤ ) × ( ℂ ↑m 𝑆 ) ) → { ⟨ 𝑓 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) } ∈ V )
47 43 46 syl ⊢ ( 𝑆 ∈ 𝑉 → { ⟨ 𝑓 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) } ∈ V )
48 14 23 24 47 fvmptd3 ⊢ ( 𝑆 ∈ 𝑉 → ( ⇝𝑢 ‘ 𝑆 ) = { ⟨ 𝑓 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) } )
49 48 breqd ⊢ ( 𝑆 ∈ 𝑉 → ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ↔ 𝐹 { ⟨ 𝑓 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) } 𝐺 ) )
50 simpl ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐺 ) → 𝑓 = 𝐹 )
51 50 feq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ↔ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) )
52 simpr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐺 ) → 𝑦 = 𝐺 )
53 52 feq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( 𝑦 : 𝑆 ⟶ ℂ ↔ 𝐺 : 𝑆 ⟶ ℂ ) )
54 50 fveq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( 𝑓 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
55 54 fveq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) )
56 52 fveq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( 𝑦 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
57 55 56 oveq12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) )
58 57 fveq2d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) )
59 58 breq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) )
60 59 ralbidv ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) )
61 60 rexralbidv ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) )
62 61 ralbidv ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) )
63 51 53 62 3anbi123d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) ↔ ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) ) )
64 63 rexbidv ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐺 ) → ( ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) ↔ ∃ 𝑛 ∈ ℤ ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) ) )
65 eqid ⊢ { ⟨ 𝑓 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) } = { ⟨ 𝑓 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) }
66 64 65 brabga ⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 𝐹 { ⟨ 𝑓 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑦 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) } 𝐺 ↔ ∃ 𝑛 ∈ ℤ ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) ) )
67 49 66 sylan9bb ⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ) → ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ↔ ∃ 𝑛 ∈ ℤ ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) ) )
68 67 ex ⊢ ( 𝑆 ∈ 𝑉 → ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ↔ ∃ 𝑛 ∈ ℤ ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) ) ) )
69 3 13 68 pm5.21ndd ⊢ ( 𝑆 ∈ 𝑉 → ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ↔ ∃ 𝑛 ∈ ℤ ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) ) )