# 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 ) ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( 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 ) )`