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