This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ellimc

Description: Value of the limit predicate. C is the limit of the function F at B if the function G , formed by adding B to the domain of F and setting it to C , is continuous at B . (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses limcval.j ⊢ 𝐽 = ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) )
limcval.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
ellimc.g ⊢ 𝐺 = ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) )
ellimc.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
ellimc.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
ellimc.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
Assertion ellimc ( 𝜑 → ( 𝐶 ∈ ( 𝐹 limℂ 𝐵 ) ↔ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 limcval.j ⊢ 𝐽 = ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) )
2 limcval.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
3 ellimc.g ⊢ 𝐺 = ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) )
4 ellimc.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
5 ellimc.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
6 ellimc.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
7 1 2 limcfval ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 limℂ 𝐵 ) = { 𝑦 ∣ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) } ∧ ( 𝐹 limℂ 𝐵 ) ⊆ ℂ ) )
8 4 5 6 7 syl3anc ⊢ ( 𝜑 → ( ( 𝐹 limℂ 𝐵 ) = { 𝑦 ∣ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) } ∧ ( 𝐹 limℂ 𝐵 ) ⊆ ℂ ) )
9 8 simpld ⊢ ( 𝜑 → ( 𝐹 limℂ 𝐵 ) = { 𝑦 ∣ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) } )
10 9 eleq2d ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐹 limℂ 𝐵 ) ↔ 𝐶 ∈ { 𝑦 ∣ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) } ) )
11 1 2 3 limcvallem ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) → 𝐶 ∈ ℂ ) )
12 4 5 6 11 syl3anc ⊢ ( 𝜑 → ( 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) → 𝐶 ∈ ℂ ) )
13 ifeq1 ⊢ ( 𝑦 = 𝐶 → if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) = if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) )
14 13 mpteq2dv ⊢ ( 𝑦 = 𝐶 → ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) )
15 14 3 eqtr4di ⊢ ( 𝑦 = 𝐶 → ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) = 𝐺 )
16 15 eleq1d ⊢ ( 𝑦 = 𝐶 → ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ↔ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) )
17 16 elab3g ⊢ ( ( 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) → 𝐶 ∈ ℂ ) → ( 𝐶 ∈ { 𝑦 ∣ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) } ↔ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) )
18 12 17 syl ⊢ ( 𝜑 → ( 𝐶 ∈ { 𝑦 ∣ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) } ↔ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) )
19 10 18 bitrd ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐹 limℂ 𝐵 ) ↔ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) )