Metamath Proof Explorer
Description: The topology of a topological group. (Contributed by Mario Carneiro, 27-Jun-2014) (Revised by Mario Carneiro, 13-Aug-2015)
|
|
Ref |
Expression |
|
Hypotheses |
tgpcn.j |
⊢ 𝐽 = ( TopOpen ‘ 𝐺 ) |
|
|
tgptopon.x |
⊢ 𝑋 = ( Base ‘ 𝐺 ) |
|
Assertion |
tgptopon |
⊢ ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
tgpcn.j |
⊢ 𝐽 = ( TopOpen ‘ 𝐺 ) |
2 |
|
tgptopon.x |
⊢ 𝑋 = ( Base ‘ 𝐺 ) |
3 |
|
tgptps |
⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopSp ) |
4 |
2 1
|
istps |
⊢ ( 𝐺 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
5 |
3 4
|
sylib |
⊢ ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |