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	|- ( ph -> F : A --> CC )
	ellimciota.a	|- ( ph -> A C_ CC )
	ellimciota.b	|- ( ph -> B e. ( ( limPt ` K ) ` A ) )
	ellimciota.4	|- ( ph -> ( F limCC B ) =/= (/) )
	ellimciota.k	|- K = ( TopOpen ` CCfld )
Assertion	ellimciota	|- ( ph -> ( iota x x e. ( F limCC B ) ) e. ( F limCC B ) )

Proof

Step	Hyp	Ref	Expression
1		ellimciota.f	|- ( ph -> F : A --> CC )
2		ellimciota.a	|- ( ph -> A C_ CC )
3		ellimciota.b	|- ( ph -> B e. ( ( limPt ` K ) ` A ) )
4		ellimciota.4	|- ( ph -> ( F limCC B ) =/= (/) )
5		ellimciota.k	|- K = ( TopOpen ` CCfld )
6		eleq1	|- ( x = y -> ( x e. ( F limCC B ) <-> y e. ( F limCC B ) ) )
7	6	cbviotavw	|- ( iota x x e. ( F limCC B ) ) = ( iota y y e. ( F limCC B ) )
8		iotaex	|- ( iota y y e. ( F limCC B ) ) e. _V
9		n0	|- ( ( F limCC B ) =/= (/) <-> E. x x e. ( F limCC B ) )
10	4 9	sylib	|- ( ph -> E. x x e. ( F limCC B ) )
11	1 2 3 5	limcmo	|- ( ph -> E* x x e. ( F limCC B ) )
12		df-eu	|- ( E! x x e. ( F limCC B ) <-> ( E. x x e. ( F limCC B ) /\ E* x x e. ( F limCC B ) ) )
13	10 11 12	sylanbrc	|- ( ph -> E! x x e. ( F limCC B ) )
14		eleq1	|- ( x = ( iota y y e. ( F limCC B ) ) -> ( x e. ( F limCC B ) <-> ( iota y y e. ( F limCC B ) ) e. ( F limCC B ) ) )
15	14	iota2	|- ( ( ( iota y y e. ( F limCC B ) ) e. _V /\ E! x x e. ( F limCC B ) ) -> ( ( iota y y e. ( F limCC B ) ) e. ( F limCC B ) <-> ( iota x x e. ( F limCC B ) ) = ( iota y y e. ( F limCC B ) ) ) )
16	8 13 15	sylancr	|- ( ph -> ( ( iota y y e. ( F limCC B ) ) e. ( F limCC B ) <-> ( iota x x e. ( F limCC B ) ) = ( iota y y e. ( F limCC B ) ) ) )
17	7 16	mpbiri	|- ( ph -> ( iota y y e. ( F limCC B ) ) e. ( F limCC B ) )
18	7 17	eqeltrid	|- ( ph -> ( iota x x e. ( F limCC B ) ) e. ( F limCC B ) )