Theorem symgbas

Description: The base set of the symmetric group. (Contributed by Mario Carneiro, 12-Jan-2015) (Proof shortened by AV, 29-Mar-2024)

	Ref	Expression
Hypotheses	symgbas.1	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
	symgbas.2	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	symgbas	⊢ 𝐵 = { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2		symgbas.2	⊢ 𝐵 = ( Base ‘ 𝐺 )
3		eqid	⊢ { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 } = { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 }
4	1 3	symgval	⊢ 𝐺 = ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 } )
5	4	eqcomi	⊢ ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 } ) = 𝐺
6	5	fveq2i	⊢ ( Base ‘ ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 } ) ) = ( Base ‘ 𝐺 )
7		f1of	⊢ ( 𝑥 : 𝐴 –1-1-onto→ 𝐴 → 𝑥 : 𝐴 ⟶ 𝐴 )
8	7	ss2abi	⊢ { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 } ⊆ { 𝑥 ∣ 𝑥 : 𝐴 ⟶ 𝐴 }
9		eqid	⊢ ( EndoFMnd ‘ 𝐴 ) = ( EndoFMnd ‘ 𝐴 )
10		eqid	⊢ ( Base ‘ ( EndoFMnd ‘ 𝐴 ) ) = ( Base ‘ ( EndoFMnd ‘ 𝐴 ) )
11	9 10	efmndbasabf	⊢ ( Base ‘ ( EndoFMnd ‘ 𝐴 ) ) = { 𝑥 ∣ 𝑥 : 𝐴 ⟶ 𝐴 }
12	8 11	sseqtrri	⊢ { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 } ⊆ ( Base ‘ ( EndoFMnd ‘ 𝐴 ) )
13		eqid	⊢ ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 } ) = ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 } )
14	13 10	ressbas2	⊢ ( { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 } ⊆ ( Base ‘ ( EndoFMnd ‘ 𝐴 ) ) → { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 } = ( Base ‘ ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 } ) ) )
15	12 14	ax-mp	⊢ { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 } = ( Base ‘ ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 } ) )
16	6 15 2	3eqtr4ri	⊢ 𝐵 = { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 }