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 ℤ ) )