Theorem lmbr3v

Description: Express the binary relation "sequence F converges to point P " in a metric space using an arbitrary upper set of integers. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypothesis	lmbr3v.1	|- ( ph -> J e. ( TopOn ` X ) )
Assertion	lmbr3v	|- ( ph -> ( F ( ~~>t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lmbr3v.1	|- ( ph -> J e. ( TopOn ` X ) )
2		eqid	|- ( ZZ>= ` 0 ) = ( ZZ>= ` 0 )
3		0zd	|- ( ph -> 0 e. ZZ )
4	1 2 3	lmbr2	|- ( ph -> ( F ( ~~>t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. j e. ( ZZ>= ` 0 ) A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )
5		0z	|- 0 e. ZZ
6	2	rexuz3	|- ( 0 e. ZZ -> ( E. j e. ( ZZ>= ` 0 ) A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
7	5 6	ax-mp	|- ( E. j e. ( ZZ>= ` 0 ) A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) )
8	7	imbi2i	|- ( ( P e. u -> E. j e. ( ZZ>= ` 0 ) A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) <-> ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
9	8	ralbii	|- ( A. u e. J ( P e. u -> E. j e. ( ZZ>= ` 0 ) A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) <-> A. u e. J ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
10	9	3anbi3i	|- ( ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. j e. ( ZZ>= ` 0 ) A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) )
11	4 10	bitrdi	|- ( ph -> ( F ( ~~>t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )