Metamath Proof Explorer


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 )