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 ) )