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 𝐾 ) ‘ 𝐵 ) ) )