Metamath Proof Explorer

Theorem sslm

Description: A finer topology has fewer convergent sequences (but the sequences that do converge, converge to the same value). (Contributed by Mario Carneiro, 15-Sep-2015)

Ref Expression
Assertion sslm 
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) -> ( ~~>t ` K ) C_ ( ~~>t ` J ) )

Proof

Step Hyp Ref Expression
1 idd 
 |-  ( J C_ K -> ( f e. ( X ^pm CC ) -> f e. ( X ^pm CC ) ) )
2 idd 
 |-  ( J C_ K -> ( x e. X -> x e. X ) )
3 ssralv 
 |-  ( J C_ K -> ( A. u e. K ( 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 ) ) )
4 1 2 3 3anim123d 
 |-  ( J C_ K -> ( ( f e. ( X ^pm CC ) /\ x e. X /\ A. u e. K ( 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 ) ) ) )
5 4 ssopab2dv 
 |-  ( J C_ K -> { <. f , x >. | ( f e. ( X ^pm CC ) /\ x e. X /\ A. u e. K ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } C_ { <. 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 ) ) } )
6 5 3ad2ant3 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) -> { <. f , x >. | ( f e. ( X ^pm CC ) /\ x e. X /\ A. u e. K ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } C_ { <. 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 ) ) } )
7 lmfval 
 |-  ( K e. ( TopOn ` X ) -> ( ~~>t ` K ) = { <. f , x >. | ( f e. ( X ^pm CC ) /\ x e. X /\ A. u e. K ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } )
8 7 3ad2ant2 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) -> ( ~~>t ` K ) = { <. f , x >. | ( f e. ( X ^pm CC ) /\ x e. X /\ A. u e. K ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } )
9 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 ) ) } )
10 9 3ad2ant1 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) -> ( ~~>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 ) ) } )
11 6 8 10 3sstr4d 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) -> ( ~~>t ` K ) C_ ( ~~>t ` J ) )