Metamath Proof Explorer

Theorem lmfval

Description: The relation "sequence f converges to point y " in a metric space. (Contributed by NM, 7-Sep-2006) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion lmfval 
|- ( J e. ( TopOn ` X ) -> ( ~~>t ` J ) = { <. f , x >. | ( f e. ( X ^pm CC ) /\ x e. X /\ A. u e. J ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } )

Proof

Step Hyp Ref Expression
1 df-lm 
 |-  ~~>t = ( j e. Top |-> { <. f , x >. | ( f e. ( U. j ^pm CC ) /\ x e. U. j /\ A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } )
2 simpr 
 |-  ( ( J e. ( TopOn ` X ) /\ j = J ) -> j = J )
3 2 unieqd 
 |-  ( ( J e. ( TopOn ` X ) /\ j = J ) -> U. j = U. J )
4 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
5 4 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ j = J ) -> X = U. J )
6 3 5 eqtr4d 
 |-  ( ( J e. ( TopOn ` X ) /\ j = J ) -> U. j = X )
7 6 oveq1d 
 |-  ( ( J e. ( TopOn ` X ) /\ j = J ) -> ( U. j ^pm CC ) = ( X ^pm CC ) )
8 7 eleq2d 
 |-  ( ( J e. ( TopOn ` X ) /\ j = J ) -> ( f e. ( U. j ^pm CC ) <-> f e. ( X ^pm CC ) ) )
9 6 eleq2d 
 |-  ( ( J e. ( TopOn ` X ) /\ j = J ) -> ( x e. U. j <-> x e. X ) )
10 2 raleqdv 
 |-  ( ( J e. ( TopOn ` X ) /\ j = J ) -> ( A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) <-> A. u e. J ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) )
11 8 9 10 3anbi123d 
 |-  ( ( J e. ( TopOn ` X ) /\ j = J ) -> ( ( f e. ( U. j ^pm CC ) /\ x e. U. j /\ A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) <-> ( f e. ( X ^pm CC ) /\ x e. X /\ A. u e. J ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) ) )
12 11 opabbidv 
 |-  ( ( J e. ( TopOn ` X ) /\ j = J ) -> { <. f , x >. | ( f e. ( U. j ^pm CC ) /\ x e. U. j /\ A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } = { <. f , x >. | ( f e. ( X ^pm CC ) /\ x e. X /\ A. u e. J ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } )
13 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
14 df-3an 
 |-  ( ( f e. ( X ^pm CC ) /\ x e. X /\ A. u e. J ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) <-> ( ( f e. ( X ^pm CC ) /\ x e. X ) /\ A. u e. J ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) )
15 14 opabbii 
 |-  { <. f , x >. | ( f e. ( X ^pm CC ) /\ x e. X /\ A. u e. J ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } = { <. f , x >. | ( ( f e. ( X ^pm CC ) /\ x e. X ) /\ A. u e. J ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) }
16 opabssxp 
 |-  { <. f , x >. | ( ( f e. ( X ^pm CC ) /\ x e. X ) /\ A. u e. J ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } C_ ( ( X ^pm CC ) X. X )
17 15 16 eqsstri 
 |-  { <. f , x >. | ( f e. ( X ^pm CC ) /\ x e. X /\ A. u e. J ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } C_ ( ( X ^pm CC ) X. X )
18 ovex 
 |-  ( X ^pm CC ) e. _V
19 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
20 xpexg 
 |-  ( ( ( X ^pm CC ) e. _V /\ X e. J ) -> ( ( X ^pm CC ) X. X ) e. _V )
21 18 19 20 sylancr 
 |-  ( J e. ( TopOn ` X ) -> ( ( X ^pm CC ) X. X ) e. _V )
22 ssexg 
 |-  ( ( { <. f , x >. | ( f e. ( X ^pm CC ) /\ x e. X /\ A. u e. J ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } C_ ( ( X ^pm CC ) X. X ) /\ ( ( X ^pm CC ) X. X ) e. _V ) -> { <. f , x >. | ( f e. ( X ^pm CC ) /\ x e. X /\ A. u e. J ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } e. _V )
23 17 21 22 sylancr 
 |-  ( J e. ( TopOn ` X ) -> { <. f , x >. | ( f e. ( X ^pm CC ) /\ x e. X /\ A. u e. J ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } e. _V )
24 1 12 13 23 fvmptd2 
 |-  ( J e. ( TopOn ` X ) -> ( ~~>t ` J ) = { <. f , x >. | ( f e. ( X ^pm CC ) /\ x e. X /\ A. u e. J ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } )