Description: TopSet is unaffected by restriction. (Contributed by Mario Carneiro, 13-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | resstset.1 | |- H = ( G |`s A ) |
|
resstset.2 | |- J = ( TopSet ` G ) |
||
Assertion | resstset | |- ( A e. V -> J = ( TopSet ` H ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resstset.1 | |- H = ( G |`s A ) |
|
2 | resstset.2 | |- J = ( TopSet ` G ) |
|
3 | df-tset | |- TopSet = Slot 9 |
|
4 | 9nn | |- 9 e. NN |
|
5 | 1lt9 | |- 1 < 9 |
|
6 | 1 2 3 4 5 | resslem | |- ( A e. V -> J = ( TopSet ` H ) ) |