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

Metamath Proof Explorer

Theorem limcmo

Description: If B is a limit point of the domain of the function F , then there is at most one limit value of F at B . (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses limcflf.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
limcflf.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
limcflf.b ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ 𝐾 ) ‘ 𝐴 ) )
limcflf.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
Assertion limcmo ( 𝜑 → ∃* 𝑥 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 limcflf.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
2 limcflf.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
3 limcflf.b ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ 𝐾 ) ‘ 𝐴 ) )
4 limcflf.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
5 4 cnfldhaus ⊢ 𝐾 ∈ Haus
6 eqid ⊢ ( 𝐴 ∖ { 𝐵 } ) = ( 𝐴 ∖ { 𝐵 } )
7 eqid ⊢ ( ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↾t ( 𝐴 ∖ { 𝐵 } ) ) = ( ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↾t ( 𝐴 ∖ { 𝐵 } ) )
8 1 2 3 4 6 7 limcflflem ⊢ ( 𝜑 → ( ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↾t ( 𝐴 ∖ { 𝐵 } ) ) ∈ ( Fil ‘ ( 𝐴 ∖ { 𝐵 } ) ) )
9 difss ⊢ ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴
10 fssres ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴 ) → ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) : ( 𝐴 ∖ { 𝐵 } ) ⟶ ℂ )
11 1 9 10 sylancl ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) : ( 𝐴 ∖ { 𝐵 } ) ⟶ ℂ )
12 4 cnfldtopon ⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
13 12 toponunii ⊢ ℂ = ∪ 𝐾
14 13 hausflf ⊢ ( ( 𝐾 ∈ Haus ∧ ( ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↾t ( 𝐴 ∖ { 𝐵 } ) ) ∈ ( Fil ‘ ( 𝐴 ∖ { 𝐵 } ) ) ∧ ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) : ( 𝐴 ∖ { 𝐵 } ) ⟶ ℂ ) → ∃* 𝑥 𝑥 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↾t ( 𝐴 ∖ { 𝐵 } ) ) ) ‘ ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) ) )
15 5 8 11 14 mp3an2i ⊢ ( 𝜑 → ∃* 𝑥 𝑥 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↾t ( 𝐴 ∖ { 𝐵 } ) ) ) ‘ ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) ) )
16 1 2 3 4 6 7 limcflf ⊢ ( 𝜑 → ( 𝐹 limℂ 𝐵 ) = ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↾t ( 𝐴 ∖ { 𝐵 } ) ) ) ‘ ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) ) )
17 16 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ↔ 𝑥 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↾t ( 𝐴 ∖ { 𝐵 } ) ) ) ‘ ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) ) ) )
18 17 mobidv ⊢ ( 𝜑 → ( ∃* 𝑥 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ↔ ∃* 𝑥 𝑥 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↾t ( 𝐴 ∖ { 𝐵 } ) ) ) ‘ ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) ) ) )
19 15 18 mpbird ⊢ ( 𝜑 → ∃* 𝑥 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) )