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 ↾ C lim ℂ B = F lim ℂ 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 ↾ C lim ℂ B → F ↾ C : dom ⁡ F ↾ C ⟶ ℂ ∧ dom ⁡ F ↾ C ⊆ ℂ ∧ B ∈ ℂ
8 7 simp3d ⊢ x ∈ F ↾ C lim ℂ B → B ∈ ℂ
9 limccl ⊢ F ↾ C lim ℂ B ⊆ ℂ
10 9 sseli ⊢ x ∈ F ↾ C lim ℂ B → x ∈ ℂ
11 8 10 jca ⊢ x ∈ F ↾ C lim ℂ B → B ∈ ℂ ∧ x ∈ ℂ
12 11 a1i ⊢ φ → x ∈ F ↾ C lim ℂ B → B ∈ ℂ ∧ x ∈ ℂ
13 limcrcl ⊢ x ∈ F lim ℂ B → F : dom ⁡ F ⟶ ℂ ∧ dom ⁡ F ⊆ ℂ ∧ B ∈ ℂ
14 13 simp3d ⊢ x ∈ F lim ℂ B → B ∈ ℂ
15 limccl ⊢ F lim ℂ B ⊆ ℂ
16 15 sseli ⊢ x ∈ F lim ℂ B → x ∈ ℂ
17 14 16 jca ⊢ x ∈ F lim ℂ B → B ∈ ℂ ∧ x ∈ ℂ
18 17 a1i ⊢ φ → x ∈ F lim ℂ 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 → if z = B x F ⁡ z ∈ ℂ
41 elsni ⊢ z ∈ B → z = B
42 41 adantl ⊢ φ ∧ B ∈ ℂ ∧ x ∈ ℂ ∧ z ∈ B → z = B
43 42 iftrued ⊢ φ ∧ B ∈ ℂ ∧ x ∈ ℂ ∧ z ∈ B → if z = B x F ⁡ z = x
44 simplrr ⊢ φ ∧ B ∈ ℂ ∧ x ∈ ℂ ∧ z ∈ B → x ∈ ℂ
45 43 44 eqeltrd ⊢ φ ∧ B ∈ ℂ ∧ x ∈ ℂ ∧ z ∈ B → if z = B x F ⁡ z ∈ ℂ
46 40 45 jaodan ⊢ φ ∧ B ∈ ℂ ∧ x ∈ ℂ ∧ z ∈ A ∨ z ∈ B → if z = B x F ⁡ z ∈ ℂ
47 36 46 sylan2b ⊢ φ ∧ B ∈ ℂ ∧ x ∈ ℂ ∧ z ∈ A ∪ B → if z = B x F ⁡ z ∈ ℂ
48 47 fmpttd ⊢ φ ∧ B ∈ ℂ ∧ x ∈ ℂ → z ∈ A ∪ B ⟼ if z = B x F ⁡ z : A ∪ B ⟶ ℂ
49 33 feq2d ⊢ φ ∧ B ∈ ℂ ∧ x ∈ ℂ → z ∈ A ∪ B ⟼ if z = B x F ⁡ z : A ∪ B ⟶ ℂ ↔ z ∈ A ∪ B ⟼ if z = B x F ⁡ z : ⋃ J ⟶ ℂ
50 48 49 mpbid ⊢ φ ∧ B ∈ ℂ ∧ x ∈ ℂ → z ∈ A ∪ B ⟼ if z = B x F ⁡ 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 ⟼ if z = B x F ⁡ z : ⋃ J ⟶ ℂ → z ∈ A ∪ B ⟼ if z = B x F ⁡ z ∈ J CnP K ⁡ B ↔ z ∈ A ∪ B ⟼ if z = B x F ⁡ z ↾ C ∪ B ∈ J ↾ 𝑡 C ∪ B CnP K ⁡ B
54 28 34 35 50 53 syl22anc ⊢ φ ∧ B ∈ ℂ ∧ x ∈ ℂ → z ∈ A ∪ B ⟼ if z = B x F ⁡ z ∈ J CnP K ⁡ B ↔ z ∈ A ∪ B ⟼ if z = B x F ⁡ z ↾ C ∪ B ∈ J ↾ 𝑡 C ∪ B CnP K ⁡ B
55 eqid ⊢ z ∈ A ∪ B ⟼ if z = B x F ⁡ z = z ∈ A ∪ B ⟼ if z = B x F ⁡ z
56 5 4 55 38 20 21 ellimc ⊢ φ ∧ B ∈ ℂ ∧ x ∈ ℂ → x ∈ F lim ℂ B ↔ z ∈ A ∪ B ⟼ if z = B x F ⁡ z ∈ J CnP K ⁡ B
57 eqid ⊢ K ↾ 𝑡 C ∪ B = K ↾ 𝑡 C ∪ B
58 eqid ⊢ z ∈ C ∪ B ⟼ if z = B x F ↾ C ⁡ z = z ∈ C ∪ B ⟼ if z = B x F ↾ 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 ↾ C lim ℂ B ↔ z ∈ C ∪ B ⟼ if z = B x F ↾ C ⁡ z ∈ K ↾ 𝑡 C ∪ B CnP K ⁡ 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 → if z = B x F ↾ C ⁡ z = if z = B x F ⁡ z
71 65 70 sylbi ⊢ z ∈ C ∪ B → if z = B x F ↾ C ⁡ z = if z = B x F ⁡ z
72 71 mpteq2ia ⊢ z ∈ C ∪ B ⟼ if z = B x F ↾ C ⁡ z = z ∈ C ∪ B ⟼ if z = B x F ⁡ z
73 31 resmptd ⊢ φ ∧ B ∈ ℂ ∧ x ∈ ℂ → z ∈ A ∪ B ⟼ if z = B x F ⁡ z ↾ C ∪ B = z ∈ C ∪ B ⟼ if z = B x F ⁡ z
74 72 73 eqtr4id ⊢ φ ∧ B ∈ ℂ ∧ x ∈ ℂ → z ∈ C ∪ B ⟼ if z = B x F ↾ C ⁡ z = z ∈ A ∪ B ⟼ if z = B x F ⁡ 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 ∪ B CnP K = J ↾ 𝑡 C ∪ B CnP K
83 82 fveq1d ⊢ φ ∧ B ∈ ℂ ∧ x ∈ ℂ → K ↾ 𝑡 C ∪ B CnP K ⁡ B = J ↾ 𝑡 C ∪ B CnP K ⁡ B
84 74 83 eleq12d ⊢ φ ∧ B ∈ ℂ ∧ x ∈ ℂ → z ∈ C ∪ B ⟼ if z = B x F ↾ C ⁡ z ∈ K ↾ 𝑡 C ∪ B CnP K ⁡ B ↔ z ∈ A ∪ B ⟼ if z = B x F ⁡ z ↾ C ∪ B ∈ J ↾ 𝑡 C ∪ B CnP K ⁡ B
85 61 84 bitrd ⊢ φ ∧ B ∈ ℂ ∧ x ∈ ℂ → x ∈ F ↾ C lim ℂ B ↔ z ∈ A ∪ B ⟼ if z = B x F ⁡ z ↾ C ∪ B ∈ J ↾ 𝑡 C ∪ B CnP K ⁡ B
86 54 56 85 3bitr4rd ⊢ φ ∧ B ∈ ℂ ∧ x ∈ ℂ → x ∈ F ↾ C lim ℂ B ↔ x ∈ F lim ℂ B
87 86 ex ⊢ φ → B ∈ ℂ ∧ x ∈ ℂ → x ∈ F ↾ C lim ℂ B ↔ x ∈ F lim ℂ B
88 12 18 87 pm5.21ndd ⊢ φ → x ∈ F ↾ C lim ℂ B ↔ x ∈ F lim ℂ B
89 88 eqrdv ⊢ φ → F ↾ C lim ℂ B = F lim ℂ B