Metamath Proof Explorer


Theorem resstset

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

Proof

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