Theorem restid

Description: The subspace topology of the base set is the original topology. (Contributed by Jeff Hankins, 9-Jul-2009) (Revised by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Hypothesis	restid.1	|- X = U. J
Assertion	restid	|- ( J e. V -> ( J |`t X ) = J )

Proof

Step	Hyp	Ref	Expression
1		restid.1	|- X = U. J
2		uniexg	|- ( J e. V -> U. J e. _V )
3	1 2	eqeltrid	|- ( J e. V -> X e. _V )
4	1	eqimss2i	|- U. J C_ X
5		sspwuni	|- ( J C_ ~P X <-> U. J C_ X )
6	4 5	mpbir	|- J C_ ~P X
7		restid2	|- ( ( X e. _V /\ J C_ ~P X ) -> ( J |`t X ) = J )
8	3 6 7	sylancl	|- ( J e. V -> ( J |`t X ) = J )