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