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

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ℂ 𝐵 ) )