Metamath Proof Explorer

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 }