Metamath Proof Explorer

Theorem cnplimc

Description: A function is continuous at B iff its limit at B equals the value of the function there. (Contributed by Mario Carneiro, 28-Dec-2016)

Ref Expression
Hypotheses cnplimc.k ⊢ K = TopOpen ⁡ ℂ fld
cnplimc.j ⊢ J = K ↾ 𝑡 A
Assertion cnplimc ⊢ A ⊆ ℂ ∧ B ∈ A → F ∈ J CnP K ⁡ B ↔ F : A ⟶ ℂ ∧ F ⁡ B ∈ F lim ℂ B

Proof

Step Hyp Ref Expression
1 cnplimc.k ⊢ K = TopOpen ⁡ ℂ fld
2 cnplimc.j ⊢ J = K ↾ 𝑡 A
3 1 cnfldtopon ⊢ K ∈ TopOn ⁡ ℂ
4 simpl ⊢ A ⊆ ℂ ∧ B ∈ A → A ⊆ ℂ
5 resttopon ⊢ K ∈ TopOn ⁡ ℂ ∧ A ⊆ ℂ → K ↾ 𝑡 A ∈ TopOn ⁡ A
6 3 4 5 sylancr ⊢ A ⊆ ℂ ∧ B ∈ A → K ↾ 𝑡 A ∈ TopOn ⁡ A
7 2 6 eqeltrid ⊢ A ⊆ ℂ ∧ B ∈ A → J ∈ TopOn ⁡ A
8 cnpf2 ⊢ J ∈ TopOn ⁡ A ∧ K ∈ TopOn ⁡ ℂ ∧ F ∈ J CnP K ⁡ B → F : A ⟶ ℂ
9 8 3expia ⊢ J ∈ TopOn ⁡ A ∧ K ∈ TopOn ⁡ ℂ → F ∈ J CnP K ⁡ B → F : A ⟶ ℂ
10 7 3 9 sylancl ⊢ A ⊆ ℂ ∧ B ∈ A → F ∈ J CnP K ⁡ B → F : A ⟶ ℂ
11 10 pm4.71rd ⊢ A ⊆ ℂ ∧ B ∈ A → F ∈ J CnP K ⁡ B ↔ F : A ⟶ ℂ ∧ F ∈ J CnP K ⁡ B
12 simpr ⊢ A ⊆ ℂ ∧ B ∈ A ∧ F : A ⟶ ℂ → F : A ⟶ ℂ
13 simplr ⊢ A ⊆ ℂ ∧ B ∈ A ∧ F : A ⟶ ℂ → B ∈ A
14 13 snssd ⊢ A ⊆ ℂ ∧ B ∈ A ∧ F : A ⟶ ℂ → B ⊆ A
15 ssequn2 ⊢ B ⊆ A ↔ A ∪ B = A
16 14 15 sylib ⊢ A ⊆ ℂ ∧ B ∈ A ∧ F : A ⟶ ℂ → A ∪ B = A
17 16 feq2d ⊢ A ⊆ ℂ ∧ B ∈ A ∧ F : A ⟶ ℂ → F : A ∪ B ⟶ ℂ ↔ F : A ⟶ ℂ
18 12 17 mpbird ⊢ A ⊆ ℂ ∧ B ∈ A ∧ F : A ⟶ ℂ → F : A ∪ B ⟶ ℂ
19 18 feqmptd ⊢ A ⊆ ℂ ∧ B ∈ A ∧ F : A ⟶ ℂ → F = x ∈ A ∪ B ⟼ F ⁡ x
20 16 oveq2d ⊢ A ⊆ ℂ ∧ B ∈ A ∧ F : A ⟶ ℂ → K ↾ 𝑡 A ∪ B = K ↾ 𝑡 A
21 2 20 eqtr4id ⊢ A ⊆ ℂ ∧ B ∈ A ∧ F : A ⟶ ℂ → J = K ↾ 𝑡 A ∪ B
22 21 oveq1d ⊢ A ⊆ ℂ ∧ B ∈ A ∧ F : A ⟶ ℂ → J CnP K = K ↾ 𝑡 A ∪ B CnP K
23 22 fveq1d ⊢ A ⊆ ℂ ∧ B ∈ A ∧ F : A ⟶ ℂ → J CnP K ⁡ B = K ↾ 𝑡 A ∪ B CnP K ⁡ B
24 19 23 eleq12d ⊢ A ⊆ ℂ ∧ B ∈ A ∧ F : A ⟶ ℂ → F ∈ J CnP K ⁡ B ↔ x ∈ A ∪ B ⟼ F ⁡ x ∈ K ↾ 𝑡 A ∪ B CnP K ⁡ B
25 eqid ⊢ K ↾ 𝑡 A ∪ B = K ↾ 𝑡 A ∪ B
26 ifid ⊢ if x = B F ⁡ x F ⁡ x = F ⁡ x
27 fveq2 ⊢ x = B → F ⁡ x = F ⁡ B
28 27 adantl ⊢ x ∈ A ∪ B ∧ x = B → F ⁡ x = F ⁡ B
29 28 ifeq1da ⊢ x ∈ A ∪ B → if x = B F ⁡ x F ⁡ x = if x = B F ⁡ B F ⁡ x
30 26 29 syl5eqr ⊢ x ∈ A ∪ B → F ⁡ x = if x = B F ⁡ B F ⁡ x
31 30 mpteq2ia ⊢ x ∈ A ∪ B ⟼ F ⁡ x = x ∈ A ∪ B ⟼ if x = B F ⁡ B F ⁡ x
32 simpll ⊢ A ⊆ ℂ ∧ B ∈ A ∧ F : A ⟶ ℂ → A ⊆ ℂ
33 32 13 sseldd ⊢ A ⊆ ℂ ∧ B ∈ A ∧ F : A ⟶ ℂ → B ∈ ℂ
34 25 1 31 12 32 33 ellimc ⊢ A ⊆ ℂ ∧ B ∈ A ∧ F : A ⟶ ℂ → F ⁡ B ∈ F lim ℂ B ↔ x ∈ A ∪ B ⟼ F ⁡ x ∈ K ↾ 𝑡 A ∪ B CnP K ⁡ B
35 24 34 bitr4d ⊢ A ⊆ ℂ ∧ B ∈ A ∧ F : A ⟶ ℂ → F ∈ J CnP K ⁡ B ↔ F ⁡ B ∈ F lim ℂ B
36 35 pm5.32da ⊢ A ⊆ ℂ ∧ B ∈ A → F : A ⟶ ℂ ∧ F ∈ J CnP K ⁡ B ↔ F : A ⟶ ℂ ∧ F ⁡ B ∈ F lim ℂ B
37 11 36 bitrd ⊢ A ⊆ ℂ ∧ B ∈ A → F ∈ J CnP K ⁡ B ↔ F : A ⟶ ℂ ∧ F ⁡ B ∈ F lim ℂ B