Metamath Proof Explorer

Theorem ellimciota

Description: An explicit value for the limit, when the limit exists at a limit point. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses ellimciota.f ⊢φ→F:A⟶ℂ
ellimciota.a ⊢φ→A⊆ℂ
ellimciota.b ⊢φ→B∈limPt⁡K⁡A
ellimciota.4 ⊢φ→FlimℂB≠∅
ellimciota.k ⊢K=TopOpen⁡ℂfld
Assertion ellimciota ⊢φ→ιx|x∈FlimℂB∈FlimℂB

Proof

Step Hyp Ref Expression
1 ellimciota.f ⊢φ→F:A⟶ℂ
2 ellimciota.a ⊢φ→A⊆ℂ
3 ellimciota.b ⊢φ→B∈limPt⁡K⁡A
4 ellimciota.4 ⊢φ→FlimℂB≠∅
5 ellimciota.k ⊢K=TopOpen⁡ℂfld
6 eleq1 ⊢x=y→x∈FlimℂB↔y∈FlimℂB
7 6 cbviotavw ⊢ιx|x∈FlimℂB=ιy|y∈FlimℂB
8 iotaex ⊢ιy|y∈FlimℂB∈V
9 n0 ⊢FlimℂB≠∅↔∃xx∈FlimℂB
10 4 9 sylib ⊢φ→∃xx∈FlimℂB
11 1 2 3 5 limcmo ⊢φ→∃*xx∈FlimℂB
12 df-eu ⊢∃!xx∈FlimℂB↔∃xx∈FlimℂB∧∃*xx∈FlimℂB
13 10 11 12 sylanbrc ⊢φ→∃!xx∈FlimℂB
14 eleq1 ⊢x=ιy|y∈FlimℂB→x∈FlimℂB↔ιy|y∈FlimℂB∈FlimℂB
15 14 iota2 ⊢ιy|y∈FlimℂB∈V∧∃!xx∈FlimℂB→ιy|y∈FlimℂB∈FlimℂB↔ιx|x∈FlimℂB=ιy|y∈FlimℂB
16 8 13 15 sylancr ⊢φ→ιy|y∈FlimℂB∈FlimℂB↔ιx|x∈FlimℂB=ιy|y∈FlimℂB
17 7 16 mpbiri ⊢φ→ιy|y∈FlimℂB∈FlimℂB
18 7 17 eqeltrid ⊢φ→ιx|x∈FlimℂB∈FlimℂB