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