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

Metamath Proof Explorer

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 ⊢ ( ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐻 ) → 𝐺 = 𝐻 )