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

Metamath Proof Explorer

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ℂ 𝐵 ) ⊆ ℂ