Metamath Proof Explorer

Theorem limcdif

Description: It suffices to consider functions which are not defined at B to define the limit of a function. In particular, the value of the original function F at B does not affect the limit of F . (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypothesis limccl.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
Assertion limcdif ( 𝜑 → ( 𝐹 limℂ 𝐵 ) = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 limccl.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
2 1 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
3 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ) → dom 𝐹 = 𝐴 )
4 limcrcl ⊢ ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) )
5 4 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ) → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) )
6 5 simp2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ) → dom 𝐹 ⊆ ℂ )
7 3 6 eqsstrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ) → 𝐴 ⊆ ℂ )
8 5 simp3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ) → 𝐵 ∈ ℂ )
9 7 8 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ) → ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) )
10 9 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) → ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ) )
11 undif1 ⊢ ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) = ( 𝐴 ∪ { 𝐵 } )
12 difss ⊢ ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴
13 fssres ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴 ) → ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) : ( 𝐴 ∖ { 𝐵 } ) ⟶ ℂ )
14 1 12 13 sylancl ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) : ( 𝐴 ∖ { 𝐵 } ) ⟶ ℂ )
15 14 fdmd ⊢ ( 𝜑 → dom ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) = ( 𝐴 ∖ { 𝐵 } ) )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) ) → dom ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) = ( 𝐴 ∖ { 𝐵 } ) )
17 limcrcl ⊢ ( 𝑥 ∈ ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) → ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) : dom ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) ⟶ ℂ ∧ dom ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) ⊆ ℂ ∧ 𝐵 ∈ ℂ ) )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) ) → ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) : dom ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) ⟶ ℂ ∧ dom ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) ⊆ ℂ ∧ 𝐵 ∈ ℂ ) )
19 18 simp2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) ) → dom ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) ⊆ ℂ )
20 16 19 eqsstrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) ) → ( 𝐴 ∖ { 𝐵 } ) ⊆ ℂ )
21 18 simp3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) ) → 𝐵 ∈ ℂ )
22 21 snssd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) ) → { 𝐵 } ⊆ ℂ )
23 20 22 unssd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) ) → ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) ⊆ ℂ )
24 11 23 eqsstrrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) ) → ( 𝐴 ∪ { 𝐵 } ) ⊆ ℂ )
25 24 unssad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) ) → 𝐴 ⊆ ℂ )
26 25 21 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) ) → ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) )
27 26 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) → ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ) )
28 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∪ { 𝐵 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∪ { 𝐵 } ) )
29 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
30 eqid ⊢ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) )
31 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ) → 𝐹 : 𝐴 ⟶ ℂ )
32 simprl ⊢ ( ( 𝜑 ∧ ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ) → 𝐴 ⊆ ℂ )
33 simprr ⊢ ( ( 𝜑 ∧ ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ) → 𝐵 ∈ ℂ )
34 28 29 30 31 32 33 ellimc ⊢ ( ( 𝜑 ∧ ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ) → ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ↔ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐵 ) ) )
35 11 eqcomi ⊢ ( 𝐴 ∪ { 𝐵 } ) = ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } )
36 35 oveq2i ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∪ { 𝐵 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) )
37 35 mpteq1i ⊢ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) )
38 elun ⊢ ( 𝑧 ∈ ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) ↔ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∨ 𝑧 ∈ { 𝐵 } ) )
39 velsn ⊢ ( 𝑧 ∈ { 𝐵 } ↔ 𝑧 = 𝐵 )
40 39 orbi2i ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∨ 𝑧 ∈ { 𝐵 } ) ↔ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∨ 𝑧 = 𝐵 ) )
41 pm5.61 ⊢ ( ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∨ 𝑧 = 𝐵 ) ∧ ¬ 𝑧 = 𝐵 ) ↔ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ ¬ 𝑧 = 𝐵 ) )
42 fvres ⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) → ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
43 42 adantr ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ ¬ 𝑧 = 𝐵 ) → ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
44 41 43 sylbi ⊢ ( ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∨ 𝑧 = 𝐵 ) ∧ ¬ 𝑧 = 𝐵 ) → ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
45 44 ifeq2da ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∨ 𝑧 = 𝐵 ) → if ( 𝑧 = 𝐵 , 𝑥 , ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) ‘ 𝑧 ) ) = if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) )
46 40 45 sylbi ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∨ 𝑧 ∈ { 𝐵 } ) → if ( 𝑧 = 𝐵 , 𝑥 , ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) ‘ 𝑧 ) ) = if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) )
47 38 46 sylbi ⊢ ( 𝑧 ∈ ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) → if ( 𝑧 = 𝐵 , 𝑥 , ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) ‘ 𝑧 ) ) = if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) )
48 47 mpteq2ia ⊢ ( 𝑧 ∈ ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) )
49 37 48 eqtr4i ⊢ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) ‘ 𝑧 ) ) )
50 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ) → ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) : ( 𝐴 ∖ { 𝐵 } ) ⟶ ℂ )
51 32 ssdifssd ⊢ ( ( 𝜑 ∧ ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ) → ( 𝐴 ∖ { 𝐵 } ) ⊆ ℂ )
52 36 29 49 50 51 33 ellimc ⊢ ( ( 𝜑 ∧ ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ) → ( 𝑥 ∈ ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) ↔ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐵 ) ) )
53 34 52 bitr4d ⊢ ( ( 𝜑 ∧ ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ) → ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ↔ 𝑥 ∈ ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) ) )
54 53 ex ⊢ ( 𝜑 → ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ↔ 𝑥 ∈ ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) ) ) )
55 10 27 54 pm5.21ndd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ↔ 𝑥 ∈ ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) ) )
56 55 eqrdv ⊢ ( 𝜑 → ( 𝐹 limℂ 𝐵 ) = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) )