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 ) |
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 ) |