Theorem symgid

Description: The group identity element of the symmetric group on a set A . (Contributed by Paul Chapman, 25-Jul-2008) (Revised by Mario Carneiro, 13-Jan-2015) (Proof shortened by AV, 1-Apr-2024)

	Ref	Expression
Hypothesis	symggrp.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
Assertion	symgid	$$⊢A\in V\to {\mathrm{I}\upharpoonright }_A=0_G$$

Proof

Step	Hyp	Ref	Expression
1		symggrp.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		eqid	Could not format ( EndoFMnd ` A ) = ( EndoFMnd ` A ) : No typesetting found for |- ( EndoFMnd ` A ) = ( EndoFMnd ` A ) with typecode |-
3	2	efmndid	Could not format ( A e. V -> ( _I |` A ) = ( 0g ` ( EndoFMnd ` A ) ) ) : No typesetting found for |- ( A e. V -> ( _I |` A ) = ( 0g ` ( EndoFMnd ` A ) ) ) with typecode |-
4		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
5	2 1 4	symgsubmefmnd	Could not format ( A e. V -> ( Base ` G ) e. ( SubMnd ` ( EndoFMnd ` A ) ) ) : No typesetting found for |- ( A e. V -> ( Base ` G ) e. ( SubMnd ` ( EndoFMnd ` A ) ) ) with typecode |-
6	1 4 2	symgressbas	Could not format G = ( ( EndoFMnd ` A ) |`s ( Base ` G ) ) : No typesetting found for |- G = ( ( EndoFMnd ` A ) |`s ( Base ` G ) ) with typecode |-
7		eqid	Could not format ( 0g ` ( EndoFMnd ` A ) ) = ( 0g ` ( EndoFMnd ` A ) ) : No typesetting found for |- ( 0g ` ( EndoFMnd ` A ) ) = ( 0g ` ( EndoFMnd ` A ) ) with typecode |-
8	6 7	subm0	Could not format ( ( Base ` G ) e. ( SubMnd ` ( EndoFMnd ` A ) ) -> ( 0g ` ( EndoFMnd ` A ) ) = ( 0g ` G ) ) : No typesetting found for |- ( ( Base ` G ) e. ( SubMnd ` ( EndoFMnd ` A ) ) -> ( 0g ` ( EndoFMnd ` A ) ) = ( 0g ` G ) ) with typecode |-
9	5 8	syl	Could not format ( A e. V -> ( 0g ` ( EndoFMnd ` A ) ) = ( 0g ` G ) ) : No typesetting found for |- ( A e. V -> ( 0g ` ( EndoFMnd ` A ) ) = ( 0g ` G ) ) with typecode |-
10	3 9	eqtrd	$$⊢A\in V\to {\mathrm{I}\upharpoonright }_A=0_G$$