Metamath Proof Explorer


Theorem ulmcl

Description: Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015)

Ref Expression
Assertion ulmcl ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐺 : 𝑆 ⟶ ℂ )

Proof

Step Hyp Ref Expression
1 ulmscl ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝑆 ∈ V )
2 ulmval ( 𝑆 ∈ V → ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺 ↔ ∃ 𝑛 ∈ ℤ ( 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ) ) )
3 1 2 syl ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺 → ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺 ↔ ∃ 𝑛 ∈ ℤ ( 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ) ) )
4 3 ibi ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺 → ∃ 𝑛 ∈ ℤ ( 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ) )
5 simp2 ( ( 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ) → 𝐺 : 𝑆 ⟶ ℂ )
6 5 rexlimivw ( ∃ 𝑛 ∈ ℤ ( 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ) → 𝐺 : 𝑆 ⟶ ℂ )
7 4 6 syl ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐺 : 𝑆 ⟶ ℂ )