ulmf2

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

		Ref	Expression
	Assertion	ulmf2	⊢ ( ( 𝐹 Fn 𝑍 ∧ 𝐹 ( ⇝_𝑢 ‘ 𝑆 ) 𝐺 ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑_m 𝑆 ) )

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

Metamath Proof Explorer