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	|- G = ( SymGrp ` A )
	symgbas.2	|- B = ( Base ` G )
Assertion	symgbas	|- B = { x | x : A -1-1-onto-> A }

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	|- G = ( SymGrp ` A )
2		symgbas.2	|- B = ( Base ` G )
3		eqid	|- { x | x : A -1-1-onto-> A } = { x | x : A -1-1-onto-> A }
4	1 3	symgval	|- G = ( ( EndoFMnd ` A ) |`s { x | x : A -1-1-onto-> A } )
5	4	eqcomi	|- ( ( EndoFMnd ` A ) |`s { x | x : A -1-1-onto-> A } ) = G
6	5	fveq2i	|- ( Base ` ( ( EndoFMnd ` A ) |`s { x | x : A -1-1-onto-> A } ) ) = ( Base ` G )
7		f1of	|- ( x : A -1-1-onto-> A -> x : A --> A )
8	7	ss2abi	|- { x | x : A -1-1-onto-> A } C_ { x | x : A --> A }
9		eqid	|- ( EndoFMnd ` A ) = ( EndoFMnd ` A )
10		eqid	|- ( Base ` ( EndoFMnd ` A ) ) = ( Base ` ( EndoFMnd ` A ) )
11	9 10	efmndbasabf	|- ( Base ` ( EndoFMnd ` A ) ) = { x | x : A --> A }
12	8 11	sseqtrri	|- { x | x : A -1-1-onto-> A } C_ ( Base ` ( EndoFMnd ` A ) )
13		eqid	|- ( ( EndoFMnd ` A ) |`s { x | x : A -1-1-onto-> A } ) = ( ( EndoFMnd ` A ) |`s { x | x : A -1-1-onto-> A } )
14	13 10	ressbas2	|- ( { x | x : A -1-1-onto-> A } C_ ( Base ` ( EndoFMnd ` A ) ) -> { x | x : A -1-1-onto-> A } = ( Base ` ( ( EndoFMnd ` A ) |`s { x | x : A -1-1-onto-> A } ) ) )
15	12 14	ax-mp	|- { x | x : A -1-1-onto-> A } = ( Base ` ( ( EndoFMnd ` A ) |`s { x | x : A -1-1-onto-> A } ) )
16	6 15 2	3eqtr4ri	|- B = { x | x : A -1-1-onto-> A }