Metamath Proof Explorer

Theorem limcrcl

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

Ref Expression
Assertion limcrcl ⊢C∈Flimℂ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⟼ifz=xyf⁡z∈j↾𝑡dom⁡f∪xCnPj⁡x
2 1 elmpocl ⊢C∈Flimℂ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∈FlimℂB→F:dom⁡F⟶ℂ∧dom⁡F⊆ℂ∧B∈ℂ