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 | tsetid | |- TopSet = Slot ( TopSet ` ndx ) |
|
4 | tsetndxnbasendx | |- ( TopSet ` ndx ) =/= ( Base ` ndx ) |
|
5 | 1 2 3 4 | resseqnbas | |- ( A e. V -> J = ( TopSet ` H ) ) |