df-symg

Description: Define the symmetric group on set x . We represent the group as the set of one-to-one onto functions from x to itself under function composition, and topologize it as a function space assuming the set is discrete. This definition is based on the fact that a symmetric group is a restriction of the monoid of endofunctions. (Contributed by Paul Chapman, 25-Feb-2008) (Revised by AV, 28-Mar-2024)

		Ref	Expression
	Assertion	df-symg	⊢ SymGrp = ( 𝑥 ∈ V ↦ ( ( EndoFMnd ‘ 𝑥 ) ↾_s { ℎ ∣ ℎ : 𝑥 –1-1-onto→ 𝑥 } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csymg	⊢ SymGrp
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		cefmnd	⊢ EndoFMnd
4	1	cv	⊢ 𝑥
5	4 3	cfv	⊢ ( EndoFMnd ‘ 𝑥 )
6		cress	⊢ ↾_s
7		vh	⊢ ℎ
8	7	cv	⊢ ℎ
9	4 4 8	wf1o	⊢ ℎ : 𝑥 –1-1-onto→ 𝑥
10	9 7	cab	⊢ { ℎ ∣ ℎ : 𝑥 –1-1-onto→ 𝑥 }
11	5 10 6	co	⊢ ( ( EndoFMnd ‘ 𝑥 ) ↾_s { ℎ ∣ ℎ : 𝑥 –1-1-onto→ 𝑥 } )
12	1 2 11	cmpt	⊢ ( 𝑥 ∈ V ↦ ( ( EndoFMnd ‘ 𝑥 ) ↾_s { ℎ ∣ ℎ : 𝑥 –1-1-onto→ 𝑥 } ) )
13	0 12	wceq	⊢ SymGrp = ( 𝑥 ∈ V ↦ ( ( EndoFMnd ‘ 𝑥 ) ↾_s { ℎ ∣ ℎ : 𝑥 –1-1-onto→ 𝑥 } ) )

Metamath Proof Explorer

Definition df-symg

Detailed syntax breakdown