Metamath Proof Explorer

Theorem limcrcl

Description: Reverse closure for the limit operator. (Contributed by Mario Carneiro, 28-Dec-2016)

Ref Expression
Assertion limcrcl ⊢ C ∈ F lim ℂ B → F : dom ⁡ F ⟶ ℂ ∧ dom ⁡ F ⊆ ℂ ∧ B ∈ ℂ

Proof

Step Hyp Ref Expression
1 df-limc ⊢ lim ℂ = f ∈ ℂ ↑ 𝑝𝑚 ℂ , x ∈ ℂ ⟼ y | [˙ TopOpen ⁡ ℂ fld / j]˙ z ∈ dom ⁡ f ∪ x ⟼ if z = x y f ⁡ z ∈ j ↾ 𝑡 dom ⁡ f ∪ x CnP j ⁡ x
2 1 elmpocl ⊢ C ∈ F lim ℂ B → F ∈ ℂ ↑ 𝑝𝑚 ℂ ∧ B ∈ ℂ
3 cnex ⊢ ℂ ∈ V
4 3 3 elpm2 ⊢ F ∈ ℂ ↑ 𝑝𝑚 ℂ ↔ F : dom ⁡ F ⟶ ℂ ∧ dom ⁡ F ⊆ ℂ
5 4 anbi1i ⊢ F ∈ ℂ ↑ 𝑝𝑚 ℂ ∧ B ∈ ℂ ↔ F : dom ⁡ F ⟶ ℂ ∧ dom ⁡ F ⊆ ℂ ∧ B ∈ ℂ
6 df-3an ⊢ F : dom ⁡ F ⟶ ℂ ∧ dom ⁡ F ⊆ ℂ ∧ B ∈ ℂ ↔ F : dom ⁡ F ⟶ ℂ ∧ dom ⁡ F ⊆ ℂ ∧ B ∈ ℂ
7 5 6 bitr4i ⊢ F ∈ ℂ ↑ 𝑝𝑚 ℂ ∧ B ∈ ℂ ↔ F : dom ⁡ F ⟶ ℂ ∧ dom ⁡ F ⊆ ℂ ∧ B ∈ ℂ
8 2 7 sylib ⊢ C ∈ F lim ℂ B → F : dom ⁡ F ⟶ ℂ ∧ dom ⁡ F ⊆ ℂ ∧ B ∈ ℂ