Metamath Proof Explorer


Theorem resstset

Description: TopSet is unaffected by restriction. (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Hypotheses resstset.1 𝐻 = ( 𝐺s 𝐴 )
resstset.2 𝐽 = ( TopSet ‘ 𝐺 )
Assertion resstset ( 𝐴𝑉𝐽 = ( TopSet ‘ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 resstset.1 𝐻 = ( 𝐺s 𝐴 )
2 resstset.2 𝐽 = ( TopSet ‘ 𝐺 )
3 tsetid TopSet = Slot ( TopSet ‘ ndx )
4 tsetndxnbasendx ( TopSet ‘ ndx ) ≠ ( Base ‘ ndx )
5 1 2 3 4 resseqnbas ( 𝐴𝑉𝐽 = ( TopSet ‘ 𝐻 ) )