Metamath Proof Explorer

Theorem lmmbr2

Description: Express the binary relation "sequence F converges to point P " in a metric space. Definition 1.4-1 of Kreyszig p. 25. The condition F C_ ( CC X. X ) allows us to use objects more general than sequences when convenient; see the comment in df-lm . (Contributed by NM, 7-Dec-2006) (Revised by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses lmmbr.2 
|- J = ( MetOpen ` D )
lmmbr.3 
|- ( ph -> D e. ( *Met ` X ) )
Assertion lmmbr2 
|- ( ph -> ( F ( ~~>t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) ) )

Proof

Step Hyp Ref Expression
1 lmmbr.2 
 |-  J = ( MetOpen ` D )
2 lmmbr.3 
 |-  ( ph -> D e. ( *Met ` X ) )
3 1 2 lmmbr 
 |-  ( ph -> ( F ( ~~>t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. x e. RR+ E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) ) ) )
4 df-3an 
 |-  ( ( F e. ( X ^pm CC ) /\ P e. X /\ A. x e. RR+ E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) ) <-> ( ( F e. ( X ^pm CC ) /\ P e. X ) /\ A. x e. RR+ E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) ) )
5 uzf 
 |-  ZZ>= : ZZ --> ~P ZZ
6 ffn 
 |-  ( ZZ>= : ZZ --> ~P ZZ -> ZZ>= Fn ZZ )
7 reseq2 
 |-  ( y = ( ZZ>= ` j ) -> ( F |` y ) = ( F |` ( ZZ>= ` j ) ) )
8 id 
 |-  ( y = ( ZZ>= ` j ) -> y = ( ZZ>= ` j ) )
9 7 8 feq12d 
 |-  ( y = ( ZZ>= ` j ) -> ( ( F |` y ) : y --> ( P ( ball ` D ) x ) <-> ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( P ( ball ` D ) x ) ) )
10 9 rexrn 
 |-  ( ZZ>= Fn ZZ -> ( E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) <-> E. j e. ZZ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( P ( ball ` D ) x ) ) )
11 5 6 10 mp2b 
 |-  ( E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) <-> E. j e. ZZ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( P ( ball ` D ) x ) )
12 simp2l 
 |-  ( ( D e. ( *Met ` X ) /\ ( F e. ( X ^pm CC ) /\ P e. X ) /\ x e. RR+ ) -> F e. ( X ^pm CC ) )
13 elfvdm 
 |-  ( D e. ( *Met ` X ) -> X e. dom *Met )
14 13 3ad2ant1 
 |-  ( ( D e. ( *Met ` X ) /\ ( F e. ( X ^pm CC ) /\ P e. X ) /\ x e. RR+ ) -> X e. dom *Met )
15 cnex 
 |-  CC e. _V
16 elpmg 
 |-  ( ( X e. dom *Met /\ CC e. _V ) -> ( F e. ( X ^pm CC ) <-> ( Fun F /\ F C_ ( CC X. X ) ) ) )
17 14 15 16 sylancl 
 |-  ( ( D e. ( *Met ` X ) /\ ( F e. ( X ^pm CC ) /\ P e. X ) /\ x e. RR+ ) -> ( F e. ( X ^pm CC ) <-> ( Fun F /\ F C_ ( CC X. X ) ) ) )
18 12 17 mpbid 
 |-  ( ( D e. ( *Met ` X ) /\ ( F e. ( X ^pm CC ) /\ P e. X ) /\ x e. RR+ ) -> ( Fun F /\ F C_ ( CC X. X ) ) )
19 18 simpld 
 |-  ( ( D e. ( *Met ` X ) /\ ( F e. ( X ^pm CC ) /\ P e. X ) /\ x e. RR+ ) -> Fun F )
20 ffvresb 
 |-  ( Fun F -> ( ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( P ( ball ` D ) x ) <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( P ( ball ` D ) x ) ) ) )
