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 ⊢φ→F:A⟶ℂ
limcres.c ⊢φ→C⊆A
limcres.a ⊢φ→A⊆ℂ
limcres.k ⊢K=TopOpen⁡ℂfld
limcres.j ⊢J=K↾𝑡A∪B
limcres.i ⊢φ→B∈int⁡J⁡C∪B
Assertion limcres ⊢φ→F↾ClimℂB=FlimℂB

Proof

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