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

Metamath Proof Explorer

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