Metamath Proof Explorer


Theorem sratset

Description: Topology component of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015) (Revised by Thierry Arnoux, 16-Jun-2019)

Ref Expression
Hypotheses srapart.a φ A = subringAlg W S
srapart.s φ S Base W
Assertion sratset φ TopSet W = TopSet A

Proof

Step Hyp Ref Expression
1 srapart.a φ A = subringAlg W S
2 srapart.s φ S Base W
3 df-tset TopSet = Slot 9
4 9nn 9
5 8lt9 8 < 9
6 5 olci 9 < 5 8 < 9
7 1 2 3 4 6 sralem φ TopSet W = TopSet A