This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ulmpm

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

Ref Expression
Assertion ulmpm ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝐹 ∈ ( ( ℂ ↑m 𝑆 ) ↑pm ℤ ) )

Proof

Step Hyp Ref Expression
1 ulmf ⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → ∃ 𝑛 ∈ ℤ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) )
2 uzssz ⊢ ( ℤ≥ ‘ 𝑛 ) ⊆ ℤ
3 ovex ⊢ ( ℂ ↑m 𝑆 ) ∈ V
4 zex ⊢ ℤ ∈ V
5 elpm2r ⊢ ( ( ( ( ℂ ↑m 𝑆 ) ∈ V ∧ ℤ ∈ V ) ∧ ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ ( ℤ≥ ‘ 𝑛 ) ⊆ ℤ ) ) → 𝐹 ∈ ( ( ℂ ↑m 𝑆 ) ↑pm ℤ ) )
6 3 4 5 mpanl12 ⊢ ( ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ ( ℤ≥ ‘ 𝑛 ) ⊆ ℤ ) → 𝐹 ∈ ( ( ℂ ↑m 𝑆 ) ↑pm ℤ ) )
7 2 6 mpan2 ⊢ ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) → 𝐹 ∈ ( ( ℂ ↑m 𝑆 ) ↑pm ℤ ) )
8 7 rexlimivw ⊢ ( ∃ 𝑛 ∈ ℤ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) → 𝐹 ∈ ( ( ℂ ↑m 𝑆 ) ↑pm ℤ ) )
9 1 8 syl ⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝐹 ∈ ( ( ℂ ↑m 𝑆 ) ↑pm ℤ ) )