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

Metamath Proof Explorer

Theorem limcrcl

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

Ref Expression
Assertion limcrcl ( 𝐶 ∈ ( 𝐹 limℂ 𝐵 ) → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) )

Proof

Step Hyp Ref Expression
1 df-limc ⊢ limℂ = ( 𝑓 ∈ ( ℂ ↑pm ℂ ) , 𝑥 ∈ ℂ ↦ { 𝑦 ∣ [ ( TopOpen ‘ ℂfld ) / 𝑗 ] ( 𝑧 ∈ ( dom 𝑓 ∪ { 𝑥 } ) ↦ if ( 𝑧 = 𝑥 , 𝑦 , ( 𝑓 ‘ 𝑧 ) ) ) ∈ ( ( ( 𝑗 ↾t ( dom 𝑓 ∪ { 𝑥 } ) ) CnP 𝑗 ) ‘ 𝑥 ) } )
2 1 elmpocl ⊢ ( 𝐶 ∈ ( 𝐹 limℂ 𝐵 ) → ( 𝐹 ∈ ( ℂ ↑pm ℂ ) ∧ 𝐵 ∈ ℂ ) )
3 cnex ⊢ ℂ ∈ V
4 3 3 elpm2 ⊢ ( 𝐹 ∈ ( ℂ ↑pm ℂ ) ↔ ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ) )
5 4 anbi1i ⊢ ( ( 𝐹 ∈ ( ℂ ↑pm ℂ ) ∧ 𝐵 ∈ ℂ ) ↔ ( ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ) ∧ 𝐵 ∈ ℂ ) )
6 df-3an ⊢ ( ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) ↔ ( ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ) ∧ 𝐵 ∈ ℂ ) )
7 5 6 bitr4i ⊢ ( ( 𝐹 ∈ ( ℂ ↑pm ℂ ) ∧ 𝐵 ∈ ℂ ) ↔ ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) )
8 2 7 sylib ⊢ ( 𝐶 ∈ ( 𝐹 limℂ 𝐵 ) → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) )