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 ⊢ 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 ↾ 𝑠 x | x : A ⟶ 1-1 onto A
5 4 eqcomi ⊢ EndoFMnd ⁡ A ↾ 𝑠 x | x : A ⟶ 1-1 onto A = G
6 5 fveq2i ⊢ Base EndoFMnd ⁡ A ↾ 𝑠 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 ⊆ 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 ⊆ Base EndoFMnd ⁡ A
13 eqid ⊢ EndoFMnd ⁡ A ↾ 𝑠 x | x : A ⟶ 1-1 onto A = EndoFMnd ⁡ A ↾ 𝑠 x | x : A ⟶ 1-1 onto A
14 13 10 ressbas2 ⊢ x | x : A ⟶ 1-1 onto A ⊆ Base EndoFMnd ⁡ A → x | x : A ⟶ 1-1 onto A = Base EndoFMnd ⁡ A ↾ 𝑠 x | x : A ⟶ 1-1 onto A
15 12 14 ax-mp ⊢ x | x : A ⟶ 1-1 onto A = Base EndoFMnd ⁡ A ↾ 𝑠 x | x : A ⟶ 1-1 onto A
16 6 15 2 3eqtr4ri ⊢ B = x | x : A ⟶ 1-1 onto A