Theorem hlimuni

Description: A Hilbert space sequence converges to at most one limit. (Contributed by NM, 19-Aug-1999) (Revised by Mario Carneiro, 2-May-2015) (New usage is discouraged.)

	Ref	Expression
Assertion	hlimuni	⊢ ( ( 𝐹 ⇝𝑣 𝐴 ∧ 𝐹 ⇝𝑣 𝐵 ) → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		hlimf	⊢ ⇝𝑣 : dom ⇝𝑣 ⟶ ℋ
2		ffun	⊢ ( ⇝𝑣 : dom ⇝𝑣 ⟶ ℋ → Fun ⇝𝑣 )
3		funbrfv	⊢ ( Fun ⇝𝑣 → ( 𝐹 ⇝𝑣 𝐴 → ( ⇝𝑣 ‘ 𝐹 ) = 𝐴 ) )
4	1 2 3	mp2b	⊢ ( 𝐹 ⇝𝑣 𝐴 → ( ⇝𝑣 ‘ 𝐹 ) = 𝐴 )
5		funbrfv	⊢ ( Fun ⇝𝑣 → ( 𝐹 ⇝𝑣 𝐵 → ( ⇝𝑣 ‘ 𝐹 ) = 𝐵 ) )
6	1 2 5	mp2b	⊢ ( 𝐹 ⇝𝑣 𝐵 → ( ⇝𝑣 ‘ 𝐹 ) = 𝐵 )
7	4 6	sylan9req	⊢ ( ( 𝐹 ⇝𝑣 𝐴 ∧ 𝐹 ⇝𝑣 𝐵 ) → 𝐴 = 𝐵 )