Theorem mgptsetOLD

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	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
Assertion	mgptsetOLD	⊢ ( 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	mgplemOLD	⊢ ( TopSet ‘ 𝑅 ) = ( TopSet ‘ 𝑀 )