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

Metamath Proof Explorer

Theorem restsspw

Description: The subspace topology is a collection of subsets of the restriction set. (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion restsspw 
|- ( J |`t A ) C_ ~P A

Proof

Step Hyp Ref Expression
1 n0i 
 |-  ( x e. ( J |`t A ) -> -. ( J |`t A ) = (/) )
2 restfn 
 |-  |`t Fn ( _V X. _V )
3 fndm 
 |-  ( |`t Fn ( _V X. _V ) -> dom |`t = ( _V X. _V ) )
4 2 3 ax-mp 
 |-  dom |`t = ( _V X. _V )
5 4 ndmov 
 |-  ( -. ( J e. _V /\ A e. _V ) -> ( J |`t A ) = (/) )
6 1 5 nsyl2 
 |-  ( x e. ( J |`t A ) -> ( J e. _V /\ A e. _V ) )
7 elrest 
 |-  ( ( J e. _V /\ A e. _V ) -> ( x e. ( J |`t A ) <-> E. y e. J x = ( y i^i A ) ) )
8 6 7 syl 
 |-  ( x e. ( J |`t A ) -> ( x e. ( J |`t A ) <-> E. y e. J x = ( y i^i A ) ) )
9 8 ibi 
 |-  ( x e. ( J |`t A ) -> E. y e. J x = ( y i^i A ) )
10 inss2 
 |-  ( y i^i A ) C_ A
11 sseq1 
 |-  ( x = ( y i^i A ) -> ( x C_ A <-> ( y i^i A ) C_ A ) )
12 10 11 mpbiri 
 |-  ( x = ( y i^i A ) -> x C_ A )
13 12 rexlimivw 
 |-  ( E. y e. J x = ( y i^i A ) -> x C_ A )
14 9 13 syl 
 |-  ( x e. ( J |`t A ) -> x C_ A )
15 velpw 
 |-  ( x e. ~P A <-> x C_ A )
16 14 15 sylibr 
 |-  ( x e. ( J |`t A ) -> x e. ~P A )
17 16 ssriv 
 |-  ( J |`t A ) C_ ~P A