Metamath Proof Explorer

Theorem lmmbr

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

Proof

Step Hyp Ref Expression
1 lmmbr.2 
 |-  J = ( MetOpen ` D )
2 lmmbr.3 
 |-  ( ph -> D e. ( *Met ` X ) )
3 1 mopntopon 
 |-  ( D e. ( *Met ` X ) -> J e. ( TopOn ` X ) )
4 2 3 syl 
 |-  ( ph -> J e. ( TopOn ` X ) )
5 4 lmbr 
 |-  ( ph -> ( F ( ~~>t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) ) ) )
6 rpxr 
 |-  ( x e. RR+ -> x e. RR* )
7 1 blopn 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ x e. RR* ) -> ( P ( ball ` D ) x ) e. J )
8 6 7 syl3an3 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ x e. RR+ ) -> ( P ( ball ` D ) x ) e. J )
9 blcntr 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ x e. RR+ ) -> P e. ( P ( ball ` D ) x ) )
10 eleq2 
 |-  ( u = ( P ( ball ` D ) x ) -> ( P e. u <-> P e. ( P ( ball ` D ) x ) ) )
11 feq3 
 |-  ( u = ( P ( ball ` D ) x ) -> ( ( F |` y ) : y --> u <-> ( F |` y ) : y --> ( P ( ball ` D ) x ) ) )
12 11 rexbidv 
 |-  ( u = ( P ( ball ` D ) x ) -> ( E. y e. ran ZZ>= ( F |` y ) : y --> u <-> E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) ) )
13 10 12 imbi12d 
 |-  ( u = ( P ( ball ` D ) x ) -> ( ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) <-> ( P e. ( P ( ball ` D ) x ) -> E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) ) ) )
14 13 rspcva 
 |-  ( ( ( P ( ball ` D ) x ) e. J /\ A. u e. J ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) ) -> ( P e. ( P ( ball ` D ) x ) -> E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) ) )
15 14 impancom 
 |-  ( ( ( P ( ball ` D ) x ) e. J /\ P e. ( P ( ball ` D ) x ) ) -> ( A. u e. J ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) -> E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) ) )
16 8 9 15 syl2anc 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ x e. RR+ ) -> ( A. u e. J ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) -> E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) ) )
17 16 3expa 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ x e. RR+ ) -> ( A. u e. J ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) -> E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) ) )
18 17 adantlrl 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( F e. ( X ^pm CC ) /\ P e. X ) ) /\ x e. RR+ ) -> ( A. u e. J ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) -> E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) ) )
19 18 impancom 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( F e. ( X ^pm CC ) /\ P e. X ) ) /\ A. u e. J ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) ) -> ( x e. RR+ -> E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) ) )
20 19 ralrimiv 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( F e. ( X ^pm CC ) /\ P e. X ) ) /\ A. u e. J ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) ) -> A. x e. RR+ E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) )
21 1 mopni2 
 |-  ( ( D e. ( *Met ` X ) /\ u e. J /\ P e. u ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ u )
22 r19.29 
 |-  ( ( A. x e. RR+ E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) /\ E. x e. RR+ ( P ( ball ` D ) x ) C_ u ) -> E. x e. RR+ ( E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) /\ ( P ( ball ` D ) x ) C_ u ) )
23 fss 
 |-  ( ( ( F |` y ) : y --> ( P ( ball ` D ) x ) /\ ( P ( ball ` D ) x ) C_ u ) -> ( F |` y ) : y --> u )
24 23 expcom 
 |-  ( ( P ( ball ` D ) x ) C_ u -> ( ( F |` y ) : y --> ( P ( ball ` D ) x ) -> ( F |` y ) : y --> u ) )
25 24 reximdv 
 |-  ( ( P ( ball ` D ) x ) C_ u -> ( E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) )
26 25 impcom 
 |-  ( ( E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) /\ ( P ( ball ` D ) x ) C_ u ) -> E. y e. ran ZZ>= ( F |` y ) : y --> u )
27 26 rexlimivw 
 |-  ( E. x e. RR+ ( E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) /\ ( P ( ball ` D ) x ) C_ u ) -> E. y e. ran ZZ>= ( F |` y ) : y --> u )
28 22 27 syl 
 |-  ( ( A. x e. RR+ E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) /\ E. x e. RR+ ( P ( ball ` D ) x ) C_ u ) -> E. y e. ran ZZ>= ( F |` y ) : y --> u )
29 21 28 sylan2 
 |-  ( ( A. x e. RR+ E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) /\ ( D e. ( *Met ` X ) /\ u e. J /\ P e. u ) ) -> E. y e. ran ZZ>= ( F |` y ) : y --> u )
30 29 3exp2 
 |-  ( A. x e. RR+ E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) -> ( D e. ( *Met ` X ) -> ( u e. J -> ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) ) ) )
31 30 impcom 
 |-  ( ( D e. ( *Met ` X ) /\ A. x e. RR+ E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) ) -> ( u e. J -> ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) ) )
32 31 adantlr 
 |-  ( ( ( 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 ) ) -> ( u e. J -> ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) ) )
33 32 ralrimiv 
 |-  ( ( ( 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. u e. J ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) )
34 20 33 impbida 
 |-  ( ( D e. ( *Met ` X ) /\ ( F e. ( X ^pm CC ) /\ P e. X ) ) -> ( A. u e. J ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) <-> A. x e. RR+ E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) ) )
35 34 pm5.32da 
 |-  ( D e. ( *Met ` X ) -> ( ( ( F e. ( X ^pm CC ) /\ P e. X ) /\ A. u e. J ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) ) <-> ( ( F e. ( X ^pm CC ) /\ P e. X ) /\ A. x e. RR+ E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) ) ) )
36 df-3an 
 |-  ( ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) ) <-> ( ( F e. ( X ^pm CC ) /\ P e. X ) /\ A. u e. J ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) ) )
37 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 ) ) )
38 35 36 37 3bitr4g 
 |-  ( D e. ( *Met ` X ) -> ( ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) ) <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. x e. RR+ E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) ) ) )
39 2 38 syl 
 |-  ( ph -> ( ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) ) <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. x e. RR+ E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) ) ) )
40 5 39 bitrd 
 |-  ( 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 ) ) ) )