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	⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝐺 : 𝑆 ⟶ ℂ )