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