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 𝑗 ) ‘ 𝑥 ) } )