21 19 20 syl 
 |-  ( ( D e. ( *Met ` X ) /\ ( F e. ( X ^pm CC ) /\ P e. X ) /\ x e. RR+ ) -> ( ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( P ( ball ` D ) x ) <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( P ( ball ` D ) x ) ) ) )
22 rpxr 
 |-  ( x e. RR+ -> x e. RR* )
23 elbl 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ x e. RR* ) -> ( ( F ` k ) e. ( P ( ball ` D ) x ) <-> ( ( F ` k ) e. X /\ ( P D ( F ` k ) ) < x ) ) )
24 22 23 syl3an3 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ x e. RR+ ) -> ( ( F ` k ) e. ( P ( ball ` D ) x ) <-> ( ( F ` k ) e. X /\ ( P D ( F ` k ) ) < x ) ) )
25 xmetsym 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ ( F ` k ) e. X ) -> ( P D ( F ` k ) ) = ( ( F ` k ) D P ) )
26 25 breq1d 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ ( F ` k ) e. X ) -> ( ( P D ( F ` k ) ) < x <-> ( ( F ` k ) D P ) < x ) )
27 26 3expa 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( F ` k ) e. X ) -> ( ( P D ( F ` k ) ) < x <-> ( ( F ` k ) D P ) < x ) )
28 27 pm5.32da 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( ( ( F ` k ) e. X /\ ( P D ( F ` k ) ) < x ) <-> ( ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) )
29 28 3adant3 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ x e. RR+ ) -> ( ( ( F ` k ) e. X /\ ( P D ( F ` k ) ) < x ) <-> ( ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) )
30 24 29 bitrd 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ x e. RR+ ) -> ( ( F ` k ) e. ( P ( ball ` D ) x ) <-> ( ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) )
31 30 3adant2l 
 |-  ( ( D e. ( *Met ` X ) /\ ( F e. ( X ^pm CC ) /\ P e. X ) /\ x e. RR+ ) -> ( ( F ` k ) e. ( P ( ball ` D ) x ) <-> ( ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) )
32 31 anbi2d 
 |-  ( ( D e. ( *Met ` X ) /\ ( F e. ( X ^pm CC ) /\ P e. X ) /\ x e. RR+ ) -> ( ( k e. dom F /\ ( F ` k ) e. ( P ( ball ` D ) x ) ) <-> ( k e. dom F /\ ( ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) ) )
33 3anass 
 |-  ( ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) <-> ( k e. dom F /\ ( ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) )
34 32 33 syl6bbr 
 |-  ( ( D e. ( *Met ` X ) /\ ( F e. ( X ^pm CC ) /\ P e. X ) /\ x e. RR+ ) -> ( ( k e. dom F /\ ( F ` k ) e. ( P ( ball ` D ) x ) ) <-> ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) )
35 34 ralbidv 
 |-  ( ( D e. ( *Met ` X ) /\ ( F e. ( X ^pm CC ) /\ P e. X ) /\ x e. RR+ ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( P ( ball ` D ) x ) ) <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) )
36 21 35 bitrd 
 |-  ( ( D e. ( *Met ` X ) /\ ( F e. ( X ^pm CC ) /\ P e. X ) /\ x e. RR+ ) -> ( ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( P ( ball ` D ) x ) <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) )
37 36 rexbidv 
 |-  ( ( D e. ( *Met ` X ) /\ ( F e. ( X ^pm CC ) /\ P e. X ) /\ x e. RR+ ) -> ( E. j e. ZZ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( P ( ball ` D ) x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) )
38 11 37 syl5bb 
 |-  ( ( D e. ( *Met ` X ) /\ ( F e. ( X ^pm CC ) /\ P e. X ) /\ x e. RR+ ) -> ( E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) )
39 38 3expa 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( F e. ( X ^pm CC ) /\ P e. X ) ) /\ x e. RR+ ) -> ( E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) )
40 39 ralbidva 
 |-  ( ( D e. ( *Met ` X ) /\ ( F e. ( X ^pm CC ) /\ P e. X ) ) -> ( A. x e. RR+ E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) <-> A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) )
41 40 pm5.32da 
 |-  ( D e. ( *Met ` X ) -> ( ( ( F e. ( X ^pm CC ) /\ P e. X ) /\ A. x e. RR+ E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) ) <-> ( ( F e. ( X ^pm CC ) /\ P e. X ) /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) ) )
42 2 41 syl 
 |-  ( ph -> ( ( ( F e. ( X ^pm CC ) /\ P e. X ) /\ A. x e. RR+ E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) ) <-> ( ( F e. ( X ^pm CC ) /\ P e. X ) /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) ) )
43 4 42 syl5bb 
 |-  ( ph -> ( ( F e. ( X ^pm CC ) /\ P e. X /\ A. x e. RR+ E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) ) <-> ( ( F e. ( X ^pm CC ) /\ P e. X ) /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) ) )
44 df-3an 
 |-  ( ( F e. ( X ^pm CC ) /\ P e. X /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) <-> ( ( F e. ( X ^pm CC ) /\ P e. X ) /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) )
45 43 44 syl6bbr 
 |-  ( ph -> ( ( F e. ( X ^pm CC ) /\ P e. X /\ A. x e. RR+ E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) ) <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) ) )
46 3 45 bitrd 
 |-  ( ph -> ( F ( ~~>t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) ) )