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ℂ 𝐵 ) ) ) )