Description: The topology of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | topgrpfn.w | |- W = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } |
|
Assertion | topgrptset | |- ( J e. X -> J = ( TopSet ` W ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | topgrpfn.w | |- W = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } |
|
2 | 1 | topgrpstr | |- W Struct <. 1 , 9 >. |
3 | tsetid | |- TopSet = Slot ( TopSet ` ndx ) |
|
4 | snsstp3 | |- { <. ( TopSet ` ndx ) , J >. } C_ { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } |
|
5 | 4 1 | sseqtrri | |- { <. ( TopSet ` ndx ) , J >. } C_ W |
6 | 2 3 5 | strfv | |- ( J e. X -> J = ( TopSet ` W ) ) |