This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ↾ 𝑠 A
resstset.2 ⊢ J = TopSet ⁡ G
Assertion resstset ⊢ A ∈ V → J = TopSet ⁡ H

Proof

Step Hyp Ref Expression
1 resstset.1 ⊢ H = G ↾ 𝑠 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 ∈ V → J = TopSet ⁡ H