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

Metamath Proof Explorer

Definition df-limc

Description: Define the set of limits of a complex function at a point. Under normal circumstances, this will be a singleton or empty, depending on whether the limit exists. (Contributed by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion df-limc limℂ = ( 𝑓 ∈ ( ℂ ↑pm ℂ ) , 𝑥 ∈ ℂ ↦ { 𝑦 ∣ [ ( TopOpen ‘ ℂfld ) / 𝑗 ] ( 𝑧 ∈ ( dom 𝑓 ∪ { 𝑥 } ) ↦ if ( 𝑧 = 𝑥 , 𝑦 , ( 𝑓 ‘ 𝑧 ) ) ) ∈ ( ( ( 𝑗 ↾t ( dom 𝑓 ∪ { 𝑥 } ) ) CnP 𝑗 ) ‘ 𝑥 ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 climc ⊢ limℂ
1 vf ⊢ 𝑓
2 cc ⊢ ℂ
3 cpm ⊢ ↑pm
4 2 2 3 co ⊢ ( ℂ ↑pm ℂ )
5 vx ⊢ 𝑥
6 vy ⊢ 𝑦
7 ctopn ⊢ TopOpen
8 ccnfld ⊢ ℂfld
9 8 7 cfv ⊢ ( TopOpen ‘ ℂfld )
10 vj ⊢ 𝑗
11 vz ⊢ 𝑧
12 1 cv ⊢ 𝑓
13 12 cdm ⊢ dom 𝑓
14 5 cv ⊢ 𝑥
15 14 csn ⊢ { 𝑥 }
16 13 15 cun ⊢ ( dom 𝑓 ∪ { 𝑥 } )
17 11 cv ⊢ 𝑧
18 17 14 wceq ⊢ 𝑧 = 𝑥
19 6 cv ⊢ 𝑦
20 17 12 cfv ⊢ ( 𝑓 ‘ 𝑧 )
21 18 19 20 cif ⊢ if ( 𝑧 = 𝑥 , 𝑦 , ( 𝑓 ‘ 𝑧 ) )
22 11 16 21 cmpt ⊢ ( 𝑧 ∈ ( dom 𝑓 ∪ { 𝑥 } ) ↦ if ( 𝑧 = 𝑥 , 𝑦 , ( 𝑓 ‘ 𝑧 ) ) )
23 10 cv ⊢ 𝑗
24 crest ⊢ ↾t
25 23 16 24 co ⊢ ( 𝑗 ↾t ( dom 𝑓 ∪ { 𝑥 } ) )
26 ccnp ⊢ CnP
27 25 23 26 co ⊢ ( ( 𝑗 ↾t ( dom 𝑓 ∪ { 𝑥 } ) ) CnP 𝑗 )
28 14 27 cfv ⊢ ( ( ( 𝑗 ↾t ( dom 𝑓 ∪ { 𝑥 } ) ) CnP 𝑗 ) ‘ 𝑥 )
29 22 28 wcel ⊢ ( 𝑧 ∈ ( dom 𝑓 ∪ { 𝑥 } ) ↦ if ( 𝑧 = 𝑥 , 𝑦 , ( 𝑓 ‘ 𝑧 ) ) ) ∈ ( ( ( 𝑗 ↾t ( dom 𝑓 ∪ { 𝑥 } ) ) CnP 𝑗 ) ‘ 𝑥 )
30 29 10 9 wsbc ⊢ [ ( TopOpen ‘ ℂfld ) / 𝑗 ] ( 𝑧 ∈ ( dom 𝑓 ∪ { 𝑥 } ) ↦ if ( 𝑧 = 𝑥 , 𝑦 , ( 𝑓 ‘ 𝑧 ) ) ) ∈ ( ( ( 𝑗 ↾t ( dom 𝑓 ∪ { 𝑥 } ) ) CnP 𝑗 ) ‘ 𝑥 )
31 30 6 cab ⊢ { 𝑦 ∣ [ ( TopOpen ‘ ℂfld ) / 𝑗 ] ( 𝑧 ∈ ( dom 𝑓 ∪ { 𝑥 } ) ↦ if ( 𝑧 = 𝑥 , 𝑦 , ( 𝑓 ‘ 𝑧 ) ) ) ∈ ( ( ( 𝑗 ↾t ( dom 𝑓 ∪ { 𝑥 } ) ) CnP 𝑗 ) ‘ 𝑥 ) }
32 1 5 4 2 31 cmpo ⊢ ( 𝑓 ∈ ( ℂ ↑pm ℂ ) , 𝑥 ∈ ℂ ↦ { 𝑦 ∣ [ ( TopOpen ‘ ℂfld ) / 𝑗 ] ( 𝑧 ∈ ( dom 𝑓 ∪ { 𝑥 } ) ↦ if ( 𝑧 = 𝑥 , 𝑦 , ( 𝑓 ‘ 𝑧 ) ) ) ∈ ( ( ( 𝑗 ↾t ( dom 𝑓 ∪ { 𝑥 } ) ) CnP 𝑗 ) ‘ 𝑥 ) } )
33 0 32 wceq ⊢ limℂ = ( 𝑓 ∈ ( ℂ ↑pm ℂ ) , 𝑥 ∈ ℂ ↦ { 𝑦 ∣ [ ( TopOpen ‘ ℂfld ) / 𝑗 ] ( 𝑧 ∈ ( dom 𝑓 ∪ { 𝑥 } ) ↦ if ( 𝑧 = 𝑥 , 𝑦 , ( 𝑓 ‘ 𝑧 ) ) ) ∈ ( ( ( 𝑗 ↾t ( dom 𝑓 ∪ { 𝑥 } ) ) CnP 𝑗 ) ‘ 𝑥 ) } )