Description: Obsolete version of mgptset as of 18-Oct-2024. Topology component of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | mgpbas.1 | |- M = ( mulGrp ` R ) |
|
| Assertion | mgptsetOLD | |- ( TopSet ` R ) = ( TopSet ` M ) |
| 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 | mgplemOLD | |- ( TopSet ` R ) = ( TopSet ` M ) |