This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 5 fndmi 
 |-  dom |`t = ( _V X. _V )
7 6 ndmov 
 |-  ( -. ( J e. _V /\ A e. _V ) -> ( J |`t A ) = (/) )
8 4 7 nsyl2 
 |-  ( x e. ( J |`t A ) -> ( J e. _V /\ A e. _V ) )
9 8 adantl 
 |-  ( ( ( K e. V /\ J C_ K ) /\ x e. ( J |`t A ) ) -> ( J e. _V /\ A e. _V ) )
10 elrest 
 |-  ( ( J e. _V /\ A e. _V ) -> ( x e. ( J |`t A ) <-> E. y e. J x = ( y i^i A ) ) )
11 9 10 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 ) ) )
12 simpll 
 |-  ( ( ( K e. V /\ J C_ K ) /\ x e. ( J |`t A ) ) -> K e. V )
13 9 simprd 
 |-  ( ( ( K e. V /\ J C_ K ) /\ x e. ( J |`t A ) ) -> A e. _V )
14 elrest 
 |-  ( ( K e. V /\ A e. _V ) -> ( x e. ( K |`t A ) <-> E. y e. K x = ( y i^i A ) ) )
15 12 13 14 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 ) ) )
16 3 11 15 3imtr4d 
 |-  ( ( ( K e. V /\ J C_ K ) /\ x e. ( J |`t A ) ) -> ( x e. ( J |`t A ) -> x e. ( K |`t A ) ) )
17 1 16 mpd 
 |-  ( ( ( K e. V /\ J C_ K ) /\ x e. ( J |`t A ) ) -> x e. ( K |`t A ) )
18 17 ex 
 |-  ( ( K e. V /\ J C_ K ) -> ( x e. ( J |`t A ) -> x e. ( K |`t A ) ) )
19 18 ssrdv 
 |-  ( ( K e. V /\ J C_ K ) -> ( J |`t A ) C_ ( K |`t A ) )