Theorem limccl

Description: Closure of the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016)

	Ref	Expression
Assertion	limccl	⊢ ( 𝐹 limℂ 𝐵 ) ⊆ ℂ

Proof

Step	Hyp	Ref	Expression
1		limcrcl	⊢ ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) )
2		eqid	⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( dom 𝐹 ∪ { 𝐵 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( dom 𝐹 ∪ { 𝐵 } ) )
3		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
4	2 3	limcfval	⊢ ( ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 limℂ 𝐵 ) = { 𝑦 ∣ ( 𝑧 ∈ ( dom 𝐹 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( dom 𝐹 ∪ { 𝐵 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐵 ) } ∧ ( 𝐹 limℂ 𝐵 ) ⊆ ℂ ) )
5	1 4	syl	⊢ ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) → ( ( 𝐹 limℂ 𝐵 ) = { 𝑦 ∣ ( 𝑧 ∈ ( dom 𝐹 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝑦 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( dom 𝐹 ∪ { 𝐵 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝐵 ) } ∧ ( 𝐹 limℂ 𝐵 ) ⊆ ℂ ) )
6	5	simprd	⊢ ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) → ( 𝐹 limℂ 𝐵 ) ⊆ ℂ )
7		id	⊢ ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) → 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) )
8	6 7	sseldd	⊢ ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) → 𝑥 ∈ ℂ )
9	8	ssriv	⊢ ( 𝐹 limℂ 𝐵 ) ⊆ ℂ