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 𝐾 = ( TopOpen ‘ ℂfld )
cnplimc.j 𝐽 = ( 𝐾t 𝐴 )
Assertion cnplimc ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ( 𝐹𝐵 ) ∈ ( 𝐹 lim 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 cnplimc.k 𝐾 = ( TopOpen ‘ ℂfld )
2 cnplimc.j 𝐽 = ( 𝐾t 𝐴 )
3 1 cnfldtopon 𝐾 ∈ ( TopOn ‘ ℂ )
4 simpl ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) → 𝐴 ⊆ ℂ )
5 resttopon ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝐴 ⊆ ℂ ) → ( 𝐾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
6 3 4 5 sylancr ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) → ( 𝐾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
7 2 6 eqeltrid ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) → 𝐽 ∈ ( TopOn ‘ 𝐴 ) )
8 cnpf2 ( ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) ∧ 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) → 𝐹 : 𝐴 ⟶ ℂ )
9 8 3expia ( ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) ∧ 𝐾 ∈ ( TopOn ‘ ℂ ) ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) → 𝐹 : 𝐴 ⟶ ℂ ) )
10 7 3 9 sylancl ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) → 𝐹 : 𝐴 ⟶ ℂ ) )
11 10 pm4.71rd ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) ) )
12 simpr ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ )
13 simplr ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐵𝐴 )
14 13 snssd ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → { 𝐵 } ⊆ 𝐴 )
15 ssequn2 ( { 𝐵 } ⊆ 𝐴 ↔ ( 𝐴 ∪ { 𝐵 } ) = 𝐴 )
16 14 15 sylib ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( 𝐴 ∪ { 𝐵 } ) = 𝐴 )
17 16 feq2d ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( 𝐹 : ( 𝐴 ∪ { 𝐵 } ) ⟶ ℂ ↔ 𝐹 : 𝐴 ⟶ ℂ ) )
18 12 17 mpbird ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐹 : ( 𝐴 ∪ { 𝐵 } ) ⟶ ℂ )
19 18 feqmptd ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐹 = ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ( 𝐹𝑥 ) ) )
20 16 oveq2d ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( 𝐾t ( 𝐴 ∪ { 𝐵 } ) ) = ( 𝐾t 𝐴 ) )
21 2 20 eqtr4id ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐽 = ( 𝐾t ( 𝐴 ∪ { 𝐵 } ) ) )
22 21 oveq1d ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( 𝐽 CnP 𝐾 ) = ( ( 𝐾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) )
23 22 fveq1d ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) = ( ( ( 𝐾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) )
24 19 23 eleq12d ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ↔ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ( 𝐹𝑥 ) ) ∈ ( ( ( 𝐾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ) )
25 eqid ( 𝐾t ( 𝐴 ∪ { 𝐵 } ) ) = ( 𝐾t ( 𝐴 ∪ { 𝐵 } ) )
26 ifid if ( 𝑥 = 𝐵 , ( 𝐹𝑥 ) , ( 𝐹𝑥 ) ) = ( 𝐹𝑥 )
27 fveq2 ( 𝑥 = 𝐵 → ( 𝐹𝑥 ) = ( 𝐹𝐵 ) )
28 27 adantl ( ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ∧ 𝑥 = 𝐵 ) → ( 𝐹𝑥 ) = ( 𝐹𝐵 ) )
29 28 ifeq1da ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) → if ( 𝑥 = 𝐵 , ( 𝐹𝑥 ) , ( 𝐹𝑥 ) ) = if ( 𝑥 = 𝐵 , ( 𝐹𝐵 ) , ( 𝐹𝑥 ) ) )
30 26 29 eqtr3id ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) → ( 𝐹𝑥 ) = if ( 𝑥 = 𝐵 , ( 𝐹𝐵 ) , ( 𝐹𝑥 ) ) )
31 30 mpteq2ia ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ( 𝐹𝑥 ) ) = ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , ( 𝐹𝐵 ) , ( 𝐹𝑥 ) ) )
32 simpll ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐴 ⊆ ℂ )
33 32 13 sseldd ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐵 ∈ ℂ )
34 25 1 31 12 32 33 ellimc ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( ( 𝐹𝐵 ) ∈ ( 𝐹 lim 𝐵 ) ↔ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ( 𝐹𝑥 ) ) ∈ ( ( ( 𝐾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ) )
35 24 34 bitr4d ( ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ↔ ( 𝐹𝐵 ) ∈ ( 𝐹 lim 𝐵 ) ) )
36 35 pm5.32da ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) → ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ( 𝐹𝐵 ) ∈ ( 𝐹 lim 𝐵 ) ) ) )
37 11 36 bitrd ( ( 𝐴 ⊆ ℂ ∧ 𝐵𝐴 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ( 𝐹𝐵 ) ∈ ( 𝐹 lim 𝐵 ) ) ) )