Metamath Proof Explorer


Theorem ssrest

Description: If K is a finer topology than J , then the subspace topologies induced by A maintain this relationship. (Contributed by Mario Carneiro, 21-Mar-2015) (Revised by Mario Carneiro, 1-May-2015)

Ref Expression
Assertion ssrest
|- ( ( K e. V /\ J C_ K ) -> ( J |`t A ) C_ ( K |`t A ) )

Proof

Step Hyp Ref Expression
1 simpr
 |-  ( ( ( K e. V /\ J C_ K ) /\ x e. ( J |`t A ) ) -> x e. ( J |`t A ) )
2 ssrexv
 |-  ( J C_ K -> ( E. y e. J x = ( y i^i A ) -> E. y e. K x = ( y i^i A ) ) )
3 2 ad2antlr
 |-  ( ( ( K e. V /\ J C_ K ) /\ x e. ( J |`t A ) ) -> ( E. y e. J x = ( y i^i A ) -> E. y e. K x = ( y i^i A ) ) )
4 n0i
 |-  ( x e. ( J |`t A ) -> -. ( J |`t A ) = (/) )
5 restfn
 |-  |`t Fn ( _V X. _V )
6 fndm
 |-  ( |`t Fn ( _V X. _V ) -> dom |`t = ( _V X. _V ) )
7 5 6 ax-mp
 |-  dom |`t = ( _V X. _V )
8 7 ndmov
 |-  ( -. ( J e. _V /\ A e. _V ) -> ( J |`t A ) = (/) )
9 4 8 nsyl2
 |-  ( x e. ( J |`t A ) -> ( J e. _V /\ A e. _V ) )
10 9 adantl
 |-  ( ( ( K e. V /\ J C_ K ) /\ x e. ( J |`t A ) ) -> ( J e. _V /\ A e. _V ) )
11 elrest
 |-  ( ( J e. _V /\ A e. _V ) -> ( x e. ( J |`t A ) <-> E. y e. J x = ( y i^i A ) ) )
12 10 11 syl
 |-  ( ( ( K e. V /\ J C_ K ) /\ x e. ( J |`t A ) ) -> ( x e. ( J |`t A ) <-> E. y e. J x = ( y i^i A ) ) )
13 simpll
 |-  ( ( ( K e. V /\ J C_ K ) /\ x e. ( J |`t A ) ) -> K e. V )
14 10 simprd
 |-  ( ( ( K e. V /\ J C_ K ) /\ x e. ( J |`t A ) ) -> A e. _V )
15 elrest
 |-  ( ( K e. V /\ A e. _V ) -> ( x e. ( K |`t A ) <-> E. y e. K x = ( y i^i A ) ) )
16 13 14 15 syl2anc
 |-  ( ( ( K e. V /\ J C_ K ) /\ x e. ( J |`t A ) ) -> ( x e. ( K |`t A ) <-> E. y e. K x = ( y i^i A ) ) )
17 3 12 16 3imtr4d
 |-  ( ( ( K e. V /\ J C_ K ) /\ x e. ( J |`t A ) ) -> ( x e. ( J |`t A ) -> x e. ( K |`t A ) ) )
18 1 17 mpd
 |-  ( ( ( K e. V /\ J C_ K ) /\ x e. ( J |`t A ) ) -> x e. ( K |`t A ) )
19 18 ex
 |-  ( ( K e. V /\ J C_ K ) -> ( x e. ( J |`t A ) -> x e. ( K |`t A ) ) )
20 19 ssrdv
 |-  ( ( K e. V /\ J C_ K ) -> ( J |`t A ) C_ ( K |`t A ) )