Theorem ulmuni

Description: A sequence of functions uniformly converges to at most one limit. (Contributed by Mario Carneiro, 5-Jul-2017)

	Ref	Expression
Assertion	ulmuni	⊢ ( ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐻 ) → 𝐺 = 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		ulmcl	⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝐺 : 𝑆 ⟶ ℂ )
2	1	adantr	⊢ ( ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐻 ) → 𝐺 : 𝑆 ⟶ ℂ )
3	2	ffnd	⊢ ( ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐻 ) → 𝐺 Fn 𝑆 )
4		ulmcl	⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐻 → 𝐻 : 𝑆 ⟶ ℂ )
5	4	adantl	⊢ ( ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐻 ) → 𝐻 : 𝑆 ⟶ ℂ )
6	5	ffnd	⊢ ( ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐻 ) → 𝐻 Fn 𝑆 )
7		eqid	⊢ ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑛 )
8		simplr	⊢ ( ( ( ( ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐻 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑛 ∈ ℤ ) ∧ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → 𝑛 ∈ ℤ )
9		simpr	⊢ ( ( ( ( ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐻 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑛 ∈ ℤ ) ∧ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) )
10		simpllr	⊢ ( ( ( ( ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐻 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑛 ∈ ℤ ) ∧ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → 𝑥 ∈ 𝑆 )
11		fvex	⊢ ( ℤ≥ ‘ 𝑛 ) ∈ V
12	11	mptex	⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ∈ V
13	12	a1i	⊢ ( ( ( ( ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐻 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑛 ∈ ℤ ) ∧ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → ( 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ∈ V )
14		fveq2	⊢ ( 𝑖 = 𝑘 → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑘 ) )
15	14	fveq1d	⊢ ( 𝑖 = 𝑘 → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) )
16		eqid	⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) = ( 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) )
17		fvex	⊢ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ∈ V
18	15 16 17	fvmpt	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) → ( ( 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) )
19	18	eqcomd	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ‘ 𝑘 ) )
20	19	adantl	⊢ ( ( ( ( ( ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐻 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑛 ∈ ℤ ) ∧ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ‘ 𝑘 ) )
21		simp-4l	⊢ ( ( ( ( ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐻 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑛 ∈ ℤ ) ∧ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
22	7 8 9 10 13 20 21	ulmclm	⊢ ( ( ( ( ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐻 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑛 ∈ ℤ ) ∧ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → ( 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) )
23		simp-4r	⊢ ( ( ( ( ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐻 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑛 ∈ ℤ ) ∧ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐻 )
24	7 8 9 10 13 20 23	ulmclm	⊢ ( ( ( ( ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐻 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑛 ∈ ℤ ) ∧ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → ( 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ⇝ ( 𝐻 ‘ 𝑥 ) )
25		climuni	⊢ ( ( ( 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) ∧ ( 𝑖 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ) ⇝ ( 𝐻 ‘ 𝑥 ) ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) )
26	22 24 25	syl2anc	⊢ ( ( ( ( ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐻 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑛 ∈ ℤ ) ∧ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) )
27		ulmf	⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → ∃ 𝑛 ∈ ℤ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) )
28	27	ad2antrr	⊢ ( ( ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐻 ) ∧ 𝑥 ∈ 𝑆 ) → ∃ 𝑛 ∈ ℤ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) )
29	26 28	r19.29a	⊢ ( ( ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐻 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) )
30	3 6 29	eqfnfvd	⊢ ( ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐻 ) → 𝐺 = 𝐻 )