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 e. 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 e. V /\ I e. V ) -> ( p : { I } --> { I } <-> p = { <. I , I >. } ) )
11 10 anidms 
 |-  ( I e. V -> ( p : { I } --> { I } <-> p = { <. I , I >. } ) )
12 9 11 syl5ib 
 |-  ( I e. V -> ( p : { I } -1-1-onto-> { I } -> p = { <. I , I >. } ) )
13 f1osng 
 |-  ( ( I e. V /\ I e. V ) -> { <. I , I >. } : { I } -1-1-onto-> { I } )
14 13 anidms 
 |-  ( I e. 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 e. V -> ( p = { <. I , I >. } -> p : { I } -1-1-onto-> { I } ) )
17 12 16 impbid 
 |-  ( I e. V -> ( p : { I } -1-1-onto-> { I } <-> p = { <. I , I >. } ) )
18 8 17 syl5bb 
 |-  ( I e. V -> ( p : A -1-1-onto-> A <-> p = { <. I , I >. } ) )
19 vex 
 |-  p e. _V
20 f1oeq1 
 |-  ( f = p -> ( f : A -1-1-onto-> A <-> p : A -1-1-onto-> A ) )
21 19 20 elab 
 |-  ( p e. { f | f : A -1-1-onto-> A } <-> p : A -1-1-onto-> A )
22 velsn 
 |-  ( p e. { { <. I , I >. } } <-> p = { <. I , I >. } )
23 18 21 22 3bitr4g 
 |-  ( I e. V -> ( p e. { f | f : A -1-1-onto-> A } <-> p e. { { <. I , I >. } } ) )
24 23 eqrdv 
 |-  ( I e. V -> { f | f : A -1-1-onto-> A } = { { <. I , I >. } } )
25 4 24 syl5eq 
 |-  ( I e. V -> B = { { <. I , I >. } } )