Theorem mgptset

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

	Ref	Expression
Hypothesis	mgpbas.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
Assertion	mgptset	⊢ ( TopSet ‘ 𝑅 ) = ( TopSet ‘ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		mgpbas.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
2		df-tset	⊢ TopSet = Slot 9
3		9nn	⊢ 9 ∈ ℕ
4		2re	⊢ 2 ∈ ℝ
5		2lt9	⊢ 2 < 9
6	4 5	gtneii	⊢ 9 ≠ 2
7	1 2 3 6	mgplem	⊢ ( TopSet ‘ 𝑅 ) = ( TopSet ‘ 𝑀 )