Metamath Proof Explorer


Theorem sratopn

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 sratopn φ TopOpen W = TopOpen A

Proof

Step Hyp Ref Expression
1 srapart.a φ A = subringAlg W S
2 srapart.s φ S Base W
3 1 2 srabase φ Base W = Base A
4 1 2 sratset φ TopSet W = TopSet A
5 3 4 topnpropd φ TopOpen W = TopOpen A