Theorem gidsn

Description: Obsolete as of 23-Jan-2020. Use mnd1id instead. The identity element of the trivial group. (Contributed by FL, 21-Jun-2010) (Proof shortened by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ablsn.1	|- A e. _V
Assertion	gidsn	|- ( GId ` { <. <. A , A >. , A >. } ) = A

Proof

Step	Hyp	Ref	Expression
1		ablsn.1	|- A e. _V
2	1	grposnOLD	|- { <. <. A , A >. , A >. } e. GrpOp
3		opex	|- <. A , A >. e. _V
4	3	rnsnop	|- ran { <. <. A , A >. , A >. } = { A }
5	4	eqcomi	|- { A } = ran { <. <. A , A >. , A >. }
6		eqid	|- ( GId ` { <. <. A , A >. , A >. } ) = ( GId ` { <. <. A , A >. , A >. } )
7	5 6	grpoidcl	|- ( { <. <. A , A >. , A >. } e. GrpOp -> ( GId ` { <. <. A , A >. , A >. } ) e. { A } )
8		elsni	|- ( ( GId ` { <. <. A , A >. , A >. } ) e. { A } -> ( GId ` { <. <. A , A >. , A >. } ) = A )
9	2 7 8	mp2b	|- ( GId ` { <. <. A , A >. , A >. } ) = A