Metamath Proof Explorer

Theorem limcmpt2

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

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

Proof

Step Hyp Ref Expression
1 limcmpt2.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
2 limcmpt2.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
3 limcmpt2.f ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵 ) ) → 𝐷 ∈ ℂ )
4 limcmpt2.j ⊢ 𝐽 = ( 𝐾 ↾t 𝐴 )
5 limcmpt2.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
6 1 ssdifssd ⊢ ( 𝜑 → ( 𝐴 ∖ { 𝐵 } ) ⊆ ℂ )
7 1 2 sseldd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
8 eldifsn ⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵 ) )
9 8 3 sylan2b ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝐷 ∈ ℂ )
10 eqid ⊢ ( 𝐾 ↾t ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) ) = ( 𝐾 ↾t ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) )
11 6 7 9 10 5 limcmpt ⊢ ( 𝜑 → ( 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ 𝐷 ) limℂ 𝐵 ) ↔ ( 𝑧 ∈ ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , 𝐷 ) ) ∈ ( ( ( 𝐾 ↾t ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ) )
12 undif1 ⊢ ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) = ( 𝐴 ∪ { 𝐵 } )
13 2 snssd ⊢ ( 𝜑 → { 𝐵 } ⊆ 𝐴 )
14 ssequn2 ⊢ ( { 𝐵 } ⊆ 𝐴 ↔ ( 𝐴 ∪ { 𝐵 } ) = 𝐴 )
15 13 14 sylib ⊢ ( 𝜑 → ( 𝐴 ∪ { 𝐵 } ) = 𝐴 )
16 12 15 syl5eq ⊢ ( 𝜑 → ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) = 𝐴 )
17 16 mpteq1d ⊢ ( 𝜑 → ( 𝑧 ∈ ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , 𝐷 ) ) = ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 = 𝐵 , 𝐶 , 𝐷 ) ) )
18 16 oveq2d ⊢ ( 𝜑 → ( 𝐾 ↾t ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) ) = ( 𝐾 ↾t 𝐴 ) )
19 18 4 eqtr4di ⊢ ( 𝜑 → ( 𝐾 ↾t ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) ) = 𝐽 )
20 19 oveq1d ⊢ ( 𝜑 → ( ( 𝐾 ↾t ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) ) CnP 𝐾 ) = ( 𝐽 CnP 𝐾 ) )
21 20 fveq1d ⊢ ( 𝜑 → ( ( ( 𝐾 ↾t ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) = ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) )
22 17 21 eleq12d ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , 𝐷 ) ) ∈ ( ( ( 𝐾 ↾t ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ↔ ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 = 𝐵 , 𝐶 , 𝐷 ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) )
23 11 22 bitrd ⊢ ( 𝜑 → ( 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ 𝐷 ) limℂ 𝐵 ) ↔ ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 = 𝐵 , 𝐶 , 𝐷 ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) )