Metamath Proof Explorer


Theorem symg1bas

Description: The symmetric group on a singleton is the symmetric group S_1 consisting of the identity only. (Contributed by AV, 9-Dec-2018)

Ref Expression
Hypotheses symg1bas.1 G = SymGrp A
symg1bas.2 B = Base G
symg1bas.0 A = I
Assertion symg1bas I V B = I I

Proof

Step Hyp Ref Expression
1 symg1bas.1 G = SymGrp A
2 symg1bas.2 B = Base G
3 symg1bas.0 A = I
4 1 2 symgbas B = f | f : A 1-1 onto A
5 eqidd A = I p = p
6 id A = I A = I
7 5 6 6 f1oeq123d A = I p : A 1-1 onto A p : I 1-1 onto I
8 3 7 ax-mp p : A 1-1 onto A p : I 1-1 onto I
9 f1of p : I 1-1 onto I p : I I
10 fsng I V I V p : I I p = I I
11 10 anidms I V p : I I p = I I
12 9 11 syl5ib I V p : I 1-1 onto I p = I I
13 f1osng I V I V I I : I 1-1 onto I
14 13 anidms I V I I : I 1-1 onto I
15 f1oeq1 p = I I p : I 1-1 onto I I I : I 1-1 onto I
16 14 15 syl5ibrcom I V p = I I p : I 1-1 onto I
17 12 16 impbid I V p : I 1-1 onto I p = I I
18 8 17 syl5bb I V p : A 1-1 onto A p = I I
19 vex p V
20 f1oeq1 f = p f : A 1-1 onto A p : A 1-1 onto A
21 19 20 elab p f | f : A 1-1 onto A p : A 1-1 onto A
22 velsn p I I p = I I
23 18 21 22 3bitr4g I V p f | f : A 1-1 onto A p I I
24 23 eqrdv I V f | f : A 1-1 onto A = I I
25 4 24 eqtrid I V B = I I