Metamath Proof Explorer

Theorem limccl

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

Ref Expression
Assertion limccl ⊢ F lim ℂ B ⊆ ℂ

Proof

Step Hyp Ref Expression
1 limcrcl ⊢ x ∈ F lim ℂ B → F : dom ⁡ F ⟶ ℂ ∧ dom ⁡ F ⊆ ℂ ∧ B ∈ ℂ
2 eqid ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 dom ⁡ F ∪ B = TopOpen ⁡ ℂ fld ↾ 𝑡 dom ⁡ F ∪ B
3 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
4 2 3 limcfval ⊢ F : dom ⁡ F ⟶ ℂ ∧ dom ⁡ F ⊆ ℂ ∧ B ∈ ℂ → F lim ℂ B = y | z ∈ dom ⁡ F ∪ B ⟼ if z = B y F ⁡ z ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 dom ⁡ F ∪ B CnP TopOpen ⁡ ℂ fld ⁡ B ∧ F lim ℂ B ⊆ ℂ
5 1 4 syl ⊢ x ∈ F lim ℂ B → F lim ℂ B = y | z ∈ dom ⁡ F ∪ B ⟼ if z = B y F ⁡ z ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 dom ⁡ F ∪ B CnP TopOpen ⁡ ℂ fld ⁡ B ∧ F lim ℂ B ⊆ ℂ
6 5 simprd ⊢ x ∈ F lim ℂ B → F lim ℂ B ⊆ ℂ
7 id ⊢ x ∈ F lim ℂ B → x ∈ F lim ℂ B
8 6 7 sseldd ⊢ x ∈ F lim ℂ B → x ∈ ℂ
9 8 ssriv ⊢ F lim ℂ B ⊆ ℂ