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 ⊢ φ → F lim ℂ B ≠ ∅
ellimciota.k ⊢ K = TopOpen ⁡ ℂ fld
Assertion ellimciota ⊢ φ → ι x | x ∈ F lim ℂ B ∈ F lim ℂ 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 ⊢ φ → F lim ℂ B ≠ ∅
5 ellimciota.k ⊢ K = TopOpen ⁡ ℂ fld
6 eleq1 ⊢ x = y → x ∈ F lim ℂ B ↔ y ∈ F lim ℂ B
7 6 cbviotavw ⊢ ι x | x ∈ F lim ℂ B = ι y | y ∈ F lim ℂ B
8 iotaex ⊢ ι y | y ∈ F lim ℂ B ∈ V
9 n0 ⊢ F lim ℂ B ≠ ∅ ↔ ∃ x x ∈ F lim ℂ B
10 4 9 sylib ⊢ φ → ∃ x x ∈ F lim ℂ B
11 1 2 3 5 limcmo ⊢ φ → ∃* x x ∈ F lim ℂ B
12 df-eu ⊢ ∃! x x ∈ F lim ℂ B ↔ ∃ x x ∈ F lim ℂ B ∧ ∃* x x ∈ F lim ℂ B
13 10 11 12 sylanbrc ⊢ φ → ∃! x x ∈ F lim ℂ B
14 eleq1 ⊢ x = ι y | y ∈ F lim ℂ B → x ∈ F lim ℂ B ↔ ι y | y ∈ F lim ℂ B ∈ F lim ℂ B
15 14 iota2 ⊢ ι y | y ∈ F lim ℂ B ∈ V ∧ ∃! x x ∈ F lim ℂ B → ι y | y ∈ F lim ℂ B ∈ F lim ℂ B ↔ ι x | x ∈ F lim ℂ B = ι y | y ∈ F lim ℂ B
16 8 13 15 sylancr ⊢ φ → ι y | y ∈ F lim ℂ B ∈ F lim ℂ B ↔ ι x | x ∈ F lim ℂ B = ι y | y ∈ F lim ℂ B
17 7 16 mpbiri ⊢ φ → ι y | y ∈ F lim ℂ B ∈ F lim ℂ B
18 7 17 eqeltrid ⊢ φ → ι x | x ∈ F lim ℂ B ∈ F lim ℂ B