Theorem limcmpt

Description: Express the limit operator for a function defined by a mapping. (Contributed by Mario Carneiro, 25-Dec-2016)

	Ref	Expression
Hypotheses	limcmpt.a	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
	limcmpt.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	limcmpt.f	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐷 ∈ ℂ )
	limcmpt.j	⊢ 𝐽 = ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) )
	limcmpt.k	⊢ 𝐾 = ( TopOpen ‘ ℂfld )
Assertion	limcmpt	⊢ ( 𝜑 → ( 𝐶 ∈ ( ( 𝑧 ∈ 𝐴 ↦ 𝐷 ) limℂ 𝐵 ) ↔ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , 𝐷 ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		limcmpt.a	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
2		limcmpt.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		limcmpt.f	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐷 ∈ ℂ )
4		limcmpt.j	⊢ 𝐽 = ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) )
5		limcmpt.k	⊢ 𝐾 = ( TopOpen ‘ ℂfld )
6		nfcv	⊢ Ⅎ 𝑦 if ( 𝑧 = 𝐵 , 𝐶 , ( ( 𝑧 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑧 ) )
7		nfv	⊢ Ⅎ 𝑧 𝑦 = 𝐵
8		nfcv	⊢ Ⅎ 𝑧 𝐶
9		nffvmpt1	⊢ Ⅎ 𝑧 ( ( 𝑧 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑦 )
10	7 8 9	nfif	⊢ Ⅎ 𝑧 if ( 𝑦 = 𝐵 , 𝐶 , ( ( 𝑧 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑦 ) )
11		eqeq1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 = 𝐵 ↔ 𝑦 = 𝐵 ) )
12		fveq2	⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑧 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑦 ) )
13	11 12	ifbieq2d	⊢ ( 𝑧 = 𝑦 → if ( 𝑧 = 𝐵 , 𝐶 , ( ( 𝑧 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑧 ) ) = if ( 𝑦 = 𝐵 , 𝐶 , ( ( 𝑧 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑦 ) ) )
14	6 10 13	cbvmpt	⊢ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( ( 𝑧 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑧 ) ) ) = ( 𝑦 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑦 = 𝐵 , 𝐶 , ( ( 𝑧 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑦 ) ) )
15	3	fmpttd	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐴 ↦ 𝐷 ) : 𝐴 ⟶ ℂ )
16	4 5 14 15 1 2	ellimc	⊢ ( 𝜑 → ( 𝐶 ∈ ( ( 𝑧 ∈ 𝐴 ↦ 𝐷 ) limℂ 𝐵 ) ↔ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( ( 𝑧 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) )
17		elun	⊢ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↔ ( 𝑧 ∈ 𝐴 ∨ 𝑧 ∈ { 𝐵 } ) )
18		velsn	⊢ ( 𝑧 ∈ { 𝐵 } ↔ 𝑧 = 𝐵 )
19	18	orbi2i	⊢ ( ( 𝑧 ∈ 𝐴 ∨ 𝑧 ∈ { 𝐵 } ) ↔ ( 𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐵 ) )
20	17 19	bitri	⊢ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↔ ( 𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐵 ) )
21		pm5.61	⊢ ( ( ( 𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐵 ) ∧ ¬ 𝑧 = 𝐵 ) ↔ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 = 𝐵 ) )
22	21	simplbi	⊢ ( ( ( 𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐵 ) ∧ ¬ 𝑧 = 𝐵 ) → 𝑧 ∈ 𝐴 )
23	20 22	sylanb	⊢ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ∧ ¬ 𝑧 = 𝐵 ) → 𝑧 ∈ 𝐴 )
24	23 3	sylan2	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ∧ ¬ 𝑧 = 𝐵 ) ) → 𝐷 ∈ ℂ )
25		eqid	⊢ ( 𝑧 ∈ 𝐴 ↦ 𝐷 ) = ( 𝑧 ∈ 𝐴 ↦ 𝐷 )
26	25	fvmpt2	⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝐷 ∈ ℂ ) → ( ( 𝑧 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑧 ) = 𝐷 )
27	23 24 26	syl2an2	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ∧ ¬ 𝑧 = 𝐵 ) ) → ( ( 𝑧 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑧 ) = 𝐷 )
28	27	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ¬ 𝑧 = 𝐵 ) → ( ( 𝑧 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑧 ) = 𝐷 )
29	28	ifeq2da	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ) → if ( 𝑧 = 𝐵 , 𝐶 , ( ( 𝑧 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑧 ) ) = if ( 𝑧 = 𝐵 , 𝐶 , 𝐷 ) )
30	29	mpteq2dva	⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( ( 𝑧 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , 𝐷 ) ) )
31	30	eleq1d	⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( ( 𝑧 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑧 ) ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ↔ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , 𝐷 ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) )
32	16 31	bitrd	⊢ ( 𝜑 → ( 𝐶 ∈ ( ( 𝑧 ∈ 𝐴 ↦ 𝐷 ) limℂ 𝐵 ) ↔ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , 𝐷 ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) )