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) (Proof modification is discouraged.) (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$$