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ℂ 𝐵 ) )