This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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→ 𝐴 }