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 ( 𝜑𝐹 : 𝐴 ⟶ ℂ )
ellimciota.a ( 𝜑𝐴 ⊆ ℂ )
ellimciota.b ( 𝜑𝐵 ∈ ( ( limPt ‘ 𝐾 ) ‘ 𝐴 ) )
ellimciota.4 ( 𝜑 → ( 𝐹 lim 𝐵 ) ≠ ∅ )
ellimciota.k 𝐾 = ( TopOpen ‘ ℂfld )
Assertion ellimciota ( 𝜑 → ( ℩ 𝑥 𝑥 ∈ ( 𝐹 lim 𝐵 ) ) ∈ ( 𝐹 lim 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ellimciota.f ( 𝜑𝐹 : 𝐴 ⟶ ℂ )
2 ellimciota.a ( 𝜑𝐴 ⊆ ℂ )
3 ellimciota.b ( 𝜑𝐵 ∈ ( ( limPt ‘ 𝐾 ) ‘ 𝐴 ) )
4 ellimciota.4 ( 𝜑 → ( 𝐹 lim 𝐵 ) ≠ ∅ )
5 ellimciota.k 𝐾 = ( TopOpen ‘ ℂfld )
6 eleq1 ( 𝑥 = 𝑦 → ( 𝑥 ∈ ( 𝐹 lim 𝐵 ) ↔ 𝑦 ∈ ( 𝐹 lim 𝐵 ) ) )
7 6 cbviotavw ( ℩ 𝑥 𝑥 ∈ ( 𝐹 lim 𝐵 ) ) = ( ℩ 𝑦 𝑦 ∈ ( 𝐹 lim 𝐵 ) )
8 iotaex ( ℩ 𝑦 𝑦 ∈ ( 𝐹 lim 𝐵 ) ) ∈ V
9 n0 ( ( 𝐹 lim 𝐵 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝐹 lim 𝐵 ) )
10 4 9 sylib ( 𝜑 → ∃ 𝑥 𝑥 ∈ ( 𝐹 lim 𝐵 ) )
11 1 2 3 5 limcmo ( 𝜑 → ∃* 𝑥 𝑥 ∈ ( 𝐹 lim 𝐵 ) )
12 df-eu ( ∃! 𝑥 𝑥 ∈ ( 𝐹 lim 𝐵 ) ↔ ( ∃ 𝑥 𝑥 ∈ ( 𝐹 lim 𝐵 ) ∧ ∃* 𝑥 𝑥 ∈ ( 𝐹 lim 𝐵 ) ) )
13 10 11 12 sylanbrc ( 𝜑 → ∃! 𝑥 𝑥 ∈ ( 𝐹 lim 𝐵 ) )
14 eleq1 ( 𝑥 = ( ℩ 𝑦 𝑦 ∈ ( 𝐹 lim 𝐵 ) ) → ( 𝑥 ∈ ( 𝐹 lim 𝐵 ) ↔ ( ℩ 𝑦 𝑦 ∈ ( 𝐹 lim 𝐵 ) ) ∈ ( 𝐹 lim 𝐵 ) ) )
15 14 iota2 ( ( ( ℩ 𝑦 𝑦 ∈ ( 𝐹 lim 𝐵 ) ) ∈ V ∧ ∃! 𝑥 𝑥 ∈ ( 𝐹 lim 𝐵 ) ) → ( ( ℩ 𝑦 𝑦 ∈ ( 𝐹 lim 𝐵 ) ) ∈ ( 𝐹 lim 𝐵 ) ↔ ( ℩ 𝑥 𝑥 ∈ ( 𝐹 lim 𝐵 ) ) = ( ℩ 𝑦 𝑦 ∈ ( 𝐹 lim 𝐵 ) ) ) )
16 8 13 15 sylancr ( 𝜑 → ( ( ℩ 𝑦 𝑦 ∈ ( 𝐹 lim 𝐵 ) ) ∈ ( 𝐹 lim 𝐵 ) ↔ ( ℩ 𝑥 𝑥 ∈ ( 𝐹 lim 𝐵 ) ) = ( ℩ 𝑦 𝑦 ∈ ( 𝐹 lim 𝐵 ) ) ) )
17 7 16 mpbiri ( 𝜑 → ( ℩ 𝑦 𝑦 ∈ ( 𝐹 lim 𝐵 ) ) ∈ ( 𝐹 lim 𝐵 ) )
18 7 17 eqeltrid ( 𝜑 → ( ℩ 𝑥 𝑥 ∈ ( 𝐹 lim 𝐵 ) ) ∈ ( 𝐹 lim 𝐵 ) )