Theorem restid2

Description: The subspace topology over a subset of the base set is the original topology. (Contributed by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Assertion	restid2	|- ( ( A e. V /\ J C_ ~P A ) -> ( J |`t A ) = J )

Proof

Step	Hyp	Ref	Expression
1		pwexg	|- ( A e. V -> ~P A e. _V )
2	1	adantr	|- ( ( A e. V /\ J C_ ~P A ) -> ~P A e. _V )
3		simpr	|- ( ( A e. V /\ J C_ ~P A ) -> J C_ ~P A )
4	2 3	ssexd	|- ( ( A e. V /\ J C_ ~P A ) -> J e. _V )
5		simpl	|- ( ( A e. V /\ J C_ ~P A ) -> A e. V )
6		restval	|- ( ( J e. _V /\ A e. V ) -> ( J |`t A ) = ran ( x e. J |-> ( x i^i A ) ) )
7	4 5 6	syl2anc	|- ( ( A e. V /\ J C_ ~P A ) -> ( J |`t A ) = ran ( x e. J |-> ( x i^i A ) ) )
8	3	sselda	|- ( ( ( A e. V /\ J C_ ~P A ) /\ x e. J ) -> x e. ~P A )
9	8	elpwid	|- ( ( ( A e. V /\ J C_ ~P A ) /\ x e. J ) -> x C_ A )
10		df-ss	|- ( x C_ A <-> ( x i^i A ) = x )
11	9 10	sylib	|- ( ( ( A e. V /\ J C_ ~P A ) /\ x e. J ) -> ( x i^i A ) = x )
12	11	mpteq2dva	|- ( ( A e. V /\ J C_ ~P A ) -> ( x e. J |-> ( x i^i A ) ) = ( x e. J |-> x ) )
13		mptresid	|- ( _I |` J ) = ( x e. J |-> x )
14	12 13	eqtr4di	|- ( ( A e. V /\ J C_ ~P A ) -> ( x e. J |-> ( x i^i A ) ) = ( _I |` J ) )
15	14	rneqd	|- ( ( A e. V /\ J C_ ~P A ) -> ran ( x e. J |-> ( x i^i A ) ) = ran ( _I |` J ) )
16		rnresi	|- ran ( _I |` J ) = J
17	15 16	eqtrdi	|- ( ( A e. V /\ J C_ ~P A ) -> ran ( x e. J |-> ( x i^i A ) ) = J )
18	7 17	eqtrd	|- ( ( A e. V /\ J C_ ~P A ) -> ( J |`t A ) = J )