Metamath Proof Explorer
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 |
|
|
|
srapart.s |
|
|
Assertion |
sratset |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
srapart.a |
|
2 |
|
srapart.s |
|
3 |
|
df-tset |
|
4 |
|
9nn |
|
5 |
|
8lt9 |
|
6 |
5
|
olci |
|
7 |
1 2 3 4 6
|
sralem |
|