Theorem ulmf

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

	Ref	Expression
Assertion	ulmf	⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → ∃ 𝑛 ∈ ℤ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) )

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		simp1	⊢ ( ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) → 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) )
6	5	reximi	⊢ ( ∃ 𝑛 ∈ ℤ ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) → ∃ 𝑛 ∈ ℤ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) )
7	4 6	syl	⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → ∃ 𝑛 ∈ ℤ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) )