Description: The topology of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | topgrpfn.w | ⊢ 𝑊 = { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( TopSet ‘ ndx ) , 𝐽 〉 } | |
Assertion | topgrptset | ⊢ ( 𝐽 ∈ 𝑋 → 𝐽 = ( TopSet ‘ 𝑊 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | topgrpfn.w | ⊢ 𝑊 = { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( TopSet ‘ ndx ) , 𝐽 〉 } | |
2 | 1 | topgrpstr | ⊢ 𝑊 Struct 〈 1 , 9 〉 |
3 | tsetid | ⊢ TopSet = Slot ( TopSet ‘ ndx ) | |
4 | snsstp3 | ⊢ { 〈 ( TopSet ‘ ndx ) , 𝐽 〉 } ⊆ { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( TopSet ‘ ndx ) , 𝐽 〉 } | |
5 | 4 1 | sseqtrri | ⊢ { 〈 ( TopSet ‘ ndx ) , 𝐽 〉 } ⊆ 𝑊 |
6 | 2 3 5 | strfv | ⊢ ( 𝐽 ∈ 𝑋 → 𝐽 = ( TopSet ‘ 𝑊 ) ) |