Metamath Proof Explorer

Theorem limcres

Description: If B is an interior point of C u. { B } relative to the domain A , then a limit point of ` F |`C extends to a limit of F . (Contributed by Mario Carneiro, 27-Dec-2016)

Ref Expression
Hypotheses limcres.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
limcres.c ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
limcres.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
limcres.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
limcres.j ⊢ 𝐽 = ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) )
limcres.i ⊢ ( 𝜑 → 𝐵 ∈ ( ( int ‘ 𝐽 ) ‘ ( 𝐶 ∪ { 𝐵 } ) ) )
Assertion limcres ( 𝜑 → ( ( 𝐹 ↾ 𝐶 ) limℂ 𝐵 ) = ( 𝐹 limℂ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 limcres.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
2 limcres.c ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
3 limcres.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
4 limcres.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
5 limcres.j ⊢ 𝐽 = ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) )
6 limcres.i ⊢ ( 𝜑 → 𝐵 ∈ ( ( int ‘ 𝐽 ) ‘ ( 𝐶 ∪ { 𝐵 } ) ) )
7 limcrcl ⊢ ( 𝑥 ∈ ( ( 𝐹 ↾ 𝐶 ) limℂ 𝐵 ) → ( ( 𝐹 ↾ 𝐶 ) : dom ( 𝐹 ↾ 𝐶 ) ⟶ ℂ ∧ dom ( 𝐹 ↾ 𝐶 ) ⊆ ℂ ∧ 𝐵 ∈ ℂ ) )
8 7 simp3d ⊢ ( 𝑥 ∈ ( ( 𝐹 ↾ 𝐶 ) limℂ 𝐵 ) → 𝐵 ∈ ℂ )
9 limccl ⊢ ( ( 𝐹 ↾ 𝐶 ) limℂ 𝐵 ) ⊆ ℂ
10 9 sseli ⊢ ( 𝑥 ∈ ( ( 𝐹 ↾ 𝐶 ) limℂ 𝐵 ) → 𝑥 ∈ ℂ )
11 8 10 jca ⊢ ( 𝑥 ∈ ( ( 𝐹 ↾ 𝐶 ) limℂ 𝐵 ) → ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) )
12 11 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝐹 ↾ 𝐶 ) limℂ 𝐵 ) → ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) )
13 limcrcl ⊢ ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) )
14 13 simp3d ⊢ ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) → 𝐵 ∈ ℂ )
15 limccl ⊢ ( 𝐹 limℂ 𝐵 ) ⊆ ℂ
16 15 sseli ⊢ ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) → 𝑥 ∈ ℂ )
17 14 16 jca ⊢ ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) → ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) )
18 17 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) → ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) )
19 4 cnfldtopon ⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
20 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → 𝐴 ⊆ ℂ )
21 simprl ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → 𝐵 ∈ ℂ )
22 21 snssd ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → { 𝐵 } ⊆ ℂ )
23 20 22 unssd ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝐴 ∪ { 𝐵 } ) ⊆ ℂ )
24 resttopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ ( 𝐴 ∪ { 𝐵 } ) ⊆ ℂ ) → ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ∈ ( TopOn ‘ ( 𝐴 ∪ { 𝐵 } ) ) )
25 19 23 24 sylancr ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ∈ ( TopOn ‘ ( 𝐴 ∪ { 𝐵 } ) ) )
26 5 25 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → 𝐽 ∈ ( TopOn ‘ ( 𝐴 ∪ { 𝐵 } ) ) )
27 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ ( 𝐴 ∪ { 𝐵 } ) ) → 𝐽 ∈ Top )
28 26 27 syl ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → 𝐽 ∈ Top )
29 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → 𝐶 ⊆ 𝐴 )
30 unss1 ⊢ ( 𝐶 ⊆ 𝐴 → ( 𝐶 ∪ { 𝐵 } ) ⊆ ( 𝐴 ∪ { 𝐵 } ) )
31 29 30 syl ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝐶 ∪ { 𝐵 } ) ⊆ ( 𝐴 ∪ { 𝐵 } ) )
32 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ ( 𝐴 ∪ { 𝐵 } ) ) → ( 𝐴 ∪ { 𝐵 } ) = ∪ 𝐽 )
33 26 32 syl ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝐴 ∪ { 𝐵 } ) = ∪ 𝐽 )
34 31 33 sseqtrd ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝐶 ∪ { 𝐵 } ) ⊆ ∪ 𝐽 )
35 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → 𝐵 ∈ ( ( int ‘ 𝐽 ) ‘ ( 𝐶 ∪ { 𝐵 } ) ) )
36 elun ⊢ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↔ ( 𝑧 ∈ 𝐴 ∨ 𝑧 ∈ { 𝐵 } ) )
37 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑥 ∈ ℂ )
38 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → 𝐹 : 𝐴 ⟶ ℂ )
39 38 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
40 37 39 ifcld ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) ∧ 𝑧 ∈ 𝐴 ) → if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ∈ ℂ )
41 elsni ⊢ ( 𝑧 ∈ { 𝐵 } → 𝑧 = 𝐵 )
42 41 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) ∧ 𝑧 ∈ { 𝐵 } ) → 𝑧 = 𝐵 )
43 42 iftrued ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) ∧ 𝑧 ∈ { 𝐵 } ) → if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) = 𝑥 )
44 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) ∧ 𝑧 ∈ { 𝐵 } ) → 𝑥 ∈ ℂ )
45 43 44 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) ∧ 𝑧 ∈ { 𝐵 } ) → if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ∈ ℂ )
46 40 45 jaodan ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) ∧ ( 𝑧 ∈ 𝐴 ∨ 𝑧 ∈ { 𝐵 } ) ) → if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ∈ ℂ )
47 36 46 sylan2b ⊢ ( ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) ∧ 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ) → if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ∈ ℂ )
48 47 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ) : ( 𝐴 ∪ { 𝐵 } ) ⟶ ℂ )
49 33 feq2d ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ) : ( 𝐴 ∪ { 𝐵 } ) ⟶ ℂ ↔ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ) : ∪ 𝐽 ⟶ ℂ ) )
50 48 49 mpbid ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ) : ∪ 𝐽 ⟶ ℂ )
51 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
52 19 toponunii ⊢ ℂ = ∪ 𝐾
53 51 52 cnprest ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝐶 ∪ { 𝐵 } ) ⊆ ∪ 𝐽 ) ∧ ( 𝐵 ∈ ( ( int ‘ 𝐽 ) ‘ ( 𝐶 ∪ { 𝐵 } ) ) ∧ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ) : ∪ 𝐽 ⟶ ℂ ) ) → ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ↔ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ) ↾ ( 𝐶 ∪ { 𝐵 } ) ) ∈ ( ( ( 𝐽 ↾t ( 𝐶 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ) )
54 28 34 35 50 53 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ↔ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ) ↾ ( 𝐶 ∪ { 𝐵 } ) ) ∈ ( ( ( 𝐽 ↾t ( 𝐶 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ) )
55 eqid ⊢ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) )
56 5 4 55 38 20 21 ellimc ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ↔ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) )
57 eqid ⊢ ( 𝐾 ↾t ( 𝐶 ∪ { 𝐵 } ) ) = ( 𝐾 ↾t ( 𝐶 ∪ { 𝐵 } ) )
58 eqid ⊢ ( 𝑧 ∈ ( 𝐶 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝐶 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑧 ) ) )
59 38 29 fssresd ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ ℂ )
60 29 20 sstrd ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → 𝐶 ⊆ ℂ )
61 57 4 58 59 60 21 ellimc ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑥 ∈ ( ( 𝐹 ↾ 𝐶 ) limℂ 𝐵 ) ↔ ( 𝑧 ∈ ( 𝐶 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑧 ) ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐶 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ) )
62 elun ⊢ ( 𝑧 ∈ ( 𝐶 ∪ { 𝐵 } ) ↔ ( 𝑧 ∈ 𝐶 ∨ 𝑧 ∈ { 𝐵 } ) )
63 velsn ⊢ ( 𝑧 ∈ { 𝐵 } ↔ 𝑧 = 𝐵 )
64 63 orbi2i ⊢ ( ( 𝑧 ∈ 𝐶 ∨ 𝑧 ∈ { 𝐵 } ) ↔ ( 𝑧 ∈ 𝐶 ∨ 𝑧 = 𝐵 ) )
65 62 64 bitri ⊢ ( 𝑧 ∈ ( 𝐶 ∪ { 𝐵 } ) ↔ ( 𝑧 ∈ 𝐶 ∨ 𝑧 = 𝐵 ) )
66 pm5.61 ⊢ ( ( ( 𝑧 ∈ 𝐶 ∨ 𝑧 = 𝐵 ) ∧ ¬ 𝑧 = 𝐵 ) ↔ ( 𝑧 ∈ 𝐶 ∧ ¬ 𝑧 = 𝐵 ) )
67 fvres ⊢ ( 𝑧 ∈ 𝐶 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
68 67 adantr ⊢ ( ( 𝑧 ∈ 𝐶 ∧ ¬ 𝑧 = 𝐵 ) → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
69 66 68 sylbi ⊢ ( ( ( 𝑧 ∈ 𝐶 ∨ 𝑧 = 𝐵 ) ∧ ¬ 𝑧 = 𝐵 ) → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
70 69 ifeq2da ⊢ ( ( 𝑧 ∈ 𝐶 ∨ 𝑧 = 𝐵 ) → if ( 𝑧 = 𝐵 , 𝑥 , ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑧 ) ) = if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) )
71 65 70 sylbi ⊢ ( 𝑧 ∈ ( 𝐶 ∪ { 𝐵 } ) → if ( 𝑧 = 𝐵 , 𝑥 , ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑧 ) ) = if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) )
72 71 mpteq2ia ⊢ ( 𝑧 ∈ ( 𝐶 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝐶 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) )
73 31 resmptd ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ) ↾ ( 𝐶 ∪ { 𝐵 } ) ) = ( 𝑧 ∈ ( 𝐶 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ) )
74 72 73 eqtr4id ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑧 ∈ ( 𝐶 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑧 ) ) ) = ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ) ↾ ( 𝐶 ∪ { 𝐵 } ) ) )
75 5 oveq1i ⊢ ( 𝐽 ↾t ( 𝐶 ∪ { 𝐵 } ) ) = ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ↾t ( 𝐶 ∪ { 𝐵 } ) )
76 cnex ⊢ ℂ ∈ V
77 76 ssex ⊢ ( ( 𝐴 ∪ { 𝐵 } ) ⊆ ℂ → ( 𝐴 ∪ { 𝐵 } ) ∈ V )
78 23 77 syl ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝐴 ∪ { 𝐵 } ) ∈ V )
79 restabs ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ ( 𝐶 ∪ { 𝐵 } ) ⊆ ( 𝐴 ∪ { 𝐵 } ) ∧ ( 𝐴 ∪ { 𝐵 } ) ∈ V ) → ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ↾t ( 𝐶 ∪ { 𝐵 } ) ) = ( 𝐾 ↾t ( 𝐶 ∪ { 𝐵 } ) ) )
80 19 31 78 79 mp3an2i ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ↾t ( 𝐶 ∪ { 𝐵 } ) ) = ( 𝐾 ↾t ( 𝐶 ∪ { 𝐵 } ) ) )
81 75 80 eqtr2id ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝐾 ↾t ( 𝐶 ∪ { 𝐵 } ) ) = ( 𝐽 ↾t ( 𝐶 ∪ { 𝐵 } ) ) )
82 81 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( ( 𝐾 ↾t ( 𝐶 ∪ { 𝐵 } ) ) CnP 𝐾 ) = ( ( 𝐽 ↾t ( 𝐶 ∪ { 𝐵 } ) ) CnP 𝐾 ) )
83 82 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( ( ( 𝐾 ↾t ( 𝐶 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) = ( ( ( 𝐽 ↾t ( 𝐶 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) )
84 74 83 eleq12d ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( ( 𝑧 ∈ ( 𝐶 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑧 ) ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐶 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ↔ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ) ↾ ( 𝐶 ∪ { 𝐵 } ) ) ∈ ( ( ( 𝐽 ↾t ( 𝐶 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ) )
85 61 84 bitrd ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑥 ∈ ( ( 𝐹 ↾ 𝐶 ) limℂ 𝐵 ) ↔ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑥 , ( 𝐹 ‘ 𝑧 ) ) ) ↾ ( 𝐶 ∪ { 𝐵 } ) ) ∈ ( ( ( 𝐽 ↾t ( 𝐶 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ) )
86 54 56 85 3bitr4rd ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑥 ∈ ( ( 𝐹 ↾ 𝐶 ) limℂ 𝐵 ) ↔ 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ) )
87 86 ex ⊢ ( 𝜑 → ( ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ∈ ( ( 𝐹 ↾ 𝐶 ) limℂ 𝐵 ) ↔ 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ) ) )
88 12 18 87 pm5.21ndd ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝐹 ↾ 𝐶 ) limℂ 𝐵 ) ↔ 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ) )
89 88 eqrdv ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐶 ) limℂ 𝐵 ) = ( 𝐹 limℂ 𝐵 ) )