Metamath Proof Explorer


Theorem ulmf2

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

Ref Expression
Assertion ulmf2 ( ( 𝐹 Fn 𝑍𝐹 ( ⇝𝑢𝑆 ) 𝐺 ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )

Proof

Step Hyp Ref Expression
1 ulmpm ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐹 ∈ ( ( ℂ ↑m 𝑆 ) ↑pm ℤ ) )
2 ovex ( ℂ ↑m 𝑆 ) ∈ V
3 zex ℤ ∈ V
4 2 3 elpm2 ( 𝐹 ∈ ( ( ℂ ↑m 𝑆 ) ↑pm ℤ ) ↔ ( 𝐹 : dom 𝐹 ⟶ ( ℂ ↑m 𝑆 ) ∧ dom 𝐹 ⊆ ℤ ) )
5 4 simplbi ( 𝐹 ∈ ( ( ℂ ↑m 𝑆 ) ↑pm ℤ ) → 𝐹 : dom 𝐹 ⟶ ( ℂ ↑m 𝑆 ) )
6 1 5 syl ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐹 : dom 𝐹 ⟶ ( ℂ ↑m 𝑆 ) )
7 6 adantl ( ( 𝐹 Fn 𝑍𝐹 ( ⇝𝑢𝑆 ) 𝐺 ) → 𝐹 : dom 𝐹 ⟶ ( ℂ ↑m 𝑆 ) )
8 fndm ( 𝐹 Fn 𝑍 → dom 𝐹 = 𝑍 )
9 8 adantr ( ( 𝐹 Fn 𝑍𝐹 ( ⇝𝑢𝑆 ) 𝐺 ) → dom 𝐹 = 𝑍 )
10 9 feq2d ( ( 𝐹 Fn 𝑍𝐹 ( ⇝𝑢𝑆 ) 𝐺 ) → ( 𝐹 : dom 𝐹 ⟶ ( ℂ ↑m 𝑆 ) ↔ 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) ) )
11 7 10 mpbid ( ( 𝐹 Fn 𝑍𝐹 ( ⇝𝑢𝑆 ) 𝐺 ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )