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 𝐺 = ( 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𝐴 }