Metamath Proof Explorer

Theorem mgptset

Description: Topology component of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypothesis mgpbas.1 
|- M = ( mulGrp ` R )
Assertion mgptset 
|- ( TopSet ` R ) = ( TopSet ` M )

Proof

Step Hyp Ref Expression
1 mgpbas.1 
 |-  M = ( mulGrp ` R )
2 df-tset 
 |-  TopSet = Slot 9
3 9nn 
 |-  9 e. NN
4 2re 
 |-  2 e. RR
5 2lt9 
 |-  2 < 9
6 4 5 gtneii 
 |-  9 =/= 2
7 1 2 3 6 mgplem 
 |-  ( TopSet ` R ) = ( TopSet ` M )