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	imbitrid	\|- ( 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	bitrid	\|- ( 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	eqtrid	\|- ( I e. V -> B = { { <. I , I >. } } )

Metamath Proof Explorer

Theorem symg1bas

Proof