This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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