# 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}\in \mathrm{V}$
Assertion gidsn ${⊢}\mathrm{GId}\left(\left\{⟨⟨{A},{A}⟩,{A}⟩\right\}\right)={A}$

### Proof

Step Hyp Ref Expression
1 ablsn.1 ${⊢}{A}\in \mathrm{V}$
2 1 grposnOLD ${⊢}\left\{⟨⟨{A},{A}⟩,{A}⟩\right\}\in \mathrm{GrpOp}$
3 opex ${⊢}⟨{A},{A}⟩\in \mathrm{V}$
4 3 rnsnop ${⊢}\mathrm{ran}\left\{⟨⟨{A},{A}⟩,{A}⟩\right\}=\left\{{A}\right\}$
5 4 eqcomi ${⊢}\left\{{A}\right\}=\mathrm{ran}\left\{⟨⟨{A},{A}⟩,{A}⟩\right\}$
6 eqid ${⊢}\mathrm{GId}\left(\left\{⟨⟨{A},{A}⟩,{A}⟩\right\}\right)=\mathrm{GId}\left(\left\{⟨⟨{A},{A}⟩,{A}⟩\right\}\right)$
7 5 6 grpoidcl ${⊢}\left\{⟨⟨{A},{A}⟩,{A}⟩\right\}\in \mathrm{GrpOp}\to \mathrm{GId}\left(\left\{⟨⟨{A},{A}⟩,{A}⟩\right\}\right)\in \left\{{A}\right\}$
8 elsni ${⊢}\mathrm{GId}\left(\left\{⟨⟨{A},{A}⟩,{A}⟩\right\}\right)\in \left\{{A}\right\}\to \mathrm{GId}\left(\left\{⟨⟨{A},{A}⟩,{A}⟩\right\}\right)={A}$
9 2 7 8 mp2b ${⊢}\mathrm{GId}\left(\left\{⟨⟨{A},{A}⟩,{A}⟩\right\}\right)={A}$